用大語言模型求解不等式證明

用大語言模型求解不等式證明

Solving Inequality Proofs with Large Language Models

https://arxiv.org/pdf/2506.07927v2

摘 要
不等式證明在眾多科學與數學領域中至關重要，它考驗著高級推理能力，例如發現緊致界（tight bounds）和策略性地應用定理。這使其成為大語言模型（LLMs）面臨的一個獨特而具有挑戰性的前沿任務，所提供的洞見超越了一般的數學問題求解。然而，該領域的進展受到現有數據集的制約——這些數據集往往稀缺、合成生成，或形式過于僵化。我們通過提出一種非正式但可驗證的任務形式來應對這一挑戰，將不等式證明重新表述為兩個可自動檢驗的子任務：界估計（bound estimation）與關系預測（relation prediction）。在此基礎上，我們發布了 IneqMath——一個由專家精心整理的奧林匹克級別不等式數據集，包含一個測試集和一個訓練語料庫，后者配有逐步解答和定理標注。我們還開發了一種新穎的“大語言模型作為評判者”（LLM-as-judge）評估框架，該框架結合了一個最終答案評判者與四個步驟級評判者，專門用于檢測常見的推理缺陷。在 IneqMath 上對 29 個主流大語言模型的系統評估揭示了一個令人驚訝的現實：即使是最先進的模型（如 o1），在步驟級嚴格審查下整體準確率也低于 10%；相較于僅考慮最終答案等價性時的準確率，這一數字最多下降了 65.5%。這種差距暴露了當前大語言模型在演繹鏈條上的脆弱性，以及在“找到答案”與“構建嚴謹證明”之間的關鍵鴻溝。擴大模型規模或增加測試時計算資源對整體證明正確性的提升作用有限。相反，我們的研究結果指出了若干有前景的研究方向，例如定理引導的推理（theorem-guided reasoning）和自我精煉（self-refinement）。

1 引言
數學不等式在分析、優化和概率論等諸多領域中具有基礎性地位，其應用遍及科學建模、經濟學以及競賽數學。證明一個不等式是一項復雜的工作，不僅需要計算能力，更要求一種精妙的綜合能力：包括發現緊致界（tight bounds）的直覺、策略性地選擇與應用經典定理（例如均值-幾何平均不等式 AM-GM、柯西-施瓦茨不等式 Cauchy-Schwarz）的洞察力，以及精確的符號變換能力。這些能力是高級數學推理的標志，使不等式證明區別于一般的數學問題求解。因此，若能實現這一過程的自動化，將產生廣泛影響：可為自動定理證明器（ATPs）提供缺失的引理，加速形式化驗證流程，并為通用推理系統提供一個極具挑戰性的測試平臺。

然而，盡管大語言模型（如 DeepSeek-R1 [14] 和 OpenAI o3 [48]）以及自動定理證明器本身 [16, 18, 26, 34, 50, 75] 已取得顯著進展，不等式證明的自動化仍然是一個充滿挑戰的前沿問題。阻礙大語言模型在該領域能力提升的一個主要瓶頸是缺乏合適的基準數據集。現有資源在多個方面存在不足：通用 ATP 數據集如 MiniF2F [82] 和 ProofNet [7] 中包含的不等式數量極少；合成數據集如 INT [64] 和 AIPS [63] 雖具規模，但由于基于模板生成，可能缺乏結構多樣性；而人工整理的數據集如 ChenNEQ [8] 則通常規模過小，難以支撐大規模訓練。

更根本的是，大多數現有數據集采用完全形式化的表示方式，將問題和證明編碼在 Lean [11] 或 Isabelle [42] 等形式系統中。雖然形式化數學推理能提供正確性保證，且是重要的研究方向，但大語言模型是在海量自然語言語料上訓練而成，往往展現出強大的非形式化推理能力。這表明，即使模型難以應對形式化證明器嚴苛的語法要求，它們仍可能以非形式化的方式解決問題。因此，我們的工作旨在探索并評估這種非形式化能力，通過聚焦更貼近人類直覺、更接近數學發現初期（通常結構較松散）的推理模式，來補充當前形式化數學人工智能的研究。

為彌合形式嚴謹性與直觀解題之間的鴻溝，我們提出了一種非正式但可驗證的任務形式（§2）。我們不要求模型在形式系統內生成完全可機器檢驗的證明，而是將不等式問題重新表述為兩個具體且可自動驗證的子任務：(i) 界估計（Bound estimation）——確定能使不等式成立的最大（或最小）常數 C C；(ii) 關系預測（Relation prediction）——判斷兩個表達式之間成立的關系（>、≥、=、≤ 或 <）。這兩個任務均可使用自然語言和 LaTeX 表達，由大語言模型逐步求解，其最終答案（一個常數或一個關系符號）可被自動驗證。這種方式保留了不等式證明的創造性本質，同時避免了形式化證明輔助工具帶來的沉重開銷。

基于這一任務形式，我們發布了 IneqMath（§3）——首個完全以非正式語言編寫的、大規模奧林匹克級別不等式數據集。測試集包含 200 道原創題目，均由國際數學奧林匹克（IMO）級別獎牌得主精心設計并審核，確保其原創性與難度。訓練語料庫包含 1,252 道題目，源自高等教材，先由大語言模型自動重寫為我們定義的兩個子任務形式，再經人類專家細致審校。一個關鍵特點是，每道訓練題最多配有四條逐步解答路徑，為訓練大語言模型的細粒度推理提供了豐富數據。此外，76.8% 的訓練題目標注了與其解法相關的 83 個命名定理，涵蓋 29 個類別。如表 2 所示，IneqMath 在規模、多樣性以及與人類式非形式化解題方法的對齊程度上，均超越了以往資源。

然而，僅得出正確最終答案是不夠的，推理過程本身必須可靠。為此，我們提出了一個 “大語言模型作為評判者”（LLM-as-judge）的評估框架（§4）。該框架包含一個高精度的最終答案評判者，用于驗證答案等價性；并輔以四個專門的步驟級評判者，用于評估推理步驟的合理性。這些步驟級評判者旨在檢測我們在預實驗中識別出的常見推理缺陷：過度依賴玩具案例（toy case examples）、未處理的邏輯漏洞、未經論證的數值近似，以及數值計算錯誤。在人工標注的開發集解答上驗證表明，這些評判者具有高可靠性（平均 F1 > 0.9），為大規模審查大語言模型生成證明的演繹完整性提供了可擴展的方法。

我們在 29 個主流大語言模型上進行了系統評估（§5），涵蓋從通用聊天模型到先進推理模型，包括開源與閉源系統。如圖 1 所示，關鍵結果如下：盡管專用推理模型（如 o1 [45]）在最終答案準確率上優于通用聊天模型（如 GPT-4o [43]），但這種優勢在步驟級審查下往往大幅削弱。一旦我們的評判者逐條檢查推理步驟，整體準確率最多驟降 65.5%。事實上，即便是表現最佳的模型（如 o1），其整體準確率也低于 10%（見表 4），暴露出其演繹鏈條的脆弱性，以及“找到答案”與“構建嚴謹證明”之間的顯著差距。

我們的深入研究（§5.3）表明：盡管模型規模增大與最終答案準確率提升呈正相關，但對整體準確率的影響有限（例如 o1 的整體準確率僅為 8.0%）。同樣，通過延長推理鏈來增加測試時計算資源，在整體正確性上的收益也迅速遞減（例如，當 o1 的最大輸出 token 數從 5K 增至 40K 時，其整體準確率仍維持在 8.0%；而 o3 [48] 的準確率則在約 31% 處趨于飽和）。這些發現表明，當前的模型擴展策略不足以支撐 IneqMath 中所需的穩健演繹推理。

相反，我們探索了若干有前景的改進策略：例如定理引導推理（theorem-guided reasoning）——通過提供“黃金定理”（golden theorems），可使 o3-mini [47] 的整體準確率最高提升 11%；以及批評者引導的自我精煉（critic-guided self-refinement）——例如 Gemini 2.5 Pro [22] 的整體準確率實現了 5% 的絕對提升。

綜上所述，本工作做出四項核心貢獻：

1. 提出一種不等式證明的非形式化重構方法，將任務分解為兩個可驗證的子任務（§2）；
2. 發布 IneqMath——一個由專家整理的奧林匹克級別不等式基準測試集，以及一個富含逐步解答和定理標注的訓練語料庫（§3）；
3. 開發了一個模塊化的 LLM-as-judge 框架，可嚴格評估最終答案與證明步驟的合理性（§4）；
4. 開展了一項系統的實證研究（§5），揭示了大語言模型性能與數學嚴謹性之間的顯著差距，并指明了未來研究的方向。

2 任務形式化：一種非正式視角

然而，這種形式化方法要求使用者具備專業工具的使用經驗；而自然語言中的非正式證明雖然更符合直覺，卻因其非結構化的特性而難以自動驗證。

為應對這些挑戰，我們提出一種非正式視角，將不等式證明問題重新表述為兩個可驗證的子任務：界估計（bound estimation）與關系預測（relation prediction）。

這些子任務之所以被選用，是因為它們在數學問題求解中頻繁出現，能夠簡化評估流程，并且關鍵在于，它們保留了原始不等式證明問題所固有的核心推理挑戰。一個理想的 LLM 解答不僅應給出正確的最終答案，還應呈現清晰、邏輯嚴謹且完整的推導過程，包括策略性地應用定理、準確的符號操作與計算，以及對所有關鍵步驟的充分論證。

3 IneqMath：不等式問題數據集
本節描述 IneqMath 的數據整理過程及其關鍵統計信息。IneqMath 是一個新穎的不等式問題集合，旨在支持以非正式視角來求解和證明不等式。

測試數據整理。為減少來自常見來源（如教材、競賽和在線資源）的污染——這些內容可能已存在于大語言模型的訓練語料中——我們委托國際數學奧林匹克（IMO）級別的獎牌得主專門設計全新的不等式題目。這些題目隨后由另一個獨立專家小組進行嚴格評審，并僅在全體一致確認其可解性、推理合理性及標準答案正確性后才被采納。專家認為較簡單的題目被排除在測試集之外（轉用于開發集），以確保測試集具有較高難度。為進一步說明污染程度有限，我們還在 §C.8 中對測試集進行了記憶性探測（memorization probe）。相關數據整理工具詳見 §A.2。我們還搭建了一個在線評測網站1，為社區提供公平的評估平臺。

關鍵統計信息。如表 1 所示，IneqMath 數據集包含用于基準測試的 200 道測試題、100 道帶公開標準答案的開發題，以及 1,252 道訓練題，后者在界估計和關系預測兩個子任務之間平均分配。每道訓練題均配有逐步解答，最多包含四條不同解法；其中 76.8%（即 962 道）標注了相關定理。該數據集涵蓋了 29 個類別中的 83 個命名定理，其分布情況見圖 2。測試題示例見 §A.4。

與現有數據集的比較。如表 2 所總結，IneqMath 的突出特點在于：(1) 提供由專家精心整理的訓練集和測試集；(2) 提供豐富的標注信息，包括逐步解答和 83 個有明確依據的定理；(3) 采用一種非正式且易于使用的不等式證明格式，通過界估計和關系預測兩個子任務進行表述，并借助 LLM-as-judge 框架進行評估。這一設計彌合了形式化證明系統與直觀數學推理之間的鴻溝，使 IneqMath 成為推動大語言模型在問題求解與定理證明能力方面發展的獨特資源。

潛在污染聲明。為確保評估的嚴謹性，IneqMath 測試集由 IMO 級別的獎牌得主專門設計，包含全新題目，以最大程度減少大語言模型在預訓練階段接觸過相關內容的可能性。各類模型在該測試集上的普遍不佳表現（§5.2），尤其是在整體準確率方面（該指標要求每一步推理都正確），強烈表明該基準確實構成了顯著的推理挑戰，無論模型是否對底層數學概念存在一定程度的熟悉。因此，我們相信 IneqMath 測試集能夠有效探測模型在解決新問題方面的能力，我們關于當前大語言模型在嚴謹不等式證明方面存在局限性的結論是穩健的。

4 面向不等式求解的細粒度非正式評判器
IneqMath 數據集的測試部分構成我們的基準，包含 200 道奧林匹克級別的不等式題目，對人類和當前的大語言模型均構成挑戰。在此場景下，傳統評估方法存在不足：專家人工標注雖準確，但勞動成本過高；而字符串匹配或數值等價性等自動化技術則無法捕捉逐步推理的正確性——而這正是不等式求解的核心要素。

為解決這一問題，我們提出一種細粒度的 LLM-as-judge 框架（如圖 3 所示），包括一個用于驗證預測答案的最終答案評判者（§4.1）和四個專門針對常見推理缺陷的步驟級評判者（§4.2）。只有當一個解答通過全部五個評判者的檢驗時，才被視為整體正確。如表 3 所示，這些評判者與人工標注高度一致（F1 = 0.93），為手動評估提供了一種可擴展且可靠的替代方案。

4.1 最終答案評判者

4.2 四個步驟級評判者

邏輯漏洞評判者（Logical Gap Judge）。IneqMath 的不等式問題常涉及多步推導（如代數變換、約束優化、函數變換），需要明確的論證支持。然而，大語言模型往往跳過關鍵推理步驟，或在無依據的情況下直接斷言結論（例如，直接給出最優界而不提供推導過程）。現有步驟級評估方法 [68] 能評估有效性與冗余性，但對這類邏輯遺漏缺乏細粒度判斷。我們的邏輯漏洞評判者通過標記缺失的過渡步驟、無依據的斷言以及模糊的推導（特別是在涉及不等式變換或界估計的步驟中）來解決此問題（詳見 §B.3）。

4.3 評判器有效性驗證

整體性 LLM 評判基線。為凸顯我們專用評判系統的設計動機，我們首先評估一種啟發式的 LLM-as-judge 基線方法。該方法提示一個通用大語言模型，對 IneqMath 解答的整體正確性進行綜合判斷，同時考慮最終答案的準確性以及 §4.2 中所述四類推理缺陷的步驟級合理性。如圖 4 所示，在 80 個經人工標注的開發集樣例上構建的混淆矩陣表明，這種樸素方法與人類標注的一致性很差，凸顯了其在本領域嚴謹評估中的不可靠性。

細粒度評判器的性能。相比之下，我們提出的五位專用評判器組合與人類評估高度一致。圖 5 展示了在同一開發集上每位評判器的混淆矩陣。最終答案評判者（使用 GPT-4o-mini）實現了近乎完美的對齊，而四個步驟級評判者（根據性能與成本的平衡選定，詳見 §B.6）也表現出高保真度。這證實了：將復雜的評估任務分解為有針對性的子問題，可使大語言模型成為可靠的評估工具。

評判器分歧的定性分析。盡管整體表現優異（總體 F1 = 0.93，見表 3），LLM-as-judge 的評估并非完美無缺。鑒于學界對基于 LLM 的評估普遍存在疑慮，我們對評判器判斷與人工標注不一致的失敗案例進行了定性分析。詳細示例見 §B.7。這些案例表明，盡管我們的 LLM 評判器非常有效，但在涉及專家級數學推理所特有的深度與細微理解時，仍可能面臨挑戰。

5 IneqMath 實驗

5.1 實驗設置

我們在 IneqMath 測試集的不等式問題上，對 29 個主流大語言模型進行了系統性評估。所評估的模型涵蓋兩類：通用聊天模型（包括開源和閉源模型）以及專為復雜、多步問題求解設計的專用推理大語言模型。

所有模型均在零樣本（zero-shot）設置下進行提示，輸入包含問題陳述和指令：“請以清晰、嚴謹且邏輯嚴密的步驟解答該問題”，以鼓勵模型生成詳細推理過程。模型的輸出由我們提出的 LLM-as-judge 框架（§4）進行評估。

我們報告以下三項關鍵指標：

• Answer Acc（答案準確率）：衡量預測答案的正確性，由最終答案評判者（§4.1）驗證。
• Step Acc（步驟準確率）：匯總由四個專用步驟級評判者（§4.2）判定的各推理步驟的正確性，這些評判者針對常見的推理缺陷。
• Overall Acc（整體準確率）：主要評估指標，僅當解答同時滿足最終答案正確且所有推理步驟無瑕疵（即通過全部五個評判者）時，才視為正確。

因此，只有當模型通過邏輯有效的推理步驟得出正確最終答案，并通過所有評判者的審查時，其回答才被視為完全正確（Overall Acc）。更多實驗設置細節見 §C.1。

5.2 主要評估結果

表 4 展示了所評估大語言模型在 IneqMath 上的性能。我們的分析揭示了當前大語言模型在不等式證明能力方面的若干關鍵洞見：

1. 推理型大語言模型具有更高的最終答案準確率。例如，o1（答案準確率 62.5%）和 Grok 3 mini（71.5%）在識別正確最終答案方面顯著優于通用聊天模型（如 GPT-4o 的 37.5%、Grok 3 的 54.5%）。這表明專用架構或訓練方法提升了模型搜索并找到最終答案的能力。
2. 步驟級審查暴露出性能的急劇下降。答案準確率的優勢往往掩蓋了底層推理缺陷。一旦對推理步驟進行評估，整體準確率便大幅下滑。例如，Grok 3 mini 的準確率下降了 65.5%（從 71.5% 的答案準確率降至 6.0% 的整體準確率），o3-mini 下降了 53.0%。這種顯著差距凸顯了大語言模型生成的演繹鏈條的脆弱性。
3. 構建嚴謹證明仍是一大挑戰。即便是頂尖模型如 o1，其整體準確率也較低（8.0%）。許多大型模型盡管具備中等水平的答案準確率，整體表現依然不佳（例如 Grok 3 的整體準確率僅為 3.5%）。這表明，在“找到一個看似合理的答案”與“構建數學上嚴謹、逐步推導的證明”之間存在根本性鴻溝。

5.3 深入研究

錯誤解答分析。如表 4 所示（其中報告了整體準確率、最終答案準確率以及四類步驟級錯誤的平均錯誤率），大語言模型生成解答中最常見的步驟級錯誤是邏輯漏洞（各模型平均失敗率達 85.0%）和基于玩具案例的無根據泛化（59.7%）。數值近似錯誤（26.9%）和計算錯誤（6.8%）雖較少見，但仍具顯著影響。對錯誤解答的詳細檢查（見 §C.2.1–§C.2.4 中的示例）突顯了這些普遍存在的錯誤模式——即使模型得出了正確的最終答案，這些錯誤也常常破壞整個證明的嚴謹性。除步驟級錯誤外，大語言模型在復雜問題上也難以得出正確最終答案（§C.2.5），表明其在定理應用和符號操作方面面臨更深層次的挑戰。

模型規模的縮放規律。圖 6 展示了僅評估最終預測答案正確性時，大語言模型的最終答案準確率如何隨模型規模增長。隨著模型規模增大，答案準確率穩步提升，體現出一種經驗性的縮放規律：更大的模型更擅長推斷正確的界和不等式關系。然而，當考慮整體準確率（即同時要求答案正確和中間推理步驟有效）時，這一趨勢不再成立，如圖 7 所示。在此情況下，縮放曲線趨于平緩，表明僅靠增加模型規模不足以消除逐步推理中的錯誤。

測試時計算的縮放規律。延長測試時計算、允許更長的推理鏈，是解決復雜問題的常用策略 [14]。我們通過調整推理型大語言模型的最大生成 token 數，研究了其對 IneqMath 整體準確率的影響。圖 8 顯示，盡管像 Gemini 2.5 Pro 和 o3 這樣的模型在初期隨著 token 數增加而有所提升，但其性能增益很快趨于飽和（例如，超過 20K tokens 后）。這表明，單純增加計算預算對于獲得嚴謹且步驟正確的證明所能帶來的收益遞減，凸顯出僅靠延長“思考過程”是遠遠不夠的，亟需更有效的推理機制。

5.4探索改進策略

以相關定理作為提示（hints）。為評估基于定理的提示效果，我們在模型求解一個包含 40 道題目的測試子集時，為其提供來自 IneqMath 訓練語料中最常出現的 top-k 個定理。如圖 9 所示，對于較弱的模型（例如 Grok 3 mini、o3-mini、o4-mini），提供一到兩個此類定理反而會降低其整體準確率，這可能是因為模型誤用了這些定理，或被潛在不相關的信息干擾。相反，更強的模型（如 Gemini 2.5 Pro）則能從這些提示中獲益，表明高級推理能力對于有效利用此類指導至關重要。這些結果既凸顯了定理引導推理（theorem-guided reasoning）的潛力，也強調了亟需更精細的定理檢索機制（例如 RAG [28, 24]），以可靠地提升大語言模型在不等式證明中的表現。詳細實驗見 §C.4。

通過批評者反饋實現自我改進。已有研究表明，讓大語言模型對其自身推理進行批判并修訂，可提升其在復雜任務上的表現 [78, 57]。為探究這一方法是否適用于不等式證明，我們從 IneqMath 中隨機抽取了 40 道測試題，并執行了一輪自我批判（self-critique）。如圖 10 所示，自我批判持續提升了模型性能——例如，Gemini 2.5 Pro 的整體準確率從 43% 提高至 48%。這一上升趨勢表明，自我批判是一種有前景的、無需外部監督的方法，可有效增強大語言模型在不等式推理中的邏輯嚴謹性與解答質量。更多細節見 §C.5。

6 相關工作

不等式與定理證明的數據集。提升大語言模型在不等式證明方面能力的主要瓶頸之一是缺乏合適的數據集。現有資源在多個方面存在不足：通用自動定理證明器（ATP）數據集如 MiniF2F [82] 和 ProofNet [7] 中包含的不等式數量極少；合成數據集如 INT [64] 和 AIPS [63] 雖具規模，但由于基于模板生成，往往缺乏結構多樣性；而人工整理的數據集如 ChenNEQ [8] 通常規模過小，難以支撐大規模訓練。更根本的是，大多數現有數據集 [80, 59, 73, 29, 58, 26] 采用完全形式化的表示方式，將問題和證明編碼在 Lean [11] 或 Isabelle [42] 等系統中。盡管形式化數學推理能提供正確性保證，且是重要的研究方向，但大語言模型是在海量自然語言語料上訓練而成，通常展現出強大的非形式化推理能力。因此，我們的 IneqMath 采取一種非正式視角，將不等式證明問題重新表述為兩個可驗證的子任務——界估計（bound estimation）與關系預測（relation prediction）。IneqMath 中的問題均由 IMO 級別獎牌得主專家設計并審核。其他非形式化推理數據集 [49, 39, 23, 37] 通常缺乏標注的解答、定理引用或相應的訓練數據。為彌補這些空白，IneqMath 引入了 1,252 道用于訓練的不等式問題，每道題均標注了與其解法相關的定理，并最多包含四步的逐步解答。

不等式與定理證明的方法。不等式證明十分復雜，需要識別緊致界的直覺、策略性地運用定理，以及精確的符號操作。傳統的自動定理證明器（ATPs）主要在 Lean [11] 或 Isabelle [42] 等形式系統內運行，要求問題和證明以專用語言進行編碼。受大語言模型在數學推理方面能力的啟發 [81]，近期大量工作聚焦于將 LLM 與這些形式化 ATP 集成。這些方法通常將定理證明建模為馬爾可夫決策過程（MDP），訓練 LLM 在形式系統中選擇合適的策略（tactics）和前提以構建證明 [1, 9, 62, 16, 18, 26, 34, 61, 72]。例如，Goedel-Prover [35] 利用大規模 Lean 語料庫訓練模型進行策略預測，從而實現端到端的形式化證明生成。其他方法則結合樹搜索技術，在形式框架內探索前提的搜索空間 [65, 31, 70, 71]。

大語言模型在海量自然語言語料上的訓練使其在非形式化推理方面具有優勢——這更接近人類解決問題的方式。這揭示了一種利用此類非形式化能力的新機遇。我們的工作脫離了形式化范式，提出了一種非正式但可驗證的不等式證明框架，旨在對大語言模型在類人問題求解中的表現進行基準測試與提升，并探索如定理引導推理和自我精煉等改進策略。

用于數學問題求解的 LLM-as-judge 方法。可靠評估數學問題求解不僅需要判斷最終答案的正確性，還需評估每一步推理的邏輯合理性，這對自動化系統而言是一項重大挑戰。傳統方法往往不足：專家人工標注勞動密集且難以擴展至大規模評估 [49, 39]；而字符串匹配或數值等價性等自動化技術則忽略了逐步證明正確性的關鍵方面 [25, 23, 37, 38]。盡管大語言模型作為評判者（LLM-as-judge）已展現出潛力，其在細粒度、步驟級數學判斷方面的能力仍在發展中。例如，現有的步驟級 LLM 評判器 [68, 17] 可能評估步驟的一般有效性，但往往缺乏識別細微推理缺陷的粒度。類似地，EIC-Math [30] 等框架雖提供寬泛的錯誤類別，卻可能遺漏多步推導中微妙但關鍵的問題。為應對這些局限，并有效評估不等式求解等非形式化數學證明，我們的 LLM-as-judge 框架結合了一個最終答案評判者與四個專門針對常見錯誤的步驟級評判者：玩具案例過度泛化、邏輯漏洞、未經論證的數值近似，以及數值計算錯誤。

7 結論

綜上所述，我們提出了一種非正式但可驗證的不等式證明任務形式化方法，將其分解為界估計（bound estimation）與關系預測（relation prediction）兩個子任務。基于此，我們發布了 IneqMath——一個由專家精心整理的奧林匹克級別不等式基準數據集，其訓練語料庫包含逐步解答和定理標注。我們還開發了一種新穎的 LLM-as-judge 評估框架，包含一個最終答案評判者和四個步驟級評判者，從而實現對模型推理過程的嚴格評估。

我們對多種主流大語言模型的全面評估揭示了一個關鍵差距：盡管大語言模型可能在最終答案準確率上表現較高，但在步驟級審查下，這一指標最多驟降 65.5%，即便是頂尖模型如 o1，其整體準確率也低于 10%。這一差距暴露了當前大語言模型在構建嚴謹數學證明時所依賴的演繹鏈條的脆弱性。

此外，我們發現單純擴大模型規模或增加測試時計算資源對整體證明正確性的提升作用有限。相反，我們的研究結果指出了若干有前景的研究方向，例如定理引導推理（theorem-guided reasoning）和自我精煉（self-refinement）。

原文鏈接：https://arxiv.org/pdf/2506.07927v2