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

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

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

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

看起來像解出來了，其實(shí)全是錯(cuò)的

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

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

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

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

△使用Lean進(jìn)行形式化證明的過程

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

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

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

以下是IneqMath的Bound Estimation（界限估計(jì)）和 Relation Prediction（關(guān)系判斷）兩種題目的示例：

△Bound Estimation（界限估計(jì)）訓(xùn)練集題目示例

△Relation Estimation（關(guān)系判斷）訓(xùn)練集題目示例

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

△Relation Estimation（關(guān)系判斷）測試集題目示例

另外可訪問研究團(tuán)隊(duì)的可視化工具查看IneqMath的所有題目（鏈接在文末獲取）。

LLM作為Judge，是如何運(yùn)作的？

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

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

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

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

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

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

實(shí)驗(yàn)結(jié)果揭示LLM推理的“真面目”

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

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

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

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

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

也就是說：

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

真相3：“多思考”不等于“更嚴(yán)謹(jǐn)”

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

推理更長，并未帶來質(zhì)的飛躍。

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

希望之光：兩種機(jī)制顯著改善推理質(zhì)量

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

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

讓模型在解完題后反過來“自己打分、自己挑錯(cuò)”，再進(jìn)行修改。

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

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

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

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

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

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

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

歡迎各類模型參與測試——從主流大型模型到精心調(diào)校的實(shí)驗(yàn)性模型，皆可在此一展風(fēng)采。

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

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