大规模形式化数学基准FormalMATH发布，最强模型成功率仅16%

FormalMATH团队 投稿
量子位 | 公众号 QbitAI

最强AI模型面对5560道数学难题，成功率仅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倍。

构建创新：人类在循环中的自动化流程用于自动形式化和语义一致性检测

为解决传统形式化数据依赖专家手动标注的瓶颈，研究团队提出了一套「三阶段过滤」框架：

1. 多LLM协同翻译 ：通过微调后的Qwen2.5-7B-Coder、Deepseek-Prover-V1.5-Base等模型将自然语言问题转为多个候选的形式化命题；
2. 自动化验证 ：利用Lean4编译器筛选语法正确命题，并通过多LLM语义一致性校验（如o1-mini、Claude-3.5）过滤错误；
3. 否定反证过滤 ：调用LLM证明器尝试「证伪」命题，排除无法成立的陈述。该流程在人工审核前保留了72.09%的高质量命题，大幅降低专家工作量。

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

现有LLM证明器表现：代数尚可，微积分「翻车」

整体低迷：16%成功率暴露能力断层

在FormalMATH全量数据集上，主流LLM证明器的表现远低于预期：

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

领域偏见：代数强，微积分弱

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

错误模式：滥用「捷径战术」

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

1. 冗余假设（34%）： 引入无关前提条件
2. 不完整证明（62%）： 缺失关键推导步骤, 无法形成完整构造证明
3. 自动化策略误用 （65.0%）：错误调用自动化工具（如用integral_mono_on跳过控制收敛定理验证）
4. 无法正确应对不等式 （13.0%）：错误地（例如在指数爆炸的情况）过度依赖linarith或者nlinarith等自动化不等式计算策略

突破方向：让LLM学会「严谨思考」

技术瓶颈：自然语言引导反拖后腿

研究团队发现一个反直觉现象：在链式思维（CoT）场景中，提供自然语言解题思路反而会降低证明成功率。

例如，DeepSeek-V1.5-RL模型在普通的CoT提示时表现优于引入人为自然语言引导的情况。

未来路径：从「战术依赖」到「战略规划」

未来，提升LLM形式化推理能力需从三方面突破：

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

开源开放：数据、代码与模型已全面公开

研究团队呼吁学术界与工业界共同推进形式化数学推理技术的发展，助力AI在数学发现、形式化验证等领域实现更可靠的应用。

FormalMATH基准测试的代码、训练数据及评估模型已向公众开放：

论文链接 ：
https://arxiv.org/pdf/2505.02735
项目仓库 ：
https://github.com/Sphere-AI-Lab/FormalMATH-Bench
基准数据集 ：
https://huggingface.co/SphereLab

— 完 —