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倍。
构建创新：人类在循环中的自动化流程用于自动形式化和语义一致性检测
为解决传统形式化数据依赖专家手动标注的瓶颈，研究团队提出了一套「三阶段过滤」框架：
-
多LLM协同翻译 ：通过微调后的Qwen2.5-7B-Coder、Deepseek-Prover-V1.5-Base等模型将自然语言问题转为多个候选的形式化命题； -
自动化验证 ：利用Lean4编译器筛选语法正确命题，并通过多LLM语义一致性校验（如o1-mini、Claude-3.5）过滤错误； -
否定反证过滤 ：调用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为例）：
-
冗余假设（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基准测试的代码、训练数据及评估模型已向公众开放：
论文链接 ：
https://arxiv.org/pdf/2505.02735
项目仓库 ：
https://github.com/Sphere-AI-Lab/FormalMATH-Bench
基准数据集 ：
https://huggingface.co/SphereLab
一键三连「点赞」「转发」「小心心」
欢迎在评论区留下你的想法！
— 完 —
学术投稿请于工作日发邮件到：
ai@qbitai.com
标题注明【投稿】，告诉我们：
你是谁，从哪来，投稿内容
附上论文/项目主页链接，以及联系方式哦
我们会（尽量）及时回复你
🌟 点亮星标 🌟
（文：量子位）