北大华为联队夺冠：形式化数学竞赛33支队伍角逐，国产大模型啃下形式化证明硬骨头

Lean说的都队 投稿 
量子位 | 公众号 QbitAI

当大语言模型在数学推理中频繁出现“幻觉”，如何让AI的数学证明像人类数学家一样严谨可靠？这一长期困扰AI研究界的难题，在近日落幕的CCF“面向大模型的形式化数学竞赛”中迎来突破。

由北京大学与华为联合组成的“Lean说的都队”从33支参赛队伍中脱颖而出，凭借华为openPangu-Ultra-MoE-718B大模型及创新技术架构，以总分第一的成绩夺得冠军，实现了在形式化数学推理领域的关键突破。

权威赛事：直击大模型数学“软肋”

由中国计算机学会主办、蚂蚁数字科技等机构支持的本次竞赛，是CCF大数据与计算智能大赛（CCF BDCI）的重要组成部分，聚焦解决大模型在数学推理中的“幻觉”与不可靠问题，吸引了全球33支顶尖团队参与。

不同于传统数学问答，赛事要求模型将自然语言描述的数学问题直接转化为可被计算机验证的形式化证明代码（Lean/Litex），全程禁止使用自然语言解释。这意味着AI必须兼具数学理解力与编程表达能力，既要准确理解题意，又要用严格语法完成证明。

赛事组织方指出：“本赛题不仅系统检验了当前大模型的形式化推理能力，也为构建可信AI提供了技术路径和评估基准。”

硬核战绩：33支强队中拔得头筹

在超过600人参与的激烈角逐中，“Lean说的都队”表现卓越：

• 初赛阶段：正确解答181道题（共220道），得分82.27
• 决赛阶段：成功攻克5道高难度题目（共50道），满分10分
• 方案评审：技术方案获87分高分
• 最终总分：57.21分，位居榜首

团队成员包括北京大学袁野、刘成武、李博涛、谢佳璇、李思齐，指导教师为北大张铭教授。

技术突破：openPangu大模型+混合式架构

团队构建了协同式求解系统，融合华为openPangu大模型的强大语义理解能力与专用证明器的高效执行优势，实现性能互补。

openPangu大模型的突出表现

核心模型openPangu-Ultra-MoE-718B是华为基于昇腾NPU从零训练的大规模混合专家语言模型，总参数量达7180亿，激活参数量390亿，具备快慢思考融合能力。

该模型采用Multi-head Latent Attention（MLA）、Multi-Token Prediction（MTP）等先进架构，并集成Depth-Scaled Sandwich-Norm、TinyInit等特有设计，在处理抽象数学概念和复杂逻辑时展现出强大能力。

实测显示，其在数论与代数类形式化任务中性能强劲，Lean语法检查通过率媲美Gemini 2.5 Pro与GPT-5，且生成命题更适配自动定理证明器，显著提升可证明性比例。

创新混合式架构设计

针对形式化证明中的能力覆盖与语义对齐挑战，团队提出“动态分配机制”与“多层质量检查体系”。

系统三大核心特性：

1. 动态切换策略：优先采用流水线方式生成Lean语句并交由证明器验证；失败则回退至单体模型直接完成形式化与证明。
2. 多层质量检查：建立涵盖语法正确性与语义一致性的完整保障体系，包含Kimina Server语法校验与严格语义对齐检测。
3. 多模型协同调度：综合调用多种前沿模型，依据知识边界与成本效率进行智能分配，openPangu-Ultra-MoE-718B因在数论与代数任务上的优异表现被设为默认主模型。

关键创新：语义分解验证机制

传统LLM-as-a-Judge方法易导致“判定过松”——表面语义匹配但本质偏离原题。为此，团队引入基于语义分解的多层级验证机制，将自然语言问题拆解为数据类型、前提条件、证明目标三个正交维度，实现从模糊匹配到结构化精确对齐的范式升级。

该机制源于团队先前工作FMC（Formalization of Natural Language Mathematical Competition Problems），已在ICML 2025 AI4Math Workshop发表。

团队表示：“我们识别出传统方法存在系统性误判风险，因此提出结构化解构策略，显著提升了形式化结果的可靠性。”

实战案例：覆盖抽象代数与复数计算

技术架构在实际场景中展现出广泛适应性，以下为两个典型示例：

案例一：抽象代数问题（c4078）

原始命题：“设R’/R是环的整扩张，证明rad(R)=rad(R’)∩R，其中rad(R)表示R的幂零根。”

模型表现：系统成功完成推理与表达，生成严谨Lean代码，准确处理环论核心概念。

import Mathlib.RingTheory.Nilpotentimport Mathlib.RingTheory.IntegralClosureopen Idealtheorem nilradical_eq_of_integral_extension [CommRing R] [CommRing R'] [Algebra R R']    (h : Algebra.IsIntegral R R') (hinj : Function.Injective (algebraMap R R')) :    nilradical R = (nilradical R').comap (algebraMap R R') := by  ext x  constructor  · intro hx    rw [mem_comap]    obtain ⟨n, hn⟩ := mem_nilradical.mp hx    exact mem_nilradical.mpr ⟨n, by rw [← map_pow, hn, map_zero]⟩  · intro hx    have hx' := mem_comap.mp hx    obtain ⟨n, hn⟩ := mem_nilradical.mp hx'    apply mem_nilradical.mpr    use n    apply hinj    rw [map_pow, hn, map_zero]

案例二：复数计算问题（c27）

原始命题：“有多少个实数c满足|3-ci|=7？”

模型表现：系统通过拆解子问题、计算中间值，最终生成完整形式化证明，展现处理复数运算与逻辑推导的能力。

import Mathlibopen Complextheorem problem_c27 : ({c : ℝ | Complex.abs ((3 : ℂ) - (c : ℂ) * Complex.I) = 7}).ncard = 2 := by  have h_normSq : ∀ c : ℝ, Complex.normSq ((3 : ℂ) - (c : ℂ) * Complex.I) = 9 + c ^ 2 := by    intro c    simp [Complex.normSq]    ring  have h_abs : ∀ c : ℝ, Complex.abs ((3 : ℂ) - (c : ℂ) * Complex.I) = Real.sqrt (9 + c ^ 2) := by    intro c    calc      Complex.abs ((3 : ℂ) - (c : ℂ) * Complex.I) = Real.sqrt (Complex.normSq ((3 : ℂ) - (c : ℂ) * Complex.I)) := rfl      _ = Real.sqrt (9 + c ^ 2) := by rw [h_normSq]  have h_equiv : ∀ c : ℝ, Complex.abs ((3 : ℂ) - (c : ℂ) * Complex.I) = 7 ↔ c ^ 2 = 40 := by    intro c    rw [h_abs c]    constructor    · intro h      have h1 : (Real.sqrt (9 + c ^ 2)) ^ 2 = 7 ^ 2 := by rw [h]      rw [Real.sq_sqrt (by positivity)] at h1      linarith    · intro h      have : 9 + c ^ 2 = 49 := by linarith      rw [this]      norm_num  have h1 : {c : ℝ | Complex.abs ((3 : ℂ) - (c : ℂ) * Complex.I) = 7} = {c : ℝ | c ^ 2 = 40} :=    Set.ext fun c => by rw [Set.mem_setOf_eq, Set.mem_setOf_eq, h_equiv c]  rw [h1]  have h2 : {c : ℝ | c ^ 2 = 40} = {Real.sqrt 40, -Real.sqrt 40} := by    ext c    simp only [Set.mem_setOf_eq, Set.mem_insert_iff, Set.mem_singleton_iff]    constructor    · intro h      have : c ^ 2 = (Real.sqrt 40) ^ 2 := by rw [Real.sq_sqrt (by norm_num), h]      have : (c - Real.sqrt 40) * (c + Real.sqrt 40) = 0 := by linarith      rcases eq_zero_or_eq_zero_of_mul_eq_zero this with (h' | h'')      · left; linarith      · right; linarith    · rintro (rfl | rfl)      · exact Real.sq_sqrt (by norm_num)      · ring_nf; exact Real.sq_sqrt (by norm_num)  rw [h2]  have h3 : Real.sqrt 40 ≠ -Real.sqrt 40 := by    have h_pos : 0 < Real.sqrt 40 := Real.sqrt_pos.mpr (by norm_num)    linarith  simp [h3]

挑战与展望：迈向高等数学推理

尽管取得突破，团队坦言当前系统仍存局限：现有证明器主要基于高中竞赛题训练，对微积分、代数几何等高级数学领域掌握不足；单题平均求解耗时约1小时，难以满足实时应用需求。

团队分析认为，主流大模型在竞赛类题目上训练充分，而在高等数学领域缺乏高质量数据集与评测基准，导致概念表达困难。

未来方向包括：通过主动学习从失败案例中提取高等数学语料，构建专业化证明器；探索基于难度预估的动态采样策略；建立可证明的语义等价框架；发展人机协作的交互式证明模式，允许数学家在关键节点介入指导。

团队成员介绍

袁野：北京大学计算机学院硕士生，导师张铭教授，本科毕业于北大图灵班。研究方向为大模型RAG与Agent构建、AI4Math、形式化定理证明。

刘成武：北大计算机学院博士生，导师张铭教授，现于华为基础大模型部语言实验室实习。研究方向为自然语言处理、大模型数学推理与自动定理证明。

李博涛：北大信息科学技术学院本科生，DLIB实验室实习生，曾获校程序设计大赛奖项，高中具数学竞赛背景。

谢佳璇：北大软件与微电子学院硕士生，DLIB实验室实习生，本科毕业于地球与空间科学学院。研究方向为自动形式化与定理证明，相关成果FMC被ICML25 AI4Math Workshop接收。

李思齐：北大信息科学技术学院大四本科生，图灵班成员，曾获ICPC2022南京区域赛金奖。

张铭：北京大学计算机学院二级教授、博导，北大-安克大模型算法与应用联合实验室主任，2021年CCF杰出教育奖获得者。长期从事机器学习、图神经网络、知识图谱、语言模型等领域研究，主持多项国家级科研项目，发表论文300余篇，谷歌学术引用超2.4万次。其合作提出的LINE模型为图机器学习重要基准，单篇引用逾7100次，曾获ICML 2014最佳论文奖、ACL 2025最佳论文奖及WWW 2016最佳论文提名。

结语：国产大模型的新里程碑

“Lean说的都队”的夺冠标志着中国在AI形式化数学推理领域迈出关键一步。依托openPangu等国产大模型的持续进化，AI在数学研究、科学发现、教育辅助与软件验证中的作用正日益凸显。

曾经被视为AI“禁区”的形式化证明，正在被中国科研力量逐步攻克。“能力互补优于盲目扩大计算，分解式严格对齐优于宽松验证”——这不仅是团队的技术哲学，也可能成为AI征服数学终极挑战的核心路径。