新智元報(bào)道

編輯：LRST

【新智元導(dǎo)讀】大語(yǔ)言模型在數(shù)學(xué)證明中常出現(xiàn)推理漏洞，如跳步或依賴特殊值。斯坦福等高校團(tuán)隊(duì)提出IneqMath基準(zhǔn)，將不等式證明拆解為可驗(yàn)證的子任務(wù)。結(jié)果顯示，模型的推理正確率遠(yuǎn)低于答案正確率，暴露出其在數(shù)學(xué)推理上的缺陷。

在大模型頻頻給出「看似完美」答案的今天，我們是否已經(jīng)迎來(lái)了真正「會(huì)推理」的AI？

多位網(wǎng)友分享了自己的經(jīng)歷，「我試過(guò)用LLMs做正割和正切的定理的證明，但是結(jié)果錯(cuò)誤的太多了！」

「大語(yǔ)言模型在解題的時(shí)候可能只是從訓(xùn)練數(shù)據(jù)集中概括了推理模式，但是并沒(méi)有具體問(wèn)題用具體的方法分析。」

「大語(yǔ)言模型的幻覺(jué)始終是諸多人工智能應(yīng)用（包括數(shù)學(xué)證明）的主要障礙！」

這些大模型在面對(duì)數(shù)學(xué)證明題目時(shí)，自信滿滿地輸出了「解題思路」和「證明過(guò)程」，一切看上去井井有條。但你是否注意到，很多推理其實(shí)沒(méi)有解釋關(guān)鍵步驟，甚至直接用一個(gè)「看起來(lái)合理的句子」替代了邏輯推導(dǎo)？

這不是個(gè)別現(xiàn)象，而是結(jié)構(gòu)性問(wèn)題。近日，來(lái)自斯坦福大學(xué)、麻省理工學(xué)院（MIT）與加州大學(xué)伯克利分校的研究團(tuán)隊(duì)聯(lián)合提出了一個(gè)創(chuàng)新性數(shù)學(xué)不等式基準(zhǔn)IneqMath，專門(mén)用于評(píng)估語(yǔ)言模型在復(fù)雜數(shù)學(xué)推理中的嚴(yán)謹(jǐn)性與合理性。

論文鏈接：https://arxiv.org/abs/2506.07927

官方網(wǎng)站：ineqmath.github.io

數(shù)據(jù)集鏈接：https://huggingface.co/datasets/AI4Math/IneqMath

代碼鏈接：https://github.com/lupantech/ineqmath

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

題目可視化展示：https://ineqmath.github.io/#visualization

AI會(huì)答題，但它真的會(huì)「證明」嗎？

過(guò)去幾年，像GPT-4、Claude、Gemini等大模型不斷刷新我們對(duì)AI能力的認(rèn)知。它們已經(jīng)能寫(xiě)論文、解題，甚至「解釋」自己的推理過(guò)程。

但研究者發(fā)現(xiàn)一個(gè)驚人的現(xiàn)象：很多模型確實(shí)能給出正確答案，但它們的推理過(guò)程卻漏洞百出，比如：

• 跳過(guò)中間關(guān)鍵步驟，直接下結(jié)論

• 用特殊數(shù)值代入來(lái)「猜測(cè)」一般規(guī)律

• 數(shù)值近似粗糙，邏輯推導(dǎo)不閉合

• 寫(xiě)得像人話，但并不是真正的數(shù)學(xué)語(yǔ)言

這意味著，當(dāng)前大模型并不具備穩(wěn)定、可靠的邏輯結(jié)構(gòu)。它們可以「合理地猜對(duì)」，但無(wú)法「嚴(yán)格地推理對(duì)」。

讓AI暴露推理盲點(diǎn)

為了解決這一問(wèn)題，研究團(tuán)隊(duì)構(gòu)建了全新的數(shù)學(xué)評(píng)測(cè)體系IneqMath，核心思路是：

1. 用不等式證明題作為切入點(diǎn)

2. 將證明過(guò)程拆解為「選擇題」和「填空題」形式的自然語(yǔ)言任務(wù)，包括Bound Estimation（界限估計(jì)）和Relation Prediction（關(guān)系預(yù)測(cè)）

3. 構(gòu)建訓(xùn)練、驗(yàn)證與測(cè)試數(shù)據(jù)集，涵蓋奧數(shù)級(jí)難度題目與復(fù)雜定理組合

4. 引入五種「自動(dòng)評(píng)審器」，構(gòu)成LLM-as-Judge框架，審查模型每一步推理的合理性

這種「非形式化但可驗(yàn)證」的方法，比單純要求形式邏輯更貼近人類實(shí)際思維，也能同時(shí)定量衡量大語(yǔ)言模型的答案和過(guò)程的推理準(zhǔn)確性。

其中Bound Estimation（界限估計(jì)）和Relation Prediction（關(guān)系預(yù)測(cè)）的題目示例如下

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

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

從多維角度審查AI推理過(guò)程

為了深入評(píng)估大模型的推理嚴(yán)謹(jǐn)性，研究團(tuán)隊(duì)設(shè)計(jì)了一個(gè)名為LLM-as-Judge的自動(dòng)審查框架，內(nèi)部由五個(gè)獨(dú)立的「評(píng)審器」組成，專門(mén)從多個(gè)維度對(duì)模型的解題過(guò)程進(jìn)行細(xì)致分析。

這些「評(píng)委」分別是Final Answer Judge用來(lái)衡量最終的答案是否正確、和4個(gè)Step-wise Judge用來(lái)從不同的維度衡量推理的步驟是否是正確的。

借助這一系統(tǒng)，研究者不再僅僅關(guān)注模型「猜得準(zhǔn)」與否，而是能逐步拆解每一步邏輯鏈，判斷模型是否真正具備嚴(yán)密推理的能力，而非只是「蒙對(duì)了結(jié)論」。

這4個(gè)Step-wise Judge分別是Toy Case Judge、Logical Gap Judge、Numerical Approximation Judge、Numerical Computation Judge

Toy Case Judge

它的職責(zé)是識(shí)別模型是否通過(guò)代入個(gè)別特殊數(shù)值（如a=1, b=2）來(lái)推導(dǎo)出對(duì)所有情況都成立的結(jié)論。

可以看到，該模型在求解過(guò)程中借助特定數(shù)值的帶入，并依賴代入后表達(dá)式的大小關(guān)系來(lái)推斷其最小上界，這實(shí)際上是一種以有限實(shí)例推及普遍結(jié)論的推理方式。

Toy Case Judge針對(duì)模型結(jié)果中這種通過(guò)特殊取值進(jìn)行推斷的現(xiàn)象進(jìn)行了深入剖析，精準(zhǔn)地定位了問(wèn)題，并最終判定為False，說(shuō)明該結(jié)論因基于特例而不具備普遍性，應(yīng)視為不正確。

Logical Gap Judge

它主要負(fù)責(zé)判斷模型的推理鏈條中是否存在關(guān)鍵步驟的跳過(guò)、推導(dǎo)中缺乏解釋的等價(jià)變換，或者直接從條件躍遷到結(jié)論而沒(méi)有交代中間過(guò)程。

可以看到，該語(yǔ)句聲稱「數(shù)值檢驗(yàn)確認(rèn)最小值發(fā)生在 x = 1」，卻完全未展示任何實(shí)際數(shù)值結(jié)果、評(píng)估過(guò)程或可視／分析證據(jù)來(lái)支撐這一說(shuō)法，這實(shí)際上是一種無(wú)充足依據(jù)的斷言式推理。

Logical Gap Judge針對(duì)這類缺乏實(shí)證數(shù)據(jù)與分析佐證的論斷進(jìn)行了深入評(píng)估，精準(zhǔn)定位了其中的邏輯空缺，并最終判定為False，指出該結(jié)論因證據(jù)不足而不具備說(shuō)服力，應(yīng)被視為錯(cuò)誤。

Numerical Approximation Judge

它會(huì)檢查模型是否使用了模糊不清的數(shù)值估算替代了精確計(jì)算，進(jìn)而破壞了數(shù)學(xué)證明所要求的嚴(yán)謹(jǐn)性。

可以看到，上述計(jì)算依賴于三角函數(shù)的近似十進(jìn)制值。僅通過(guò)將S的近似值與114做比較來(lái)推斷二者關(guān)系，并不具備嚴(yán)格的數(shù)學(xué)依據(jù)。

這正是Numerical Approximation Judge所關(guān)注的問(wèn)題：針對(duì)這種因過(guò)度依賴粗糙近似而產(chǎn)生的誤導(dǎo)性結(jié)論，Judge進(jìn)行了詳盡審查，精確識(shí)別了其中的數(shù)值近似漏洞，最終判定為False，表明該結(jié)論因數(shù)值近似失當(dāng)而不夠嚴(yán)謹(jǐn)，應(yīng)被視為錯(cuò)誤。

Numerical Computation Judge

它專注于捕捉模型在基礎(chǔ)運(yùn)算中出現(xiàn)的錯(cuò)誤，比如簡(jiǎn)單的乘法加法算錯(cuò)，或者代入過(guò)程中產(chǎn)生了錯(cuò)誤的數(shù)值推導(dǎo)。

可以看到，Numerical Computation Judge會(huì)首先從響應(yīng)文本中自動(dòng)識(shí)別出所有的數(shù)值計(jì)算的表達(dá)式

然后基于這些等式生成對(duì)應(yīng)的驗(yàn)證代碼（這里使用了Sympy的Rational類型）執(zhí)行后卻發(fā)現(xiàn)出現(xiàn)了數(shù)值計(jì)算上的錯(cuò)誤。

Numerical Computation Judge正是通過(guò)這種提取–編碼–執(zhí)行的數(shù)值檢驗(yàn)流程，精準(zhǔn)地定位到計(jì)算環(huán)節(jié)的遺漏或錯(cuò)誤，并最終判定該推斷為False，指出原步驟因數(shù)值計(jì)算不正確而錯(cuò)誤。

令人震驚的「Soundness Gap」

研究團(tuán)隊(duì)使用LLM-as-Judge在GPT-4、Claude、Grok、Gemini、Llama等29款主流模型上進(jìn)行了系統(tǒng)評(píng)估，結(jié)果顯示：

• Grok3 mini最終答案正確率達(dá)71.5%，但推理過(guò)程正確率僅為6.0%

• 所有模型推理正確率最多下降65.5%，說(shuō)明它們經(jīng)常「猜得準(zhǔn)但講不清」

• 開(kāi)源模型（如Mistral、Llama）的「邏輯嚴(yán)謹(jǐn)性」表現(xiàn)最弱，不超過(guò)6%

這意味著目前大語(yǔ)言模型推理鏈條中存在嚴(yán)重結(jié)構(gòu)性缺陷，即使答對(duì)了，也無(wú)法保證中間過(guò)程有邏輯閉環(huán)。

IneqMath打榜

為了推動(dòng)大語(yǔ)言模型在嚴(yán)謹(jǐn)數(shù)學(xué)論證上的突破，科研團(tuán)隊(duì)搭建了一個(gè)持續(xù)更新的IneqMath排行榜，向全球開(kāi)發(fā)者開(kāi)放提交。

不論你是在調(diào)試輕量化模型，還是在優(yōu)化頂級(jí)推理系統(tǒng)，都能將成果上傳平臺(tái)，自動(dòng)化評(píng)測(cè)其答案正確率與推理完整度。

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

排行榜提供多種篩選功能，讓您輕松挑選感興趣的模型類別；只需點(diǎn)擊表頭，即可按照任意字段自定義排序。頁(yè)面還直觀展示了各模型的關(guān)鍵參數(shù)，便于快速對(duì)比與查看。

如需提交自己的模型結(jié)果，點(diǎn)擊進(jìn)入網(wǎng)頁(yè)后即可看到提交界面。上傳模型的結(jié)果，并填寫(xiě)對(duì)應(yīng)的模型參數(shù)后，您的模型結(jié)果就會(huì)自動(dòng)的在后臺(tái)進(jìn)行評(píng)估。

提交后，點(diǎn)擊頁(yè)面上方的「Process Query」按鈕，輸入「提交時(shí)填寫(xiě)的郵箱地址」，即可查看評(píng)估結(jié)果。

在此界面，你可以將成績(jī)一鍵發(fā)布至公共排行榜，向大家展示你的出色表現(xiàn)；如對(duì)當(dāng)前排名不滿意，也可隨時(shí)在此將其移除。

參考資料：

https://ineqmath.github.io/