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

当大谈话模子在数学推理中常常出现“幻觉”，何如让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 ilradical_eq_of_integral_extension [CommRing R] [CommRing R'] [Algebra R R']    (h : Algebra.IsIntegral R R') (hinj : Function.Injective (algebraMap R R')) :    ilradical 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     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]      orm_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 orm_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 orm_num)      · ring_nf; exact Real.sq_sqrt (by orm_num)  rw [h2]  have h3 : Real.sqrt 40 ≠ -Real.sqrt 40 := by    have h_pos : 0 < Real.sqrt 40 := Real.sqrt_pos.mpr (by orm_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攻克面容化数学解释这一终极挑战的可行旅途。