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

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

圖片

「大語言模型在解題的時候可能只是從訓(xùn)練數(shù)據(jù)集中概括了推理模式，但是并沒有具體問題用具體的方法分析?！?/p>

圖片

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

圖片

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

這不是個別現(xiàn)象，而是結(jié)構(gòu)性問題。近日，來自斯坦福大學(xué)、麻省理工學(xué)院（MIT）與加州大學(xué)伯克利分校的研究團(tuán)隊(duì)聯(lián)合提出了一個創(chuàng)新性數(shù)學(xué)不等式基準(zhǔn)IneqMath，專門用于評估語言模型在復(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會答題，但它真的會「證明」嗎？

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

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

• 跳過中間關(guān)鍵步驟，直接下結(jié)論
• 用特殊數(shù)值代入來「猜測」一般規(guī)律
• 數(shù)值近似粗糙，邏輯推導(dǎo)不閉合
• 寫得像人話，但并不是真正的數(shù)學(xué)語言

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

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

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

1. 用不等式證明題作為切入點(diǎn)
2. 將證明過程拆解為「選擇題」和「填空題」形式的自然語言任務(wù)，包括Bound Estimation（界限估計(jì)）和Relation Prediction（關(guān)系預(yù)測）
3. 構(gòu)建訓(xùn)練、驗(yàn)證與測試數(shù)據(jù)集，涵蓋奧數(shù)級難度題目與復(fù)雜定理組合
4. 引入五種「自動評審器」，構(gòu)成LLM-as-Judge框架，審查模型每一步推理的合理性

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

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

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

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

從多維角度審查AI推理過程

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

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

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

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

Toy Case Judge

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

圖片

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

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

Logical Gap Judge

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

圖片

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

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

Numerical Approximation Judge

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

圖片

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

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

Numerical Computation Judge

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

圖片

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

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

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

令人震驚的「Soundness Gap」

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

• Grok3 mini最終答案正確率達(dá)71.5%，但推理過程正確率僅為6.0%
• 所有模型推理正確率最多下降65.5%，說明它們經(jīng)?！覆碌脺?zhǔn)但講不清」
• 開源模型（如Mistral、Llama）的「邏輯嚴(yán)謹(jǐn)性」表現(xiàn)最弱，不超過6%

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

圖片

IneqMath打榜

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

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

圖片

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

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

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

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

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

參考資料：https://ineqmath.github.io/