数学证明不仅要得出正确的结果，还需要有严密的逻辑推理过程。尤其是在处理不等式问题时，这一点尤为重要。即使最终答案正确，只要中间某个步骤出错，整个证明就可能失效。这让人不禁思考：这些答案是模型通过严谨的推理得来的，还是只是通过“看起来合理”的方式推测出来的？不等式问题正好可以用来检验这一点，因为它们结构清晰、逻辑简单，广泛存在于数学竞赛和实际应用中，同时需要较长的推理链条，能够暴露推理中的漏洞。

目前的形式化数学系统，如 Lean 和 Coq，提供了严格的验证机制，每一步推导都必须符合逻辑规则，并且能被计算机检查。但这类系统对语言表达的要求非常高，建模成本大，自动化程度有限，尤其在中学或奥数级别的不等式问题上，难以大规模使用。

相比之下，当前主流的大语言模型虽然不能生成可被形式系统接受的证明，但在非形式化推理方面表现不错。它们通常能给出合理的答案，模仿人类早期解决问题的思维方式。这种能力虽然不符合传统形式证明的标准，但在探索性数学研究中有一定价值。

为了解决这个问题，斯坦福大学、加州大学伯克利分校和麻省理工学院的研究团队提出了一种新方法。他们将不等式证明任务拆分为两个子任务：界限估计和关系预测。基于此，他们创建了首个奥林匹克级别的不等式证明数据集 IneqMath。这个框架介于完全形式化验证与自然语言生成之间，能够逐步审查模型的推理过程，判断其是否真正理解了推理结构，而不仅仅是猜测答案。

IneqMath 包含训练集、测试集和验证集。训练集包含 1,252 道题目，配有分步证明和定理标签。测试集由国际数学奥林匹克奖牌得主设计，经过专家审核，强调复杂策略和逻辑深度。验证集用于调参和中期评估。

为了评估模型的推理能力，研究团队开发了一套自动评审系统，包括五种评审器：判断最终答案是否正确、是否用特殊值推断一般结论、是否存在逻辑跳步、是否有不当近似、计算是否准确。这套系统与人工标注高度一致，表现出良好的可靠性。

实验结果显示，许多主流模型虽然最终答案准确率高，但经过逐步评审后准确率大幅下降。这说明当前模型存在“猜得准但推不全”的问题。此外，模型规模并不一定带来更好的推理能力，增加推理时间也未显著提升推理质量。

不过，一些改进方法显示出潜力。例如，自我批判和定理提示可以提高模型的表现。研究团队还设立了排行榜，鼓励社区参与测试模型在 IneqMath 上的表现。

尽管目前模型在逻辑严谨性上仍有不足，但通过工具使用和自我反思，它们开始展现出学习推理的可能性。未来，真正的数学 AI 不一定更大，但一定会更善于利用工具和自我修正。现在，大模型是优秀的猜测者，但还不是可靠的证明者。IneqMath 的目标是推动它们成为真正具备数学思维的系统。