AI哪怕答案正确，逻辑链却惨不忍睹，奥数级不等式证明成功率不到50%
这不是段子，而是正在发生的现象。
大语言模型解决不等式证明问题时，可以给出正确答案，但大多数时候是靠猜。推理过程经不起推敲，逻辑完全崩溃。
斯坦福大学、UC伯克利、MIT等机构联合发布研究论文《Solving Inequality Proofs with Large Language Models》，首次系统评估了29个顶级大模型在奥数级不等式证明任务上的能力。
他们系统的研究了大语言模型解决不等式证明的能力，并构建了全新数据集IneqMath以及能力超群的“LLM as Judge”评估体系。
看起来像解出来了，其实全是错的
对于这道题目，GPT-4.1给出的证明如下：
它的确是得到了正确的左边的式子小于右边的式子，但是正确的结论是通过代入特殊值a=b=c=1和a=1, b=4, c=16的方法得到的，这种方法显然是不严谨的。
在观察到“答案正确但推理过程错误”这一普遍现象后，研究团队决定深入探究大语言模型在不等式证明这一典型任务中的真实推理能力。
然而，传统的不等式证明既难以自动验证，又常依赖高度形式化的语言（如 Lean、Coq），这类系统虽然逻辑严密，却表达繁琐、建模成本高，难以适应奥数级问题的规模化分析。同时，它们与人类自然的推理过程存在较大距离。
△使用Lean进行形式化证明的过程
鉴于此，团队开发了一个自然语言表达、但可自动验证的新型不等式任务数据集IneqMath。该数据集将复杂的不等式证明过程拆解为两个子任务：Bound Estimation（界限估计）和Relation Prediction（关系判断）。
通过这一任务设计，IneqMath在保留数学推理核心挑战的同时，构建出一个介于形式化证明与人类非形式直觉之间的中间状态——即用自然语言保证了和人类直觉的统一，又能确保结果的可验证性。
此外，团队还设计了一套LLM-as-Judge评估系统，用多个专门判分器对模型的推理过程进行逐步审查，实现了从最终答案到每一步推理的自动化评分与细粒度诊断，补足传统“只看结论”的评估盲点。
以下是IneqMath的Bound Estimation（界限估计）和 Relation Prediction（关系判断）两种题目的示例：
△
△
△
△
另外可访问研究团队的可视化工具查看IneqMath的所有题目（链接在文末获取）。
LLM作为Judge，是如何运作的？
团队开发的LLM-as-Judge框架由五种“自动评审器”组成，可以逐步分析语言模型的解题过程是否符合逻辑严谨性，分别是：
评价最终答案是否正确的 Final Answer Judge
判断是否用特殊值推断出一般的结论的 Toy Case Judge
评价是否存在跳步、未解释的等价变形等逻辑偏差的 Logical Gap Judge
判断是否存在不当近似的 Numerical Approximation Judge
判断是否存在不正确计算的 Numerical Computation Judge 通过这套系统，研究者可以判断一个模型是否只是“碰巧答对了”，还是 在每一个推理节点上都做对了。
这五种评审器从不同的维度全面地评价模型的作答能力。但是他们每一个是如何工作的呢？
以Final Answer Judge为例，一道题目是需要判断在一定的约束条件下，的最小上界是多少。模型给出的回答如下所示：
可以看出，该模型在解题过程中通过代入特殊值，并依据代入后表达式的大小关系来推断表达式的最小上界。这显然是一种由特殊值推断一般结论的推理方式。对此，Toy Case Judge 分析了模型结果中使用特殊值进行推断的情况，准确定位了问题所在，并最终给出了判断结果 False，说明该结论是基于特殊值推断得出的，因而不具有普遍性，应被视为不正确。
其他评审器的工作原理与示意评审器类似。只有当模型的回答通过了所有评审器的验证，才能认为其逻辑推理是完全正确的。
实验结果揭示LLM推理的“真面目”
真相1：推理过程的“可信度错觉”——Soundness Gap并非幻觉！
在对29个当前主流大模型的系统性测试中（覆盖 GPT-4、Claude、Grok、Llama、Gemini 等），研究人员发现模型们表面看似聪明，实际推理却漏洞百出：
- Grok 3 mini
最终答案准确率高达 71.5% ，但在每步逻辑被“逐项打分”后，严谨推理得分仅剩6.0%
模型的步骤准确率在最多下滑了 65.5个百分点
即使是被认为擅长“逻辑推理”的开源 Reasoning LLMs，也鲜有突破6%严谨度的
通用聊天类模型的推理表现更惨淡，大多数连5%都难以达到 因此可以得出，当前LLM的“答案看起来对”更多是侥幸匹配，而非真正构建出了可信的推理链条。
真相2：参数更大≠推理更聪明
虽然更大的模型在选择正确答案这方面确实更稳定、更强了，但当检查推理链条是否“合逻辑”，结果却是：几乎没有改进。
也就是说：
参数提升 →
猜对的频率高了 - 但逻辑验证 →
步骤还是错的，没变聪明！ 这说明“变大”不等于“会思考”，构建严谨推理过程并不是靠堆叠模型规模就能实现的。
真相3：“多思考”不等于“更严谨”
研究人员还尝试让模型思考更久——具体方法是，允许模型生成更长的推理路径（增加推理token上限）。但最终观察到的是：
推理更长，并未带来质的飞跃。
即使reasoning chain延展了好几倍，逻辑准确率依然停留在原地徘徊，甚至出现“逻辑越写越错”的情况。
希望之光：两种机制显著改善推理质量
尽管整体结果表明大模型距离真正的逻辑证明还有明显差距，但研究也找到了两个真正有效的优化策略：
策略一：自我反思反馈机制（Self-improvement via Critic as Feedback）
让模型在解完题后反过来“自己打分、自己挑错”，再进行修改。
该方法在 Gemini 2.5 Pro 上带来了 约5%的推理质量提升 - 模型开始避免常见跳步、数值错用等问题
策略二：引入“定理线索”（Theorem Hints）辅助模型思考
研究者为模型提前准备关键定理（如 AM-GM、Cauchy-Schwarz），并嵌入到提示中，让模型像人一样“借助工具”进行证明。
Gemini 2.5 Pro 的准确率在此策略下提升 近10% - 解决了许多模型“不知道该套哪个定理”的盲区问题
加入IneqMath挑战榜，展示你的模型推理实力
为推动大语言模型在严谨数学推理方面的进展，团队构建了一个持续更新的IneqMath 评测排行榜，面向全球开放提交。无论你是在调试轻量模型，还是优化顶级推理模型，都可以将其性能提交至平台进行自动评估。
排行榜系统依托研究团队提出的LLM-as-Judge自动评分框架，可无人工干预地评估模型在最终答案正确率与推理过程完整性两方面的表现，确保高效且公正的比对。
欢迎各类模型参与测试——从主流大型模型到精心调校的实验性模型，皆可在此一展风采。
提交你的模型，看看它能否登上“推理力”榜单的高峰～
挑战页面：https://huggingface.co/spaces/AI4Math/IneqMath-Leaderboard
项目主页：ineqmath.github.io
论文：https://arxiv.org/abs/2506.07927IneqMath
数据集： https://huggingface.co/datasets/AI4Math/IneqMath
开源代码： https://github.com/lupantech/ineqmath
本文来自微信公众号“量子位”，作者：IneqMath团队，36氪经授权发布。
