這不是段子，而是正在發(fā)生的現(xiàn)象。

大語言模型解決不等式證明問題時，可以給出正確答案，但大多數(shù)時候是靠猜。推理過程經不起推敲，邏輯完全崩潰。

斯坦福大學、UC伯克利、MIT等機構聯(lián)合發(fā)布研究論文《Solving Inequality Proofs with Large Language Models》，首次系統(tǒng)評估了29個頂級大模型在奧數(shù)級不等式證明任務上的能力。

他們系統(tǒng)的研究了大語言模型解決不等式證明的能力，并構建了全新數(shù)據(jù)集IneqMath以及能力超群的“LLM as Judge”評估體系。

看起來像解出來了，其實全是錯的

對于這道題目，GPT-4.1給出的證明如下：

它的確是得到了正確的左邊的式子小于右邊的式子，但是正確的結論是通過代入特殊值a=b=c=1和a=1, b=4, c=16的方法得到的，這種方法顯然是不嚴謹?shù)摹?/span>

在觀察到“答案正確但推理過程錯誤”這一普遍現(xiàn)象后，研究團隊決定深入探究大語言模型在不等式證明這一典型任務中的真實推理能力。

然而，傳統(tǒng)的不等式證明既難以自動驗證，又常依賴高度形式化的語言（如 Lean、Coq），這類系統(tǒng)雖然邏輯嚴密，卻表達繁瑣、建模成本高，難以適應奧數(shù)級問題的規(guī)?；治觥Ｍ瑫r，它們與人類自然的推理過程存在較大距離。

△使用Lean進行形式化證明的過程

鑒于此，團隊開發(fā)了一個自然語言表達、但可自動驗證的新型不等式任務數(shù)據(jù)集IneqMath。該數(shù)據(jù)集將復雜的不等式證明過程拆解為兩個子任務：Bound Estimation（界限估計）和Relation Prediction（關系判斷）。

通過這一任務設計，IneqMath在保留數(shù)學推理核心挑戰(zhàn)的同時，構建出一個介于形式化證明與人類非形式直覺之間的中間狀態(tài)——即用自然語言保證了和人類直覺的統(tǒng)一，又能確保結果的可驗證性。

此外，團隊還設計了一套LLM-as-Judge評估系統(tǒng)，用多個專門判分器對模型的推理過程進行逐步審查，實現(xiàn)了從最終答案到每一步推理的自動化評分與細粒度診斷，補足傳統(tǒng)“只看結論”的評估盲點。

以下是IneqMath的Bound Estimation（界限估計）和 Relation Prediction（關系判斷）兩種題目的示例：

△Bound Estimation（界限估計）訓練集題目示例

△Relation Estimation（關系判斷）訓練集題目示例

△Bound Estimation（界限估計）測試集題目示例

△Relation Estimation（關系判斷）測試集題目示例

另外可訪問研究團隊的可視化工具查看IneqMath的所有題目（鏈接在文末獲?。?。

LLM作為Judge，是如何運作的？

團隊開發(fā)的LLM-as-Judge框架由五種“自動評審器”組成，可以逐步分析語言模型的解題過程是否符合邏輯嚴謹性，分別是：

• 評價最終答案是否正確的Final Answer Judge
• 判斷是否用特殊值推斷出一般的結論的Toy Case Judge
• 評價是否存在跳步、未解釋的等價變形等邏輯偏差的Logical Gap Judge
• 判斷是否存在不當近似的Numerical Approximation Judge
• 判斷是否存在不正確計算的Numerical Computation Judge通過這套系統(tǒng)，研究者可以判斷一個模型是否只是“碰巧答對了”，還是在每一個推理節(jié)點上都做對了。

這五種評審器從不同的維度全面地評價模型的作答能力。但是他們每一個是如何工作的呢？

以Final Answer Judge為例，一道題目是需要判斷在一定的約束條件下，的最小上界是多少。模型給出的回答如下所示：

可以看出，該模型在解題過程中通過代入特殊值，并依據(jù)代入后表達式的大小關系來推斷表達式的最小上界。這顯然是一種由特殊值推斷一般結論的推理方式。對此，Toy Case Judge 分析了模型結果中使用特殊值進行推斷的情況，準確定位了問題所在，并最終給出了判斷結果 False，說明該結論是基于特殊值推斷得出的，因而不具有普遍性，應被視為不正確。

其他評審器的工作原理與示意評審器類似。只有當模型的回答通過了所有評審器的驗證，才能認為其邏輯推理是完全正確的。

實驗結果揭示LLM推理的“真面目”

真相1：推理過程的“可信度錯覺”——Soundness Gap并非幻覺！

在對29個當前主流大模型的系統(tǒng)性測試中（覆蓋 GPT-4、Claude、Grok、Llama、Gemini 等），研究人員發(fā)現(xiàn)模型們表面看似聰明，實際推理卻漏洞百出：

• Grok 3 mini最終答案準確率高達71.5%，但在每步邏輯被“逐項打分”后，嚴謹推理得分僅剩6.0%
• 模型的步驟準確率在最多下滑了65.5個百分點
• 即使是被認為擅長“邏輯推理”的開源 Reasoning LLMs，也鮮有突破6%嚴謹度的
• 通用聊天類模型的推理表現(xiàn)更慘淡，大多數(shù)連5%都難以達到因此可以得出，當前LLM的“答案看起來對”更多是僥幸匹配，而非真正構建出了可信的推理鏈條。
  
  
  

真相2：參數(shù)更大≠推理更聰明

雖然更大的模型在選擇正確答案這方面確實更穩(wěn)定、更強了，但當檢查推理鏈條是否“合邏輯”，結果卻是：幾乎沒有改進。

也就是說：

• 參數(shù)提升 → 猜對的頻率高了 - 但邏輯驗證 → 步驟還是錯的，沒變聰明！這說明“變大”不等于“會思考”，構建嚴謹推理過程并不是靠堆疊模型規(guī)模就能實現(xiàn)的。

真相3：“多思考”不等于“更嚴謹”

研究人員還嘗試讓模型思考更久——具體方法是，允許模型生成更長的推理路徑（增加推理token上限）。但最終觀察到的是：

推理更長，并未帶來質的飛躍。

即使reasoning chain延展了好幾倍，邏輯準確率依然停留在原地徘徊，甚至出現(xiàn)“邏輯越寫越錯”的情況。

希望之光：兩種機制顯著改善推理質量

盡管整體結果表明大模型距離真正的邏輯證明還有明顯差距，但研究也找到了兩個真正有效的優(yōu)化策略：

策略一：自我反思反饋機制（Self-improvement via Critic as Feedback）

讓模型在解完題后反過來“自己打分、自己挑錯”，再進行修改。

• 該方法在 Gemini 2.5 Pro 上帶來了約5%的推理質量提升 - 模型開始避免常見跳步、數(shù)值錯用等問題

策略二：引入“定理線索”（Theorem Hints）輔助模型思考

研究者為模型提前準備關鍵定理（如 AM-GM、Cauchy-Schwarz），并嵌入到提示中，讓模型像人一樣“借助工具”進行證明。

• Gemini 2.5 Pro 的準確率在此策略下提升近10% - 解決了許多模型“不知道該套哪個定理”的盲區(qū)問題

加入IneqMath挑戰(zhàn)榜，展示你的模型推理實力

為推動大語言模型在嚴謹數(shù)學推理方面的進展，團隊構建了一個持續(xù)更新的IneqMath 評測排行榜，面向全球開放提交。無論你是在調試輕量模型，還是優(yōu)化頂級推理模型，都可以將其性能提交至平臺進行自動評估。

排行榜系統(tǒng)依托研究團隊提出的LLM-as-Judge自動評分框架，可無人工干預地評估模型在最終答案正確率與推理過程完整性兩方面的表現(xiàn)，確保高效且公正的比對。

歡迎各類模型參與測試——從主流大型模型到精心調校的實驗性模型，皆可在此一展風采。

提交你的模型，看看它能否登上“推理力”榜單的高峰～

挑戰(zhàn)頁面：https://huggingface.co/spaces/AI4Math/IneqMath-Leaderboard
項目主頁：ineqmath.github.io
論文：https://arxiv.org/abs/2506.07927
IneqMath數(shù)據(jù)集： https://huggingface.co/datasets/AI4Math/IneqMath
開源代碼： https://github.com/lupantech/ineqmath