大语言模型离“数学证明高手”还有多远？斯坦福、伯克利、MIT 团队提出 IneqMath 评测标准

91 0 0

文章摘要

大语言模型（LLM）在生成看似正确的结论时，往往缺乏严谨的推理过程，尤其是在数学证明领域。不等式问题因其结构简单、逻辑清晰，成为检验模型推理能力的理想工具。形式化数学系统如 Lean 和 Coq 能够无差错地验证证明过程，但其高门槛和低自动化限制了广泛应用。相比之下，大语言模型在自然语言环境下进行“非正式推理”表现较好，但如何验证其推理过程的严谨性仍是一个挑战。

斯坦福、伯克利和 MIT 的研究团队提出了一种新方法，将不等式证明拆分为两个自然语言任务——“界限估计”和“关系预测”，并构建了名为 IneqMath 的数据集。该数据集包含 1,252 道训练题和 200 道由国际数学奥林匹克金牌选手标注的测试题，旨在通过自然语言环境逐步验证模型的推理过程。这一方法在自然语言和形式化逻辑之间搭建了一座“中间桥梁”，使得模型能够在保留数学题目可证明性的同时，避免复杂的形式化要求。

为了评估模型的推理过程，研究团队设计了一套“AI 数学裁判系统”，该系统从四个角度自动评估推理步骤的严谨性：特殊值推断、逻辑偏差、不当近似和数值错误。该系统的准确率高达 F1 = 0.93，与人类专家的判断一致性非常高，能够可靠地替代大量人工审卷工作。

研究发现，尽管大语言模型在给出正确答案方面表现不错，但其推理过程往往经不起推敲。以 Grok 3 mini 为例，虽然其答案准确率为 71.5%，但仅有 6% 的答案过程合理、逻辑严谨。这表明许多模型虽然能“猜”到答案，但推理过程存在跳步、代值或模糊解释等问题。此外，模型规模的增加并不一定带来推理严谨性的提升，推理长度的增加也未能显著提高推理质量。

研究团队提出了两个有效的方法来提升模型的推理能力：自我批判和定理提示。自我批判让模型先审阅自己的答案再进行修改，而定理提示则通过提前提供相关定理来帮助模型更好地处理复杂问题。这些方法表明，仅靠增加算力并不能提升推理严谨性，教会模型“自我反思”和“使用工具”才是关键。

IneqMath 的目标不是证明模型不行，而是帮助它们逐步学会如何进行严谨的推理，最终成为真正会“证明”的数学 AI。尽管目前大模型还只是“猜得好”，但未来它们有可能真正“想得明白”。