共计 847 个字符，预计需要花费 3 分钟才能阅读完成。
最强 AI 模型面对 5560 道数学难题，成功率竟然只有 16.46%？这背后究竟隐藏着什么秘密呢？
最近，香港中文大学、西湖大学、MAP、浙江大学以及马克斯·普朗克智能系统研究所等多家机构联手推出了名为 FormalMATH 的形式化数学推理基准测试。这个测试包含了 5560 道经过严格验证的数学题目，涵盖了从小学到大学的各种难度级别，包括代数、微积分、数论等多个领域。
形式化数学推理的挑战
形式化数学推理被认为是人工智能领域的一大难点。虽然大型语言模型（LLM）在处理自然语言和编写代码方面取得了显著进步，但在需要严密逻辑推导的数学定理证明任务上依然存在诸多不足。
FormalMATH 首次系统性地评估了基于 LLM 的定理证明器的实际表现。结果表明，即便是性能最好的模型 Kimina-Prover，在有限计算资源条件下（Pass@32 采样量），其成功率也只有 16.46%；而大多数模型在微积分等领域的成绩接近随机猜测。
FormalMATH 的独特之处
FormalMATH 不仅规模庞大——比现有的经典基准 MiniF2F 大 22.8 倍，还覆盖了 12 个不同的数学子领域，从国际数学奥林匹克竞赛级的问题一直到本科课程的内容。
为了克服传统形式化数据依赖人工标注的问题，研究人员设计了一个三阶段过滤框架，利用多个 LLM 来自动转换自然语言问题为形式化命题，并通过 Lean4 编译器进行语法检查及语义一致性校验。最终，在无需过多人工干预的情况下，保留了 72.09% 的高质量命题。
各领域表现差异明显
尽管整体成功率不高，但不同领域的具体表现却有所不同。比如，在代数方面，现有模型还能勉强应付；然而到了微积分这类复杂的数学分支，则显得力不从心。此外，许多模型倾向于使用一些简化的‘捷径’方法来解决问题，这往往会导致遗漏重要的推理步骤或引入不必要的假设。
未来发展的方向
要想提高 LLM 在这方面的表现，未来的研究需要着重于加强多步推理能力、实现跨学科的知识迁移以及促进人机协作。同时，还需要重新审视如何有效地指导这些模型去进行更加严谨的思考过程。
