大语言模型与数学推理：挑战与进展

如今，大型语言模型（LLM）尽管能给出看似合理的结论，但其推理过程却常令人质疑。这些模型是否真正理解推理，抑或只是表面上的“猜测”？

不等式问题成为检验模型“真会证明”的理想测试——结构简洁、逻辑清晰，且易暴露推理漏洞。它们如同AI数学推理能力的“试金石”。

探究这些挑战的核心，即形式化数学努力验证推理的严谨性。如Lean、Coq等系统虽能无误验证，但要求极高，且自动化低，难以处理复杂问题。

反观大语言模型，虽直接生成可验证证明的能力不强，但在“非正式推理”中表现不错。探索其在自然语言环境下进行不等式证明的能力，既有趣又具研究价值。

项目主页：https://ineqmath.github.io

论文：https://arxiv.org/abs/2506.07927

代码库：https://github.com/lupantech/ineqmath

数据集：https://huggingface.co/datasets/AI4Math/IneqMath

排行榜：https://huggingface.co/spaces/AI4Math/IneqMath-Leaderboard

评估“非正式”方法的证明

研究团队将不等式问题拆分为两个可验证的小任务：“界限估计”和“关系预测”。这种方法既保留了数学题目的可证明性，又简化了过程。

Bound Estimation（估计上下限）

对于任意实数a，b，请判断a²+b²与2ab的关系。

Relation Prediction（关系预测）

对于任意实数a，b，请求出最大的常数C使得a²+b²≥Cab恒成立。

这两类任务可直接用自然语言+LaTeX表达，大模型也能按步骤解题，验证方便。

IneqMath：首个“自然语言但可验证”的不等式数据集

研究团队构建了IneqMath数据集，包含1,252道题目作为训练集，每道题目均有详细解答和定理标注。此外，还有国际数学奥林匹克金牌选手标注的200道测试题和100道验证题。

模型推理的可靠性评估

研究团队设计了“AI数学裁判系统”，不仅能判断答案是否正确，还能从四个角度评估推理步骤的合理性。

• Toy Case Judge：判断特殊值是否推断出一般结论。
• Logical Gap Judge：检测跳步和未解释等价变形。
• Numerical Approximation Judge：判断不当近似。
• Numerical Computation Judge：检查计算错误。

准确率高达F1=0.93，人类面临下岗？

这些自动评审器与人类专家的一致性很高，F1值达0.93。它们已能可靠替代大量人工审卷工作。

关键发现

“答案准”≠“推得对”

大模型能给出正确答案，但过程常经不起推敲。以Grok 3 mini为例，其答案正确率为71.5%，但经评审后只有6%的过程合理、逻辑严谨。

模型大了，推理就更好吗？不一定！

研究发现，大模型更擅长“猜答案”，但深入评估推理过程时，“变强”趋势停止。增加参数和硬件无法提升推理严谨性。

想得多，不代表想得对

增加模型生成内容并未显著提升推理质量。关键还是答到点子上。

两个有效办法

自我批判（Self-Critique）

让模型自我审查后改进答案。这招使Gemini 2.5 Pro的准确率提升约5%。

定理提示（Theorem as Hints）

提前给模型相关定理提示，准确率最多提升10%，对复杂题特别有帮助。

结语

当前大模型擅长猜测，但严格推理仍不足。IneqMath旨在帮助模型逐步学会如何推理，成为真正会“证明”的数学AI。