2025年5月7日，由香港中文大学、西湖大学、MAP、浙江大学以及德国马克斯·普朗克智能系统研究所联合研发的FormalMATH形式化数学推理基准测试正式发布。这一包含5560道严格验证数学题的超大规模基准，覆盖从奥数到大学水平的代数、微积分、数论等12个领域，旨在系统评估大型语言模型（LLM）在数学定理证明中的真实能力。测试结果令人震惊：即使是最先进的模型Kimina-Prover，在实际计算资源限制下（Pass@32采样量），成功率也仅为16.46%。这一结果揭示了AI在复杂数学推理领域的巨大瓶颈。
FormalMATH：重新定义数学推理基准
FormalMATH是目前规模最大的形式化数学推理基准，包含5560道全新命题，规模是经典基准MiniF2F的22.8倍。问题由60多位顶尖数学家（包括国际数学奥林匹克题作者和菲尔茨奖得主）精心设计，涵盖代数、数论、微积分、离散数学等，难度从竞赛级到本科课程级。所有命题均通过Lean4编译器验证，确保语义正确，杜绝数据污染风险。
为突破传统形式化数据依赖专家手动标注的瓶颈，研究团队创新提出“三阶段过滤”框架：
-
多LLM协同翻译：利用Qwen2.5-7B-Coder、Deepseek-Prover-V1.5-Base等模型，将自然语言问题转化为形式化命题。
-
自动化验证：通过Lean4编译器筛选语法正确命题，并结合o1-mini、Claude-3.5等模型进行语义一致性校验。
-
否定反证过滤：调用LLM证明器尝试“证伪”命题，排除无效陈述。
这一流程保留了72.09%的高质量命题，大幅降低人工审核负担。最终，12名奥赛金牌级专家耗时22天，逐一核查自然语言与形式化命题的语义一致性。
AI表现低迷：代数尚可，微积分“翻车”
FormalMATH测试结果暴露了当前LLM证明器的严重短板：
-
整体成功率低：最佳模型Kimina-Prover仅达16.46%，次优模型STP为13.87%，多数模型在微积分等领域的表现接近随机猜测。
-
领域偏差明显：模型在代数领域表现较好，但在微积分、分析等领域严重不足，凸显跨领域泛化能力的欠缺。
-
错误模式频发：以DeepSeek-RL为例，62%的错误源于不完整证明，65%涉及滥用自动化工具（如aesop、linarith），34%引入冗余假设，13%无法正确处理不等式。
研究团队发现，LLM证明器倾向于依赖单步“捷径战术”，如自动化策略，而非严谨的多步推理。例如，模型可能错误调用integral_mono_on跳过收敛验证，或在指数爆炸场景中过度依赖linarith，导致推理失败。
技术瓶颈与未来突破
研究揭示了一个反直觉现象：链式思维（CoT）中引入自然语言解题思路，反而降低证明成功率。例如，DeepSeek-V1.5-RL在普通CoT提示下的表现优于人为引导场景。这表明，当前LLM在处理自然语言引导时，可能因语义干扰而偏离严谨逻辑。
研究团队提出未来突破方向：
-
强化多步规划：设计分层推理架构，减少对单步战术的依赖。
-
跨领域泛化：通过课程学习平衡代数、微积分等领域的训练数据。
-
人机协同：开发交互式证明工具，让LLM与人类专家协同攻克复杂定理。
香港中文大学研究员、项目共同负责人周亮（@ZhouliangY）在X平台上表示：“Regretfully, if check the results on FormalMATH instead of MiniF2F, we know that”现有模型在复杂数学推理中的表现远未达预期，亟需技术革新。
开源共享，助力AI数学革命
FormalMATH的代码、训练数据和评估模型已全面开源，研究团队呼吁全球学术界与工业界共同推动形式化数学推理技术发展。相关资源可通过以下渠道获取：
-
论文：https://arxiv.org/pdf/2505.02735
-
项目仓库：https://github.com/Sphere-AI-Lab/FormalMATH-Bench
-
数据集：https://huggingface.co/SphereLab
FormalMATH不仅揭示了AI在数学推理领域的现状，也为未来发展指明了方向。正如周亮所言，AI若想在数学发现和形式化验证中发挥更大作用，必须学会“严谨思考”。这一基准的发布，标志着AI数学推理研究迈向新阶段。
