当大语言模型在数学推理中频频出现 " 幻觉 "，如何让 AI 的数学证明像人类数学家一样严谨可靠？

这个困扰 AI 研究界多年的难题，在近日落幕的 CCF" 面向大模型的形式化数学竞赛 " 中找到了突破性答案。

一支名为 "Lean 说的都队 " 的联合队伍从 33 支参赛队伍中脱颖而出，以总分第一的成绩斩获冠军。这支北大华为的联合队伍，凭借华为 openPangu-Ultra-MoE-718B 和创新的技术架构，在形式化数学推理这一 "AI 硬骨头 " 上实现了重要突破。

权威赛事：瞄准大模型的数学 " 硬伤 "

这项由中国计算机学会主办、蚂蚁数字科技等多家知名机构支持的竞赛，旨在解决大模型在数学推理中的核心痛点—— " 幻觉 " 和不可靠问题。作为 CCF 大数据与计算智能大赛（CCF BDCI）的重要组成部分，该赛事吸引了来自全球的 33 支顶尖团队参与。

与传统数学问答不同，竞赛要求参赛模型将自然语言描述的数学问题，直接转化为能被计算机验证的形式化证明代码（Lean/Litex），整个过程禁止使用任何自然语言解释。这相当于要求 AI 既要是数学家，又要是程序员，既要理解数学问题的本质，又要用严格的编程语言表达证明过程。

赛事组织方明确指出：" 本赛题具有重要现实意义：它不仅是对当前大模型形式化推理能力的一次系统性检验，也为未来构建可信赖的大模型提供技术路径和推理能力评估基准 "

硬核成绩：从 33 支队伍中脱颖而出

在 30 多支队伍，参赛人数超过 600 余人的激烈的竞争中，"Lean 说的都队 " 展现出了卓越的实力。根据最终成绩统计：

初赛阶段：正确解答 181 道题目（共 220 道），初赛分数 82.27 分

决赛阶段：正确解答 5 道高难度题目（共 50 道），决赛分数 10 分

方案评审：技术方案获得 87 分的高分

最终总分：57.21 分，位列榜首

队伍成员包括来自北京大学的袁野、刘成武、李博涛、谢佳璇、李思齐，指导教师为北京大学张铭教授。队伍在比赛中展现了强大的技术实力和创新能力。

技术突破：openPangu-Ultra-MoE-718B 大模型 + 混合式架构

技术团队的核心创新在于构建了一个协同式求解系统，巧妙地将华为 openPangu 大模型的形式数学推理能力与专用证明器的高效性相结合。

openPangu 大模型的卓越表现

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

该模型采用了业界主流的 Multi-head Latent Attention（MLA）、Multi-Token Prediction（MTP）、大稀疏比等架构，以及 Depth-Scaled Sandwich-Norm 和 TinyInit 等特有设计。

在形式化数学推理任务中，openPangu 大模型展现出了强大的语义理解能力和形式化表达能力，在处理抽象数学概念和复杂逻辑时表现出色。团队发现，openPangu-Ultra-MoE-718B 模型在自动定理证明中最具代表性的数论和代数问题形式化任务上表现出非常强劲的性能。

在比赛的真实场景数据上的实测表明，openPangu-Ultra-MoE-718B 模型在 Lean 的语法检查通过率方面与国际前沿的 Gemini 2.5 Pro 和 GPT-5 模型表现相当。在形式化命题的可证明性上，openPangu-Ultra-MoE-718B 模型得到的命题更加适配当前的自动定理证明器，形式化命题的可证明命题比例方面更具优势。

创新的混合式架构

面对自动形式化定理证明中能力覆盖与语义对齐的双重挑战，团队提出了 " 能力动态分配机制 " 和 " 多层质量检查体系 "。

系统架构核心特点：

1. 动态切换策略：系统首先尝试使用流水线方法，将自然语言问题输入自动形式化器生成 Lean 语句，经过语法和语义检查后交由专用证明器进行证明。如果流水线方法失败，系统会自动回退到单体模型方法，让前沿大语言模型直接同时完成形式化和证明任务。

2. 多层质量检查：建立了从语法正确性到语义一致性的完整质量保障体系，包括 Kimina Server 的语法验证和严格的语义对齐检查。

3. 多模型协同：除了 openPangu 大模型，团队还综合使用多种前沿模型，根据不同模型的知识边界和成本效率进行智能调度。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 ]

挑战与展望：AI 数学证明的 " 最后堡垒 "

尽管取得了显著进展，团队也坦诚指出了当前系统的局限性。现有证明器主要在高中竞赛题目上训练，对微积分、代数几何等高度专业化数学分支的掌握仍显不足；单题平均约 1 小时的求解时间也限制了在时间敏感场景下的应用。

" 可以预期的原因是无论是 Goedel-Prover 还是主流的 LLM 在竞赛类的题目上都进行了充分训练，自身自然语言推理能力就很强，" 团队分析道，" 而在高等数学类的题目上，无论是 benchmark 还是数据集都处在很稀缺的状态，很多数学背景的概念 LLM 难以用 Lean 语言表达。"

展望未来，团队建议通过主动学习从失败案例中提取高等数学语料，构建专门化证明器；探索基于难度预估的动态采样策略；建立可证明的语义等价性框架。同时，人机协作的交互式证明模式也值得关注，允许数学家在关键决策点介入并提供高层次指导。

团队成员介绍

袁野

北京大学计算机学院，导师是 DLIB 实验室的张铭教授，本科毕业于北京大学信息科学技术学院智能科学系图灵班。研究方向主要为大模型的 RAG 与 Agent 构建，AI4Math，形式化数学定理证明等。

刘成武

北京大学计算机学院数据科学与工程所博士生，导师是 DLIB 实验室的张铭教授。他在北京大学外国语学院获得了文学学士学位，并修读获得了信息科学技术学院的计算机科学与技术双学位。他的研究方向是自然语言处理、大语言模型的数学推理和自动定理证明，目前他正在华为基础大模型部语言实验室实习。

李博涛

北京大学信息科学技术学院本科生，目前在 DLIB 实验室实习。在校时成绩优良，热爱探索，曾获校内程序设计大赛奖项，高中时的数学竞赛经历让他对自动定理证明更感兴趣，在这次团队比赛过程中也增加了许多新的理解，期待未来继续探索定理证明领域的边界。

谢佳璇

北京大学软件与微电子学院硕士生，目前在 DLIB 实验室实习。本科毕业于北京大学地球与空间科学学院。她主要研究自动形式化与自动定理证明，工作 FMC 被 ICML25 AI4Math Workshop 接收。

李思齐

李思齐，北京大学信息科学技术学院大四本科生，导师是 DLIB 实验室的张铭教授。目前就读于北京大学图灵班，本科期间曾获 ICPC2022 南京区域赛金奖。

张铭

北京大学计算机学院二级教授，博士生导师，北大 - 安克大模型算法与应用联合实验室主任。2021 年 CCF 杰出教育奖获得者。

张铭教授本硕博都毕业于北京大学计算机系，长期致力于机器学习、图神经网络、知识图谱、文本挖掘、语言模型、推荐系统、教育大数据、科学智能等相关研究。

先后主持国家重点研发计划课题、国家自然科学基金等前沿项目，发表科研论文 300 多篇，谷歌学术被引用 24400 余次。合作提出的 LINE 模型是图机器学习领域著名的的基准模型，目前单篇被引用 7100 余次。

获得了机器学习顶级会议 ICML 2014 唯一的最佳论文奖 ACL 2025 最佳论文奖，以及 WWW 2016 最佳论文提名。

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

北大华为联队的这一突破性成果，不仅为中国在 AI 形式化推理领域赢得了荣誉，更为大模型在严谨数学证明这一 " 最后堡垒 " 的攻克提供了可行的技术路线。

随着 openPangu 等国产大模型的持续进化，我们有理由期待 AI 在数学研究、科学发现、教育辅助和软件验证等领域扮演越来越重要的角色。形式化数学证明这一曾经被认为是 AI" 禁区 " 的领域，正在被中国科研团队一步步攻克。

" 能力互补优于盲目扩大计算，分解式严格对齐优于宽松验证。" ——这不仅是 "Lean 说的都队 " 的技术哲学，或许也是 AI 攻克形式化数学证明这一终极挑战的可行路径。

一键三连「点赞」「转发」「小心心」

欢迎在评论区留下你的想法！

—  完  —

我们正在招聘一名眼疾手快、关注 AI 的学术编辑实习生 

感兴趣的小伙伴欢迎关注  了解详情

点亮星标

科技前沿进展每日见