挑战AI数学推理极限！大规模形式化数学基准FormalMATH发布，最强模型成功率仅16%
最强 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
标题注明【投稿】，告诉我们：
你是谁，从哪来，投稿内容
附上论文 / 项目主页链接，以及联系方式哦
我们会（尽量）及时回复你
点亮星标
科技前沿进展每日见