新智元報道
新智元報道
編輯：LRST
【新智元導讀】大語言模型在數學證明中常出現推理漏洞，如跳步或依賴特殊值。斯坦福等高校團隊提出IneqMath基準，將不等式證明拆解為可驗證的子任務。結果顯示，模型的推理正確率遠低於答案正確率，暴露出其在數學推理上的缺陷。
在大模型頻頻給出「看似完美」答案的今天，我們是否已經迎來了真正「會推理」的AI？
多位網友分享了自己的經歷，「我試過用LLMs做正割和正切的定理的證明，但是結果錯誤的太多了！」
「大語言模型在解題的時候可能只是從訓練資料集中概括了推理模式，但是並沒有具體問題用具體的方法分析。」
「大語言模型的幻覺始終是諸多人工智慧應用（包括數學證明）的主要障礙！」
這些大模型在面對數學證明題目時，自信滿滿地輸出了「解題思路」和「證明過程」，一切看上去井井有條。但你是否注意到，很多推理其實沒有解釋關鍵步驟，甚至直接用一個「看起來合理的句子」替代了邏輯推導？
這不是個別現象，而是結構性問題。近日，來自斯坦福大學、麻省理工學院（MIT）與加州大學伯克利分校的研究團隊聯合提出了一個創新性數學不等式基準IneqMath，專門用於評估語言模型在複雜數學推理中的嚴謹性與合理性。
論文連結：https://arxiv.org/abs/2506.07927
官方網站：ineqmath.github.io
資料集連結：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能力的認知。它們已經能寫論文、解題，甚至「解釋」自己的推理過程。
但研究者發現一個驚人的現象：很多模型確實能給出正確答案，但它們的推理過程卻漏洞百出，比如：
-
跳過中間關鍵步驟，直接下結論
-
用特殊數值代入來「猜測」一般規律
-
數值近似粗糙，邏輯推導不閉合
-
寫得像人話，但並不是真正的數學語言
這意味著，當前大模型並不具備穩定、可靠的邏輯結構。它們可以「合理地猜對」，但無法「嚴格地推理對」。
讓AI暴露推理盲點
為了解決這一問題，研究團隊構建了全新的數學評測體系IneqMath，核心思路是：
-
用不等式證明題作為切入點
-
將證明過程拆解為「選擇題」和「填空題」形式的自然語言任務，包括Bound Estimation（界限估計）和Relation Prediction（關係預測）
-
構建訓練、驗證與測試資料集，涵蓋奧數級難度題目與複雜定理組合
-
引入五種「自動評審器」，構成LLM-as-Judge框架，審查模型每一步推理的合理性
這種「非形式化但可驗證」的方法，比單純要求形式邏輯更貼近人類實際思維，也能同時定量衡量大語言模型的答案和過程的推理準確性。
其中Bound Estimation（界限估計）和Relation Prediction（關係預測）的題目示例如下
Bound Estimation（界限估計）測試集題目示例
Relation Estimation（關係判斷）測試集題目示例
從多維角度審查AI推理過程
為了深入評估大模型的推理嚴謹性，研究團隊設計了一個名為LLM-as-Judge的自動審查框架，內部由五個獨立的「評審器」組成，專門從多個維度對模型的解題過程進行細緻分析。
這些「評委」分別是Final Answer Judge用來衡量最終的答案是否正確、和4個Step-wise Judge用來從不同的維度衡量推理的步驟是否是正確的。
藉助這一系統，研究者不再僅僅關注模型「猜得準」與否，而是能逐步拆解每一步邏輯鏈，判斷模型是否真正具備嚴密推理的能力，而非只是「蒙對了結論」。
這4個Step-wise Judge分別是Toy Case Judge、Logical Gap Judge、Numerical Approximation Judge、Numerical Computation Judge
Toy Case Judge
它的職責是識別模型是否透過代入個別特殊數值（如a=1, b=2）來推匯出對所有情況都成立的結論。
可以看到，該模型在求解過程中藉助特定數值的帶入，並依賴代入後表示式的大小關係來推斷其最小上界，這實際上是一種以有限例項推及普遍結論的推理方式。
Toy Case Judge針對模型結果中這種透過特殊取值進行推斷的現象進行了深入剖析，精準地定位了問題，並最終判定為False，說明該結論因基於特例而不具備普遍性，應視為不正確。
Logical Gap Judge
它主要負責判斷模型的推理鏈條中是否存在關鍵步驟的跳過、推導中缺乏解釋的等價變換，或者直接從條件躍遷到結論而沒有交代中間過程。
可以看到，該語句聲稱「數值檢驗確認最小值發生在 x = 1」，卻完全未展示任何實際數值結果、評估過程或可視／分析證據來支撐這一說法，這實際上是一種無充足依據的斷言式推理。
Logical Gap Judge針對這類缺乏實證資料與分析佐證的論斷進行了深入評估，精準定位了其中的邏輯空缺，並最終判定為False，指出該結論因證據不足而不具備說服力，應被視為錯誤。
Numerical Approximation Judge
它會檢查模型是否使用了模糊不清的數值估算替代了精確計算，進而破壞了數學證明所要求的嚴謹性。
可以看到，上述計算依賴於三角函式的近似十進位制值。僅透過將S的近似值與114做比較來推斷二者關係，並不具備嚴格的數學依據。
這正是Numerical Approximation Judge所關注的問題：針對這種因過度依賴粗糙近似而產生的誤導性結論，Judge進行了詳盡審查，精確識別了其中的數值近似漏洞，最終判定為False，表明該結論因數值近似失當而不夠嚴謹，應被視為錯誤。
Numerical Computation Judge
它專注於捕捉模型在基礎運算中出現的錯誤，比如簡單的乘法加法算錯，或者代入過程中產生了錯誤的數值推導。
可以看到，Numerical Computation Judge會首先從響應文字中自動識別出所有的數值計算的表示式
然後基於這些等式生成對應的驗證程式碼（這裡使用了Sympy的Rational型別）執行後卻發現出現了數值計算上的錯誤。
Numerical Computation Judge正是透過這種提取–編碼–執行的數值檢驗流程，精準地定位到計算環節的遺漏或錯誤，並最終判定該推斷為False，指出原步驟因數值計算不正確而錯誤。
令人震驚的「Soundness Gap」
研究團隊使用LLM-as-Judge在GPT-4、Claude、Grok、Gemini、Llama等29款主流模型上進行了系統評估，結果顯示：
-
Grok3 mini最終答案正確率達71.5%，但推理過程正確率僅為6.0%
-
所有模型推理正確率最多下降65.5%，說明它們經常「猜得準但講不清」
-
開源模型（如Mistral、Llama）的「邏輯嚴謹性」表現最弱，不超過6%
這意味著目前大語言模型推理鏈條中存在嚴重結構性缺陷，即使答對了，也無法保證中間過程有邏輯閉環。
IneqMath打榜
為了推動大語言模型在嚴謹數學論證上的突破，科研團隊搭建了一個持續更新的IneqMath排行榜，向全球開發者開放提交。
不論你是在除錯輕量化模型，還是在最佳化頂級推理系統，都能將成果上傳平臺，自動化評測其答案正確率與推理完整度。
排行榜連結：https://huggingface.co/spaces/AI4Math/IneqMath-Leaderboard
排行榜提供多種篩選功能，讓您輕鬆挑選感興趣的模型類別；只需點選表頭，即可按照任意欄位自定義排序。頁面還直觀展示了各模型的關鍵引數，便於快速對比與檢視。
如需提交自己的模型結果，點選進入網頁後即可看到提交介面。上傳模型的結果，並填寫對應的模型引數後，您的模型結果就會自動的在後臺進行評估。
提交後，點選頁面上方的「Process Query」按鈕，輸入「提交時填寫的郵箱地址」，即可檢視評估結果。
在此介面，你可以將成績一鍵釋出至公共排行榜，向大家展示你的出色表現；如對當前排名不滿意，也可隨時在此將其移除。
參考資料：
https://ineqmath.github.io/