來源：公眾號【機器之心】

llustration From IconScout By Scout Stores

據 IneqMath 的研究，大語言模型盡管在猜測正確答案方面表現出色，但在構造嚴謹的數學證明時仍存在結構性不足。模型規模的擴大或推理長度的增加，尚未能有效提升其邏輯閉合能力。研究指出，借助定理提示和自我反思機制，模型在“學習推理”方面展現出一定潛力。這表明，未來具備可靠證明能力的數學 AI，關鍵不在于模型體量，而在于工具使用和錯誤糾正的能力。

當前，大語言模型更接近于高效的猜測者。IneqMath 的長期目標，是推動其向具備結構化證明能力的“數學思維體”演化。

數學證明不僅要得出 “對” 的答案，更要給出邏輯閉合、層層嚴謹的推理過程。在不等式問題中尤其如此 —— 哪怕最終答案是對的，只要中間某一步出現紕漏，整個證明就可能不成立。我們不禁提問：這些答案是模型通過嚴密推理得出的，還是只是通過 “看起來合理” 的過程猜出來的？

不等式問題正是檢驗這一點的理想對象：它們結構清晰、邏輯對象簡單，在數學競賽與應用數學中都極為常見，同時具備較長的推理鏈條，能夠有效揭示推理中的漏洞或模糊之處。

這正是當前形式化數學所試圖解決的問題。近年來，Lean、Coq 等系統為數學提供了嚴格可驗證的推理機制，每一步推導都必須符合邏輯規則，可被計算機檢驗。然而，這類系統對語句的表達精度要求極高，建模成本大、自動化程度有限，尤其在面對中學到奧數級別的不等式問題時，很難做到規模化應用。

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

另一方面，當前主流的大語言模型是在海量自然語言上訓練出來的。它們雖然無法直接生成可被形式系統接受的機器檢查證明，卻在 “非形式化推理” 方面表現出色 —— 也就是說，它們往往能給出看似合理、直覺對路的答案，并模仿人類在解決問題初期的思維方式。這種能力雖然不符合傳統意義上的形式證明要求，但在探索性的數學過程中具有重要價值。

為此，斯坦福大學、加州大學伯克利分校與麻省理工學院的研究團隊提出了一種創新方法：將不等式證明任務拆解為兩個 “非形式化但可驗證” 的子任務，即 “界限估計” 和 “關系預測”，并基于此構建了第一個奧林匹克級不等式證明基準數據集 ——IneqMath。這一框架提供了一種介于完全形式化驗證與自然語言生成之間的 “中間層”，可以逐步審查模型的推理鏈條，從而判斷其是否真正掌握了推理結構，而不僅僅是在猜測答案。

論文標題： Solving Inequality Proofs with Large Language Models 論文鏈接： https://arxiv.org/abs/2506.07927 代碼鏈接： https://github.com/lupantech/ineqmath 項目主頁： https://ineqmath.github.io

本項目并非試圖替代形式化系統，而是希望補足當前 LLM 推理評估的盲區 ——在不依賴形式邏輯表達的前提下，仍然能對模型的推理嚴謹性進行系統、自動的檢驗，以更貼近人類思維的方式，衡量它們是否具備構造完整數學證明的潛力。

一、如何 “非形式化” 地評估不等式證明？

論文核心思路是：將不等式證明過程拆解為以下兩種子任務：界限估計與關系預測。

對于同一道數學證明題目: 對于任意非負實數 a，b，請證明 a+b≥2√ab 兩種任務分別把證明問題改寫成了不同的形式:

1?? Bound Estimation（界限估計）

對于任意非負實數 a，b，請判斷兩個式子的關系：a+b?2√ab

2?? Relation Prediction（關系預測）、

對于任意非負實數 a，b，請求出最大的常數 C 使得a+b≥C√ab恒成立。

這兩類任務都可以用自然語言和 LaTeX 表達，適合大模型按步驟求解，同時保留了不等式證明中的創造性核心，避免了形式化證明工具帶來的復雜負擔。并且每道題目有唯一的正確答案，方便驗證結果的正確性。

二、IneqMath：首個非形式化但可驗證的不等式證明數據集

研究團隊基于上述任務結構，構建了 IneqMath 數據集，覆蓋訓練、測試與驗證三部分：

• 訓練集：包含 1,252 道不等式題目，配有分步證明和定理標簽（共包含 83 種定理，如均值不等式、Chebyshev 不等式等，以及 29 個定理類別），適用于模型微調。

• 測試集：共 200 道題目，由國際數學奧林匹克（IMO）獎牌得主手工設計、資深數學家審核，強調復雜策略組合與邏輯鏈深度。

• 驗證集：共 100 道題目，題型與測試集保持一致，主要用于調參和中期評估。

以下是 IneqMath 的訓練和測試題目示例：

三、如何評估 LLM 的推理嚴謹性？

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

• Final Answer Judge（最終答案是否正確）

• Toy Case Judge（是否用特殊值推斷出一般的結論，忽略了泛化過程）

例如，如果只通過代入 a = 1, b = 2 來得出對任何非負實數 a, b 都成立 a+b≥2√ab 的結論就是在用特殊值推斷出一般的結論。

• Logical Gap Judge（是否存在跳步、未解釋的等價變形等邏輯偏差）

例如，對于一個復雜的函數 f (x)，直接說明 “經過復雜的數值計算我們知道 f (x) 的最小值在 x=1 取到 “但是沒有給出具體的最小值求解過程的就屬于邏輯偏差的一種，因為他跳過了關鍵的步驟。

• Numerical Approximation Judge（是否存在不當近似）

例如，若 ，但是后續的證明中全部把 f (x) 近似 的行為就屬于不當近似。

• Numerical Computation Judge（計算是否正確，包括基本代數運算或代入過程中的數值錯誤）

例如，把 23x76（應該等于 1541）計算成了 1641 就屬于一種計算錯誤。

通過這套系統，研究者可以判斷一個模型是否只是 “碰巧答對了”，還是在每一個推理節點上都做對了。

同時這些評審器在準確性上表現出與人類標注高度一致。如下圖所示，評審器系統在與人工標注對齊的任務上達到了 F1 = 0.93 的表現，證明了這一方法既可靠又具可擴展性，可有效替代大規模人工審閱。

四、實驗結果

重磅發現一：Soundness Gap 是真實存在的！

研究測試了包括 GPT-4、Claude、Gemini、Grok、Mistral、LLaMA 等在內的 29 款主流 LLM，發現：

• Grok 3 mini：最終答案準確率高達 71.5%，但經逐步評審后驟降至 6.0%！

• 所有模型準確率下降幅度最多達 65.5%

• 開源推理模型：最佳也僅達 6% 準確率

• 聊天型大模型（chat LLMs）：整體準確率低于 5%

研究者指出，這意味著當前 LLM “猜得準但推不全”，邏輯鏈條存在 “虛假自洽” 的陷阱。

重磅發現二： 模型越大 = 推理越好嗎？未必！

實驗發現，大語言模型在 “最終答案準確率” 上確實會隨著模型規模提升而穩步增長，說明大模型在 “猜對答案” 這件事上確實更厲害了。但一旦我們開始評估推理過程是否嚴謹，情況就沒那么樂觀了：隨著模型變大，“整體推理正確率” 提升有限、甚至不再提升。這意味著：更大的模型并不能自動學會更嚴謹的邏輯鏈條。換句話說，LLM 可以越猜越準，但證明過程還遠談不上靠譜。僅靠堆參數，解決不了推理的本質問題。

重磅發現三：多算≠更嚴謹

研究團隊通過增加推理 token 數讓大模型在解題時 “想得更久”。結果發現：推理鏈更長，只帶來輕微提升，且很快進入飽和狀態 。換句話說，計算多了，推理依然不嚴謹。對復雜數學證明來說，“多想” 遠不如 “想對”。

五、曙光初現：批判增強與定理提示可帶來性能提升

盡管當前模型在邏輯嚴謹性上的表現仍不理想，擴大模型規模或延長推理過程也難以顯著提升推理質量，但研究團隊仍發現了一些確實有效的改進策略：

• 自我批判提升（Self-improvement via critic）：自我評判自己的作答，評判后重新對答案進行修改。 該策略為 Gemini 2.5 Pro 帶來約 5% 的提升。

• 定理提示（Theorem Augmentation）：通過自動檢索相關定理并作為提示提供給模型，幫助其在關鍵步驟做出更合理的推理選擇。 Gemini 2.5 Pro 在這一策略下準確率提升約 10%。

六、歡迎參與 IneqMath 排行榜挑戰！

為了推動模型在嚴謹數學推理上的進步，研究團隊特別設立了一個 動態更新的排行榜，供研究者與開發者提交自己的模型結果。該平臺支持自動評估提交模型在 IneqMath 中的表現，涵蓋最終答案準確率與推理過程嚴謹性，評價機制由 LLM-as-Judge 系統支撐，無需人工干預即可完成高質量判分。

研究團隊誠摯邀請社區廣泛參與 —— 無論是大型基礎模型，還是你訓練的小型創新模型，都可以提交來一試高下！

歡迎訪問：https://huggingface.co/spaces/AI4Math/IneqMath-Leaderboard 了解詳情，并提交你的挑戰結果！

七、結語

IneqMath 的研究表明，大語言模型雖能猜出不少正確答案，但在真正構造嚴謹數學證明時，仍存在結構性短板。無論是更大的模型，還是更長的 “思考過程”，都難以從根本上提升其邏輯閉合能力。

然而，曙光初現：通過定理提示與自我批判提升等方法，模型開始展現出 “學會推理” 的可能性。這意味著，真正可靠的數學 AI，不一定更大，但一定更會使用工具，更會自我反思。

大模型如今是優秀的猜測者，但還遠不是可靠的證明者。那么 IneqMath 的目標，是推動它們成為能構造證明的真正 “數學思維體”。

讓我們相信，這只是開始。

作者介紹

本項目由來自斯坦福大學、麻省理工學院（MIT）和加州大學伯克利分校的研究者聯合完成。

本項目負責人 Pan Lu 是斯坦福大學的博士后研究員。他的研究涵蓋大語言模型、智能體優化、數學與科學發現等方向，相關成果獲 ICLR、NeurIPS 最具影響力論文獎，并曾獲得 Amazon、Bloomberg、Qualcomm 等多項博士獎學金。

合作者 Alex Gu 是麻省理工學院（MIT）計算機科學博士生，師從 Armando Solar-Lezama 教授，研究方向為神經符號程序學習，聚焦編程與數學中的智能推理。他曾在 Meta AI、Jane Street、Pony.ai 等多家機構實習，并榮獲 NSF GRFP 獎學金。

另一位合作者 Jikai Jin 是斯坦福大學計算與數學工程研究所（ICME）的博士生，研究興趣跨越機器學習、統計學與運籌優化等多個領域，致力于為真實世界問題提供理論與實踐兼具的解決方案。他本科畢業于北京大學數學科學學院。

閱讀最新前沿科技趨勢報告，請訪問歐米伽研究所的“未來知識庫”

https://wx.zsxq.com/group/454854145828

未來知識庫是“ 歐米伽 未來研究所”建立的在線知識庫平臺，收藏的資料范圍包括人工智能、腦科學、互聯網、超級智能，數智大腦、能源、軍事、經濟、人類風險等等領域的前沿進展與未來趨勢。目前擁有超過8000篇重要資料。每周更新不少于100篇世界范圍最新研究資料。 歡迎掃描二維碼或訪問https://wx.zsxq.com/group/454854145828進入。

截止到3月31日 ”未來知識庫”精選的百部前沿科技趨勢報告

（加入未來知識庫，全部資料免費閱讀和下載）