FormalMATH助力数学推理：AI模型结合链式思维与自然语言处理，挑战形式化数学基准新高度

（由多段落组成）

挑战AI数学推理的极限！FormalMATH大规模形式化数学基准测试正式发布，最强模型的成功率仅为16.46%。这一结果揭示了当前人工智能在数学推理领域的局限性。

香港中文大学、西湖大学、MAP、浙江大学、马克斯·普朗克智能系统研究所等多家机构联合推出了名为FormalMATH的形式化数学推理基准测试。该测试包含5560道经过严格验证的数学题目，涵盖了从奥数到大学水平的多个领域，如代数、微积分和数论等。

形式化数学推理被认为是人工智能领域中的核心难题之一。尽管大语言模型（LLM）在自然语言处理和代码生成等领域取得了显著进展，但在需要严格逻辑推导的数学定理证明任务中，其能力仍然面临严峻挑战。FormalMATH基准测试首次系统地评估了当前基于LLM的定理证明器的实际水平。结果显示，即使是表现最佳的模型Kimina-Prover，在实际计算资源限制下（Pass@32采样量），成功率也仅为16.46%，而大多数模型在微积分等领域的表现接近“随机猜测”。

FormalMATH：“超大规模”的形式化数学推理基准
规模突破：比现有基准高出22.8倍
FormalMATH包含5560个经Lean4编译器验证的数学命题，涵盖代数、数论、微积分、离散数学等12个子领域，问题难度从国际数学奥林匹克（IMO）竞赛级延伸至本科课程，规模是经典基准MiniF2F的22.8倍。

构建创新：通过自动化流程实现高效数据生成
为解决传统形式化数据依赖专家手动标注的问题，研究团队提出了一套“三阶段过滤”框架：

– 多LLM协同翻译：通过微调后的Qwen2.5-7B-Coder、Deepseek-Prover-V1.5-Base等模型将自然语言问题转化为多个候选的形式化命题；
– 自动化验证：利用Lean4编译器筛选语法正确的命题，并通过多LLM语义一致性校验（如o1-mini、Claude-3.5）过滤错误；
– 否定反证过滤：调用LLM证明器尝试“证伪”命题，排除无法成立的陈述。

最后，团队召集了12名具有奥赛金牌级别的专家花了22天检测自然语言数学命题与Lean4形式化命题之间的语义一致性。

现有LLM证明器的表现：代数尚可，微积分表现不佳
整体低迷：16%的成功率暴露能力断层
在FormalMATH全量数据集上，主流LLM证明器的表现远低于预期：

– 最佳模型Kimina-Prover（Pass@32）：16.46%；
– 次优模型STP（Pass@32）：13.87%

领域偏见：代数强，微积分弱
现有模型在代数等领域表现较好，但在微积分等其他领域表现较差，显示出明显的领域偏差。

错误模式：滥用“捷径战术”
分析显示，LLM证明器频繁滥用自动化策略（如aesop、linarith），试图用单一步骤替代多步推理，导致以下典型错误（以DeepSeek-RL为例）：

– 冗余假设（34%）：引入无关前提条件；
– 不完整证明（62%）：缺失关键推导步骤，无法形成完整构造证明；
– 自动化策略误用（65.0%）：错误调用自动化工具（如用integral_mono_on跳过控制收敛定理验证）；
– 无法正确应对不等式（13.0%）：错误地过度依赖linarith或者nlinarith等自动化不等式计算策略。

突破方向：让LLM学会“严谨思考”
技术瓶颈：自然语言引导反而拖后腿
研究团队发现一个反直觉现象：在链式思维（CoT）场景中，提供自然语言解题思路反而会降低证明成功率。例如，DeepSeek-V1.5-RL模型在普通的CoT提示时表现优于引入人为自然语言引导的情况。

未来路径：从“战术依赖”到“战略规划”
未来，提升LLM形式化推理能力需从以下三方面突破：

– 强化多步规划：减少对aesop等单步战术的依赖，设计分层推理架构；
– 跨领域泛化：通过课程学习（Curriculum Learning）平衡代数/微积分等领域的训练数据；
– 人机协同验证：开发交互式证明辅助工具，让LLM与人类专家协同完成复杂定理证明。

开源开放：数据、代码与模型已全面公开
研究团队呼吁学术界与工业界共同推进形式化数学推理技术的发展，助力AI在数学发现、形式化验证等领域实现更可靠的应用。FormalMATH基准测试的代码、训练数据及评估模型已向公众开放。

本文来源：