当大语言模型在数学推理中频频陷入“幻觉陷阱”，如何让大模型的数学证明具备与人类数学家相媲美的严谨性与可信度？
这一问题长期困扰着全球AI研究者，尤其是在涉及数学证明的自动化与形式化领域。然而，随着中国计算机学会CCF“面向大模型的形式化数学竞赛”的圆满落幕，这一困难终于迎来了突破性的解决方案。
本次竞赛中，在学院全时导师严骏驰教授的带领下，来自上海创智学院与上海交通大学学生组成的“transcendental_function”队伍，凭借其开创性的“检索增强的级联式形式化推理框架”，从全球33支团队中脱颖而出，以总分第二的优异成绩摘得亚军！
1.形式化数学竞赛：直击大模型推理的“幻觉陷阱”
由中国计算机学会（CCF）主办、蚂蚁数科冠名支持的“面向大模型的形式化数学竞赛”是一项聚焦于评估和推动大模型在形式化数学推理领域能力的创新型竞赛。比赛直指当前通用大模型的核心软肋——逻辑幻觉、输出不可验证。
与传统的数学问答任务不同，本次竞赛要求参赛系统将自然语言描述的数学问题，自动转化为可被形式化证明系统（Lean/Litex）编译并验证通过的形式化命题，且给出对应的形式化证明代码。全程禁止使用任何自然语言解释或辅助说明。最终输出必须是一段语法正确、逻辑完整、能够独立通过验证器检查的证明脚本。
竞赛采用 Lean 4 作为主要的形式化语言环境。Lean 4 是一个基于依赖类型理论的交互式定理证明系统，其配套的数学库 Mathlib 已形式化涵盖从初等代数到高等数学（如实分析、抽象代数、拓扑等）的大量定理，是当前形式化数学社区广泛采用的开源基础设施。在 Lean 4 中，所有证明都必须通过严格的类型检查和逻辑验证，任何推理漏洞或语义偏差均无法通过。
赛事组织方指出，本赛题不仅系统性地评估了大模型在形式化数学推理方面的真实能力，也为构建可验证、可信赖的人工智能系统提供了关键的技术路径与标准化评估基准。
2.全球亚军：创智/交大团队从全球33支队伍中脱颖而出
在竞赛中，共有来自全球的33支顶尖队伍、超过600名研究人员和工程师参与角逐，竞争异常激烈。来自上海创智学院和上海交通大学的transcendental_function队凭借稳定而高效的表现，最终以总分第二的优异成绩荣获全球亚军。
比赛分为初赛和决赛两个阶段，历时26天，根据赛事官方的最终成绩统计：
·初赛阶段：正确解答179道题目（共220道），初赛得分81.36
·决赛阶段：正确解答5道高难度题目（共50道），决赛得分10
·方案评审：技术方案获得88.5的高分（满分100，为全场最高）
·最终得分：56.74，位列全球第二（前三名分别为57.21、56.74、55.69，与第一名相差0.5分）
队伍成员包括来自上海创智学院和上海交通大学的刘祺, 鲍康捷, 邱博林, 郑心浩，指导教师为上海创智学院全时导师严骏驰教授。
该团队利用开源社区主流模型和公开可用的通用大模型API接口，搭建了从自然语言数学问题生成形式化命题及证明的端到端系统，强调透明性、公平性、普及性三大核心原则，实现了轻量级专家模型与通用大模型的高效协同。
3.核心技术：检索增强的级联式形式化推理框架
该团队提出了一套检索增强的级联式形式化推理框架，其核心流程包含以下四个阶段：
（1）半形式化 (Semi-formalization)。若输入为自然语言求解题，先调用推理模型进行求解，然后组成自然语言命题 (Informal Statement)。然后将自然语言命题正规化为与Lean形式化命题风格接近的半形式化命题 (Semi-formalized Statement)。
（2）自形式化 (Autoformalization)。使用开源模型对半形式化命题进行形式化。如果类型检查或语意一致性检测失败，则进行依赖检索增强 (Dependency-retrieval-augmented) 的自形式化修复。
（3）形式化检验。使用Lean对形式化命题进行类型检查 (Typecheck)；使用开源模型对自然语言命题和形式化命题，以及解精化 (Delaboration) 重构的形式化命题进行语意一致性检查。
（4）定理证明 (Theorem Proving)。使用固定的启发式策略 (Tactic) 尝试证明，失败则调用开源模型生成证明，再次失败则先生成证明骨干 (Proof Sketch)再尝试证明其中的各个证明空隙 (Proof Gap)，如此递归。对于所有失败的证明和证明骨干，尝试进行依赖检索增强 (Dependency-retrieval-augmented) 的自形式化修复。
4.关键创新：半形式化解耦与语义重构
针对语义一致性检验这一形式化证明关键性难题上，该团队并未直接采用LLM-as-a-Judge的传统方法，而是结合了半形式化解耦、基于解精化的语义重构等创新性技术。
对于输入的自然语言形式化的数学问题，不同于直接对其形式化，该团队首先利用通用推理模型对问题进行求解与逻辑重构，生成结构更为严谨、逻辑链条清晰的半形式化命题，在自然语言空间进行的任务解耦，利用通用大模型强大的推理先验弥补了专家小模型推理能力和自然语言能力的不足。
此外，该团队注意到，自形式化得到的命题通常缺乏详尽的类型注释，由此，团队对Lean的打印优化器和解精化器进行调优，从解析到的证明状态中基于优化打印的表达式重构出对应的形式化语句。重构语句在保持较高可读性的同时，具有详尽的类型注释、运算优先级注释等细节信息，弥补了通用大模型缺乏Lean的细节语法先验的缺陷。
5.解题案例：抽象代数与质数判定
案例一：抽象代数中的群作用性质证明
题目描述 (nl_problem)
Prove that for a group acting on a set , , the function "fixingSubgroup" is antitone.
本方案执行过程与优势
（1）半形式化与自形式化：系统首先正确理解了 "antitone" 的数学含义，将其转化为蕴含关系S ⊆ T → fixingSubgroup M T ≤ fixingSubgroup M S，生成了准确的形式化命题。
（2）级联递归证明：
·在使用固定启发式策略和开源模型生成失败后，系统进而采用DSP-Prover方案进行证明。
·通用模型负责生成 Proof Sketch，它利用强大的逻辑推理能力，构建了关键的中间结论，弥补了形式化专用证明器在数学推理能力上的不足。
·专家模型负责填充 Proof Gap，即代码中的具体证明细节，完成证明。
案例二：大数质数判定
题目描述 (nl_problem)
请问 40723824643 是质数吗？
本方案执行过程与优势
（1）半形式化 (Semi-formalization) 阶段的求解先验：
·本方案在生成形式化命题前，首先调用通用推理模型进行“自然语言求解”。模型识别出该数较大，通过内部工具调用 (Function Call)，判定该数不是质数。
·基于这一先验解，半形式化模块构建了正确的自然语言命题 (Informal Statement)："Prove that 40723824643 is not a prime number."
（2）形式化与证明：
·自形式化模块将其翻译为正确的 Lean 命题：¬ Nat.Prime 40723824643。
·由于命题方向正确，后续采用固定启发式策略 (Heuristic Tactics) 即可轻松完成证明。
以上两案例代码详见链接：
https://mp.weixin.qq.com/s/Ohf18QqzZmI2AmHj3hd1oA
6.挑战与展望：大语言模型的泛化性难题
尽管已经取得了显著成果，该团队也指出了当前系统存在的局限性：
（1）证明模型的泛化瓶颈。本方案高度依赖定理证明专家模型 (Goedel-Prover-V2-8B) 进行证明。但现有的开源模型在包含新定义的上下文以及代数、程序等高中数学之外的领域上泛化性较弱。
（2）非形式化到形式化的语义鸿沟。由于代数等领域在形式化与非形式化推理上有较大的差异，通用大模型的推理过程常常无法准确地转化为证明骨干，证明修复也时常难以修正所有问题。
展望未来，该团队将致力于提升形式化大模型在本科及研究生级别数学领域、Mathlib以外的形式化库、以及其他数学任务上的泛化能力。
7.团队成员介绍
刘祺： 上海创智学院/上海交通大学计算机学院硕博连读生。在NeurIPS 2025、ICLR 2025等发表第一作者论文。主要研究方向为大模型与形式化、定理证明与问题求解。
鲍康捷： 上海交通大学数学科学学院吴文俊班大四本科生，本科期间曾获多项校级奖学金，未来将在上海创智学院/上海交通大学攻读博士，主要研究方向为形式化推理与证明。
邱博林： 上海交通大学计算机学院信息安全大四本科生，人工智能学院已录取直博生，本科期间曾获国家奖学金等多项荣誉，主要研究大模型的数学推理和形式化与自动定理证明。
郑心浩： 上海创智学院/上海交通大学计算机学院硕博连读生。在NeurIPS 2024、2025等发表多篇第一作者论文。主要研究方向为形式化、密码分析的人工智能方法。
严骏驰： 指导教师，上海创智学院全时导师、上海交通大学人工智能学院、计算机学院教授。承担科技部、基金委、教育部多个研究项目。主要研究方向为机器学习与交叉应用。
