北大华为联队斩获ICML AI4MATH Workshop赛道第一：让AI完成端到端形式化与定理证明

现如今，大语言模型的能力日益增强，AI已经可以逐渐攻克IMO级别的竞赛难题。作为人工智能与数学交叉的重要前沿方向，AI4Math正在推动AI从“解决数学问题”迈向“理解数学、发现数学与创造数学”，被认为是探索更高阶人工智能能力的重要路径。

然而，数学推理的核心不仅在于给出一个答案，更在于证明每一步推理都可靠。我们如何验证这些证明的正确性呢？形式化数学为这一挑战提供了新的解决方案：以Lean 4为代表的形式化证明系统，要求每一步推理都经过严格的类型检查和数学库验证，使AI生成的证明能够被机器独立检验。如果能够将人类可读的数学证明自动转化为形式化语言，AI的数学推理能力便能够从“看起来正确”走向“严格可信”。这正是ICML 2026 AI4Math Workshop所希望参赛者做的。

在Workshop举办的竞赛 Track 4: End-to-End Autoformalization and Theorem Proving 比赛中，由计算机学院博士生刘成武领衔、张铭教授指导的北大华为联合队 Kagemusha 取得了第一名，并由硕士生谢佳璇在Workshop现场进行报告。团队提出的 Coverage-Driven Loop Engineering 方法，将自然语言证明视为需要被覆盖的“证明蓝图”，让模型在生成、检查、反馈和修正的循环中逐步完善形式化证明。

一、赛事背景：ShadowBench 难在哪里

ShadowBench 是一个面向 Lean 4 的端到端自动形式化基准。它给出数学问题、自然语言证明、允许使用的 imports 和形式化规则，要求模型生成完整、规范、能够运行的 Lean 4 定理与证明。

它的一个重要特点是，评测并不只看代码能不能编译。官方还会使用隐藏的 Lean 检查代码去调用参赛者提交的定理，判断这个定理是否真的包含原题所要求的数学结论。比如题目要求证明某个最大值存在且能够取到，如果模型只证明了某个数是上界，代码本身可能可以编译，但隐藏检查就无法通过。

这项任务的难点在于，模型首先要读懂自然语言证明中的变量、条件、结论和逻辑关系，并补全人类证明中省略的步骤；同时，它还要正确使用公开数据库 Mathlib 中的定义、引理和定理，并严格遵守 imports、namespace 和声明名称等规则。因此，它综合考查数学理解、Lean 编程、定理检索、形式化推理和自动纠错能力。

二、冠军成绩：两项指标均位列第一

在本次比赛中，北大华为联合队伍 Kagemusha 位列第一，获得 Track 4: End-to-End Autoformalization and Theorem Proving 冠军。

这项比赛的核心指标是 SA-Pass Rate。正如前文所述，评测时，系统会使用一组隐藏的声明，尝试调用选手提交的内容。如果能成功通过 Lean 的类型检查，就说明提交的定理满足要求的语义性质，这道题会被计为一次 SA-Pass。另一个辅助指标是 Compile Rate，用来衡量提交的 Lean 代码本身能否通过类型检查。也就是说，想拿到 SA-Pass，首先必须写出真正能编译的 Lean 代码。此外，官方还会给一定形式化的结构限制。

最终，Team Kagemusha 取得 SA-Pass Rate 0.3089，在 123 道可评测题中解决 28 道；Compile Rate 达到 1.0，即全部提交均通过类型检查。两个指标均位列第一。

三、让模型学会“边写边查”：不是一次生成，而是反复修正

团队的一个核心判断是：这类任务很难依靠模型一次性完成，因此需要将整个系统设计为一个持续检查、反馈与修正的迭代过程。

首先，Agent 生成证明的基本框架，并利用团队设计的 Proof Coverage 指标，检查自然语言证明中的关键论证是否已被 Lean 代码充分覆盖。随后，模型根据覆盖情况与验证反馈持续补全证明、修正错误，并逐步消除 sorry 等临时占位内容。

在 Agent 内部的迭代循环之外，团队还设置了一层更严格的外部验证机制。该机制以可执行的代码级检查为基础，分别从编译结果、形式化规则约束以及目标定理的结构一致性三个方面进行验证，并将发现的问题反馈给 Agent 继续修正。

通过内外两层验证机制的协同，系统能够在保证代码可编译的基础上，进一步提升形式化证明的完整性、规范性与语义可靠性。

四、核心思想：Proof Coverage

图中上半部分展示的是团队提出的 Coverage Evaluation 机制。它相当于给 AI 证明过程装上一个“进度检查器”：不只看 Lean 代码能不能编译，还要看自然语言证明到底被形式化了多少。

第一步，系统会把 AI 写出的 Lean 证明片段，和原始自然语言证明逐段对应起来，检查三件事：这段代码是否对应原证明中的这一步，代码本身能不能通过 Lean 检查，以及它是不是真的推进了证明。这样可以判断哪些证明片段已经被覆盖，哪些地方还缺内容。

第二步，系统会从整体上再检查一次，避免“局部看起来都对，但整体证明仍然有漏洞”。例如，有的证明可能漏掉了关键方向，或者把本该证明的结论当成了假设。因此系统会继续检查：定理声明是否忠实对应原问题，证明是否覆盖所有关键目标，假设是否合理。

最后，这两层结果会合成一个覆盖分数，并反馈给形式化 Agent。下一轮修改时，Agent 就能知道哪里已经做对、哪里还没覆盖、哪里可能只是“看起来像证明”，从而有针对性地补充证明。

五、未来挑战

不过，这项工作也并不意味着端到端自动形式化已经被“解决”。

Coverage 指标本身也还有继续打磨的空间。目前它依赖 Semantic Alignment、Proof Substance、Dependency 和 Proof-level Adjustment 等多个组件，仍有人工设计的痕迹。还有一种常见情况是，Lean 证明可能采用了和自然语言证明不同、但数学上正确的路线，这时按文本区间去匹配覆盖情况，就可能低估系统的真实进展。

团队也观察到，相同的 Agent 和 Prompt 反复运行，很快会出现收益递减。到后期，继续堆算力未必比调整搜索策略、模型组合或验证反馈设计更有效。未来，团队希望进一步探索策略感知的证明匹配、更自动化的 Coverage 权重学习，并把这类方法拓展到软件验证、硬件验证和教育辅助证明等更广泛的场景。

六、团队成员介绍

刘成武

北京大学计算机学院数据科学与工程所博士生，导师是北大DLIB实验室的张铭教授。他的研究方向是自然语言处理、大语言模型的数学推理和自动定理证明。利用形式语言识别自然语言幻觉的工作Safe [2]和形式语言证明Hard-Mode框架 DAP [3] 分别被ACL 2025和ACL 2026主会接收。目前他正在华为基础大模型部语言实验室实习。

冯子晋

华为基础大模型部研究员，从事大语言模型与智能体相关研究，目前研究方向包括数学推理、自动定理证明、代码智能体等。

谢佳璇

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

袁野

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

索浦

目前在北京大学DLIB实验室实习，本科毕业于埃默里大学（Emory University），获应用数学与统计学学位。他感兴趣的主要方向为形式化方法以及机器学习与数学的交叉。

李思齐

李思齐，本科毕业于北京大学信息科学技术学院，导师是DLIB实验室的张铭教授，期间曾获ICPC 2022南京区域赛金奖。2026年秋季学期，他将进入北京大学计算机学院攻读硕士学位，并继续在张铭教授指导下开展研究。

李博涛

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

张铭

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

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

先后主持国家重点研发计划课题、国家自然科学基金等前沿项目，发表科研论文400多篇，谷歌学术被引用27400余次。

获得了机器学习顶级会议ICML 2014唯一的最佳论文奖、ACL 2025最佳论文奖，以及WWW 2026十年时间检验奖。

结语

除了本次ICML 2026 AI4Math Workshop的Track4赛道第一，该团队还曾在CCF 2025年举办的“面向大模型的形式化数学竞赛”中斩获冠军。这体现了北大华为联合团队在自动形式化与定理证明方向上的探索成果，同时也展现了AI4Math领域正在发生的重要转变：除了“能否给出答案”，我们现在更关注于AI “能否提供可信、可验证的推理过程”。

从数学研究到软件验证，形式化证明正在成为衡量AI推理可靠性的重要工具。未来，AI不仅需要具备解决复杂问题的能力，更需要能够解释自己的推理过程，并将其转化为机器可以验证的知识。自动形式化正是连接大模型能力与可信数学智能的重要桥梁。

参考文献

1． ICML AI4Math 比赛链接：https://www.codabench.org/competitions/16295/

2． Liu, C., Yuan, Y., Yin, Y., Xu, Y., Xu, X., Chen, Z., ... & Zhang, M. (2025, July). Safe: Enhancing mathematical reasoning in large language models via retrospective step-aware formal verification. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) (pp. 12171-12186).

3． Liu, C., Yin, Y., Yuan, Y., Xie, J., Li, B., Li, S., ... & Zhang, M. (2026, July). Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4. In Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers) (pp. 117-133).

4． Xie, J., Liu, C., Yuan, Y., Li, S., Xiao, Z., & Zhang, M. (2025). Fmc: Formalization of natural language mathematical competition problems. arXiv preprint arXiv:2507.11275.