數學證明不僅要得出 “對” 的答案，更要給出邏輯閉合、層層嚴謹的推理過程。在不等式問題中尤其如此 —— 哪怕最終答案是對的，只要中間某一步出現紕漏，整個證明就可能不成立。我們不禁提問：這些答案是模型透過嚴密推理得出的，還是隻是透過 “看起來合理” 的過程猜出來的？
不等式問題正是檢驗這一點的理想物件：它們結構清晰、邏輯物件簡單，在數學競賽與應用數學中都極為常見，同時具備較長的推理鏈條，能夠有效揭示推理中的漏洞或模糊之處。
這正是當前形式化數學所試圖解決的問題。近年來，Lean、Coq 等系統為數學提供了嚴格可驗證的推理機制，每一步推導都必須符合邏輯規則，可被計算機檢驗。然而，這類系統對語句的表達精度要求極高，建模成本大、自動化程度有限，尤其在面對中學到奧數級別的不等式問題時，很難做到規模化應用。
使用 Lean 進行形式化證明的過程
另一方面，當前主流的大語言模型是在海量自然語言上訓練出來的。它們雖然無法直接生成可被形式系統接受的機器檢查證明，卻在 “非形式化推理” 方面表現出色 —— 也就是說，它們往往能給出看似合理、直覺對路的答案，並模仿人類在解決問題初期的思維方式。這種能力雖然不符合傳統意義上的形式證明要求，但在探索性的數學過程中具有重要價值。
為此，斯坦福大學、加州大學伯克利分校與麻省理工學院的研究團隊提出了一種創新方法：將不等式證明任務拆解為兩個 “非形式化但可驗證” 的子任務，即 “界限估計” 和 “關係預測”，並基於此構建了第一個奧林匹克級不等式證明基準資料集 ——IneqMath。這一框架提供了一種介於完全形式化驗證與自然語言生成之間的 “中間層”，可以逐步審查模型的推理鏈條，從而判斷其是否真正掌握了推理結構，而不僅僅是在猜測答案。
-
完整專案主頁：🌐 https://ineqmath.github.io
-
📜 論文：https://arxiv.org/abs/2506.07927
-
🛠️ 程式碼庫：https://github.com/lupantech/ineqmath
-
📊 資料集：https://huggingface.co/datasets/AI4Math/IneqMath
-
🏆 排行榜：https://huggingface.co/spaces/AI4Math/IneqMath-Leaderboard
-
🔍 資料集視覺化展示：https://ineqmath.github.io/#visualization
-
𝕏 推特：https://x.com/lupantech/status/1932866286427779586
本專案並非試圖替代形式化系統，而是希望補足當前 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（計算是否正確，包括基本代數運算或代入過程中的數值錯誤）
例如，把 23×76（應該等於 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）的博士生，研究興趣跨越機器學習、統計學與運籌最佳化等多個領域，致力於為真實世界問題提供理論與實踐兼具的解決方案。他本科畢業於北京大學數學科學學院。
© THE END
轉載請聯絡本公眾號獲得授權
投稿或尋求報道：[email protected]