結合非形式化推理遞歸構建形式化證明

HILBERT:結合非形式化推理遞歸構建形式化證明

HILBERT: RECURSIVELY BUILDING FORMAL PROOFS WITHINFORMAL REASONING

https://arxiv.org/pdf/2509.22819?

摘要

大語言模型（LLMs）展現出令人印象深刻的數學推理能力，但其解決方案經常包含無法自動驗證的錯誤。形式化定理證明系統（如 Lean 4）提供了完全準確的自動化驗證，這促使近期研究致力于構建專門的證明器 LLM，以生成形式化語言中可驗證的證明。然而，一個顯著的差距仍然存在：當前的證明器 LLM 所解決的問題數量遠少于使用自然語言進行推理的通用 LLM。我們提出 HILBERT——一種智能體框架，通過結合非形式化推理與形式化驗證的互補優勢來彌合這一差距。我們的系統協調四個組件：一個擅長數學推理的非形式化 LLM、一個針對 Lean 4 戰術優化的專用證明器 LLM、一個形式化驗證器，以及一個語義定理檢索器。當證明器無法解決某個問題時，HILBERT 采用遞歸分解策略，將問題拆分為若干子目標，并利用證明器或推理型 LLM 分別求解。必要時，它利用驗證器的反饋對錯誤的證明進行修正。實驗結果表明，HILBERT 在關鍵基準上顯著優于現有方法，在 miniF2F 上達到 99.2% 的準確率，比當前最佳公開方法高出 6.6 個百分點；在 PutnamBench 上取得已知最佳結果，解決了 462/660 道題目（70.0%），優于 SeedProver 等閉源方法（50.4%），相比最佳公開基線提升了 422%。因此，HILBERT 有效縮小了非形式化推理與形式化證明生成之間的差距。

1 引言

通用大語言模型（LLMs）在數學理解方面取得了顯著進步。諸如 GPT-5 和 Gemini 2.5 Pro 等推理型 LLM 在高中奧林匹克競賽（如 AIME）上接近完美表現，并能解決相當比例的普特南（Putnam）競賽級別的本科難題（Dekoninck 等，2025）。這些系統在 FrontierMath 等研究級基準上也展現出潛力（Glazer 等，2024；OpenAI，2025）。

然而，幾個根本性限制嚴重制約了它們的實際效用。這些系統經常產生幻覺，輸出聽起來自信但最終錯誤的解答。即使最終答案正確，其底層推理也常常包含嚴重缺陷：例如“舉例證明”、邏輯謬誤、未經證實的假設以及計算錯誤（Petrov 等，2025；Guo 等，2025；Mahdavi 等，2025；Balunovi? 等，2025）。人工驗證生成的證明既耗時又困難，且容易出錯。盡管近期進展表明基于 LLM 的驗證器可接近人類水平（Guo 等，2025；Dekoninck 等，2025），但由于幻覺和靜默失敗（silent failures），它們仍不可靠（Mahdavi 等，2025；Petrov 等，2025）。

形式化定理證明系統（如 Lean 4；Moura 和 Ullrich，2021）通過實現完全準確的自動化證明驗證，提供了一種有前景的解決方案，能夠保證在形式化語言中證明或證偽證明的正確性。這一能力推動了專用證明器 LLM 的發展（Polu 和 Sutskever，2020），大量研究聚焦于開發用于生成 Lean 4 形式化證明的專用模型（Yang 等，2023；Xin 等，2024a,b, 2025；Ren 等，2025；Dong 和 Ma，2025；Wang 等，2025）。目前最佳的開源證明器模型在 miniF2F 上的通過率超過 90%（Zheng 等，2021），并在具有挑戰性的 PutnamBench（Tsoukalas 等，2024）657 道題中解決了 86 道。AlphaProof（AlphaProof 和 AlphaGeometry，2024）和 SeedProver（Chen 等，2025）等閉源系統展示了該范式的潛力，在國際數學奧林匹克（IMO）問題上取得了銀牌水平的表現。

盡管取得上述進展，專用證明器 LLM 與通用推理 LLM 之間仍存在顯著性能差距。例如，Dekoninck 等（2025）通過人工驗證發現，推理型 LLM 可非形式化地解決約 83% 的 PutnamBench 問題，而當前最佳公開的證明器 LLM 僅能用形式化證明解決其中的 13%。通用 LLM 擅長非形式化數學推理，并且對形式化語言語法的理解足以寫出有效的證明草稿和簡短證明（Ren 等，2025；Liang 等，2025）。然而，它們在完整的形式化程序合成方面表現不佳，在 miniF2F 上即使嘗試 16384 次也僅達到 49.1% 的通過率（Zhou 等，2025b）。相反，專用證明器 LLM 擅長為獨立定理生成語法正確的形式化證明，但在依賴語言能力的任務（如利用已有定理或錯誤修正）上表現脆弱（Liang 等，2025）。

為彌合這一差距，一些研究探索了利用通用 LLM 的非形式化推理能力來增強形式化定理證明。早期方法如 DSP（Jiang 等，2022）和 LEGO-Prover（Wang 等，2023）使用通用 LLM 提出證明草稿，再由自動定理證明器（ATP）填充形式化部分，但受限于基于啟發式的 ATP 能力。DSP+（Cao 等，2025）在此基礎上使用現代證明器 LLM 處理中間步驟。然而，這些方法因采用淺層、單層分解策略，在處理復雜子目標時表現不佳——它們雖能分解原始問題，卻無法進一步分解那些仍難以直接求解的子目標。近期的智能體框架（如 COPRA（Thakur 等，2024）、Prover-Agent（Baba 等，2025）和 ProofCompass（Wischermann 等，2025））利用非形式化推理并結合形式化驗證器的反饋迭代構造證明。盡管這些方法展現出潛力，其性能仍顯著落后于通用推理 LLM。

我們提出 HILBERT——一種將非形式化推理與形式化驗證相結合的智能體框架（見圖 1）。它協調四個核心組件：一個通用推理 LLM、一個證明器 LLM、一個驗證器和一個語義定理檢索器。給定一個數學問題，HILBERT 首先從 Mathlib（mathlib Community，2020）中檢索相關定理，并使用推理器生成詳細的非形式化證明。隨后，它創建一個 Lean 4 證明草稿，將問題分解為可管理的子目標。對于每個子目標，HILBERT 采用兩階段策略：首先嘗試用證明器生成形式化證明，若失敗則回退到結合檢索定理增強的推理器。當兩個階段均失敗時，系統會遞歸地將有問題的子目標進一步分解為更小的問題。在整個過程中，HILBERT 利用推理器在推理時解釋編譯錯誤、建議修正方案并指導證明精煉。我們總結主要貢獻如下：

• 我們設計了 HILBERT——一個多輪次智能體框架，系統性地結合非形式化數學推理與形式化證明驗證，彌合了這兩種范式之間的性能差距。
• 我們在 MiniF2F 和 PutnamBench 上進行了全面實驗，在兩個基準上均取得當前最優性能：HILBERT 在 miniF2F 上達到 99.2% 的通過率（比最佳公開方法高 6.6 個百分點），并在 PutnamBench 上解決了 462/660 道題（70.0%），優于 SeedProver 等閉源系統（50.4%），相比最佳開源基線提升超過 4 倍。
• 通過廣泛的消融實驗，我們驗證了關鍵技術的有效性：用于分解復雜證明的遞歸分解流程，以及用于增強推理能力的檢索增強生成機制。

2 相關工作

自動定理證明器（ATPs） 是旨在自動發現數學定理證明的計算系統。傳統方法主要依賴符號推理方法（Robinson, 1965；McCune, 2003；Schulz, 2002）以及像 Sledgehammer 這樣的集成工具，后者將 ATPs 與交互式證明助手連接起來（Blanchette 等，2013；Czajka 和 Kaliszyk，2018）。近期，大語言模型（LLMs）作為一種有前景的新工具被引入自動定理證明領域（Polu 和 Sutskever，2020；Yang 等，2024）。

證明器 LLMs。其基本原理是在大規模形式化證明數據集上訓練專用的證明器 LLM，其中最突出的是面向 Lean 定理證明器（Moura 和 Ullrich，2021）的模型。一些代表性模型包括 GPT-f（Polu 和 Sutskever，2020）、ReProver（Yang 等，2023）、DeepSeek Prover 系列模型（Xin 等，2024a,b；Ren 等，2025）、ABEL（Gloeckle 等，2024）、Goedel Prover V1 和 V2（Lin 等，2025a,b）、BFS Prover（Xin 等，2025）、STP-Prover（Dong 和 Ma，2025）以及 Kimina Prover（Wang 等，2025）。這些模型通過整理大量形式化證明語料庫，并結合監督微調和強化學習進行訓練。若干方法通過在訓練過程中引入子目標分解來增強這些模型（Zhao 等，2023, 2024；Ren 等，2025），而 POETRY（Wang 等，2024）和 ProD-RL（Dong 等，2024）則采用遞歸問題分解策略。閉源的證明器 LLM 如 AlphaProof（AlphaProof 和 AlphaGeometry，2024）和 SeedProver（Chen 等，2025）進一步推動了該領域的前沿，在國際數學奧林匹克（IMO）問題上取得了銀牌水平的表現。盡管如此，專用證明器模型與通用 LLM 在數學推理能力方面仍存在顯著性能差距（Dekoninck 等，2025）。

使用非形式化 LLM 進行形式化定理證明。若干先前工作嘗試利用通用 LLM 的非形式化推理能力來提升形式化推理能力。DSP（Jiang 等，2022）使用 Codex LLM 在 Isabelle 中提出證明草稿，中間步驟由 Sledgehammer 填充。LEGO-Prover（Wang 等，2023）將該框架擴展至處理一個不斷增長的中間定理技能庫，用于檢索增強的證明。Liang 等（2025）指出，通用推理型 LLM 在將問題分解為更簡單子目標方面比證明器 LLM 更有效。我們的工作在此觀察基礎上進一步推進，利用非形式化推理器遞歸地構建證明草稿，將問題分解為可由證明器或推理型 LLM 處理的更簡單子問題。

若干研究還提出在智能體框架中使用非形式化 LLM 進行自動定理證明。COPRA（Thakur 等，2024）通過查詢非形式化 LLM 逐個生成證明策略（tactic），并將執行反饋、搜索歷史和檢索到的引理整合到后續提示中。Prover-Agent（Baba 等，2025）使用一個小型非形式化推理模型生成證明步驟和引理，這些內容被自動形式化后由證明器 LLM 求解。Lean 的反饋被用于迭代修正錯誤的證明。ProofCompass（Wischermann 等，2025）通過在輸入中添加非形式化證明步驟作為注釋來增強證明器 LLM。當證明嘗試失敗時，它分析這些失敗以提取中間引理，從而實現有效的問題分解。DeltaProver（Zhou 等，2025b）引入了一種自定義的領域特定語言（DSL）來進行子目標分解，并利用驗證器反饋迭代修復生成的證明。值得注意的是，它僅使用非形式化 LLM，不依賴證明器 LLM。相比之下，我們的工作表明，當在適當設計的多智能體框架中協調調度時，證明器 LLM 會成為極為有效的工具。

3 HILBERT 系統

在本節中，我們詳細介紹 HILBERT——一種多智能體系統，通過協調通用推理型大語言模型（LLM）與專用證明器 LLM，彌合非形式化數學推理與形式化驗證之間的鴻溝。我們的方法采用遞歸子目標分解策略，將復雜定理拆解為更簡單的子目標，這些子目標可被分別證明并組合起來，從而實現超越任一方法單獨使用時的性能。

3.1 組件

在描述推理算法之前，我們首先介紹 HILBERT 所協調的各個組件。

推理器（Reasoner）：一個通用推理型 LLM，用于撰寫非形式化證明、Lean 中的證明草稿，在某些情況下也可生成形式化證明。在我們的工作中，我們使用 Google Gemini 2.5 Flash 和 Pro（Comanici 等，2025），因其具備卓越的數學推理能力（Zhou 等，2025b；Dekoninck 等，2025）。

證明器（Prover）：一個專用的證明器 LLM，用于在給定形式化定理陳述的情況下生成形式化證明。在我們的工作中，我們使用 DeepSeek-V2-7B（Ren 等，2025）和 Goedel-Prover-V2 32B（Lin 等，2025b）。

驗證器（Verifier）：一個形式化語言驗證器，用于檢查定理陳述和證明的正確性。我們使用 Kimina Lean 服務器（Santos 等，2025），其基于 Lean v4.15.0 和 Mathlib v4.15.0。

檢索器（Retriever）：一個語義搜索引擎，用于從 Mathlib（mathlib Community，2020）中檢索相關定理。該系統基于 sentence transformers（all-mpnet-base-v2；Song 等，2020）和 FAISS（Douze 等，2024）索引構建。系統計算查詢嵌入與 mathlib_informal 數據集（Gao 等，2024）中非形式化定理描述的預計算嵌入之間的余弦相似度，從而提供一種簡單而有效的替代方案，避免了使用定制的檢索模型（Gao 等，2024；Lu 等，2025）。

3.2 算法

給定一個 Lean 4 中的形式化陳述，我們首先嘗試使用 證明器（Prover） 直接證明。它生成 K initial proof = 4 個候選證明，我們使用 驗證器（Verifier） 對其進行驗證。如果其中任意一個證明有效，我們立即返回該證明。當直接證明嘗試失敗時，我們使用 推理器（Reasoner） 將問題分解為更簡單的子問題，并將它們組合成一個有效的證明策略。圖 2 概述了這一階段。

3.2.1 子目標分解

步驟 1（定理檢索）給定形式化陳述，我們提示推理器生成 s = 5 個搜索查詢，以查找可能有助于簡化證明策略的定理。對于每個搜索查詢，我們使用 檢索器（Retriever） 從 Mathlib 中檢索前 m = 5
個語義最相似的定理和策略（tactics）。隨后，我們再次提示推理器從檢索到的結果中僅選擇相關的定理。

步驟 2（形式化證明草稿生成）我們提示推理器利用檢索到的定理生成一份詳細的非形式化證明。在此證明作為上下文提供的基礎上，我們要求推理器生成一個 Lean 4 證明草稿，將問題分解為以 have 語句表示的更簡單子問題。所有子目標最初都用 sorry 填充——這是 Lean 中的一個占位符關鍵字，可被臨時視為子目標的證明。我們使用驗證器驗證該證明草稿是否有效，并利用其反饋修正任何錯誤。對于每個輸入定理，我們最多生成 K sketch attempts = 4 次草稿嘗試。

步驟 3（子目標提取）推理器從證明草稿中提取子目標，將其轉換為獨立的定理陳述，并附加上原始問題及先前子目標的相關上下文。如前所述，證明部分仍使用 sorry。我們通過統計證明草稿中的 have 語句數量并確保全部被提取，來驗證提取的完整性。若發現缺失，我們提示推理器提取遺漏的子目標。每個提取出的定理均通過驗證器進行語法驗證。當出現錯誤時，我們將錯誤信息作為上下文提供給推理器以進行修正。該方法比直接解析源代碼或從 Lean 4 的證明狀態數據結構（InfoTree）中提取子目標更為可靠（Liang 等，2025）。

步驟 4（基于子目標的證明組裝）我們將提取出的子目標定理陳述（包含 sorry 占位符）和已驗證的證明草稿提供給推理器。推理器通過將證明草稿中的每個 sorry 占位符替換為對應子目標定理的調用，生成目標定理的完整組裝證明。隨后，我們使用驗證器同時驗證子目標定理陳述和組裝后的證明，以確保整體結構正確。我們通過驗證器檢查錯誤，并通過與推理器的迭代反饋進行修正。這保證了：一旦所有子目標被證明，我們就得到了給定定理的完整證明。

3.2.2 子目標驗證

至此，我們已獲得一個有效的定理證明結構，以及一組子目標——只要這些子目標被證明，即可完成原始證明。然而，這些子目標的數學正確性與可證性尚未驗證。針對每個子目標，我們執行以下驗證與證明流程：

步驟 1（證明器嘗試）我們首先嘗試使用 證明器 直接證明每個子目標，生成 K formal proof = 4

個候選證明，并用驗證器進行驗證。若任一生成的證明有效，則接受該證明并繼續處理下一個子目標。

步驟 2（正確性驗證）對于無法直接證明的子目標，我們提示推理器評估該子目標在數學上是否正確，以及其形式化陳述是否表述恰當且可證。如果推理器判定該子目標在數學上不正確、不可證或表述不當，我們將其標記為需修正，并返回以優化原始證明草稿，從第 3.2.1 節開始重復所有步驟，并將識別出的問題作為反饋納入。除數學錯誤外，推理器在此階段檢測到的一些常見失敗模式包括：子目標定理陳述中缺少假設或條件，以及由 Lean 類型系統引起的異常行為（例如自然數截斷）3。

我們優先采用證明器嘗試而非推理器驗證，因為證明器模型計算成本更低，且一個有效的證明可自動確認數學正確性。經驗表明，大量生成的子目標可被證明器成功證明。步驟 1 確保我們在成功證明的子目標上節省了昂貴的推理器模型用于驗證的計算開銷。

步驟 3（淺層求解）在步驟 1 失敗且步驟 2 確認子目標正確的前提下，我們采用推理器模型進行“淺層求解”（shallow solve）：為證明器無法直接解決的子目標編寫簡短證明。我們從 Mathlib 庫中檢索相關定理，并要求推理器為該子目標編寫形式化證明。推理器根據驗證器反饋最多進行 K proof correction = 6

輪迭代修正。當編譯錯誤表明缺少或引用了錯誤的定理時，我們會檢索額外的相關定理。為節省計算資源，若某錯誤證明超過長度閾值 K max shallow solve length = 30 行，我們即終止此步驟——因為過長的證明表明需要進一步分解。整個淺層求解過程最多重復 K informal passes = 6
次，直至獲得成功證明或耗盡所有嘗試次數。

步驟 4（遞歸分解與證明組裝）若經過步驟 1–3 后仍有子目標未被證明，我們遞歸地應用子目標分解流程（第 3.2.1 節）對其進行進一步拆分。每個子目標被持續細分，直至被成功證明，或達到最大遞歸深度 D 。一旦所有子目標均被證明，我們通過拼接所有子目標的證明與第 3.2.1 節步驟 4 中生成的組裝證明大綱，構建給定定理的完整證明。具體做法是將子目標的證明與第 3.2.1 節步驟 4 產生的組裝證明進行拼接。若此時仍有未解決的子目標，則觸發證明失敗，促使我們重新啟動該定理的子目標分解流程。

完整算法見算法 1。關于實現細節，特別是并行化策略，請參見附錄 A.3。

4 實驗結果

4.1 主要結果

MiniF2F。MiniF2F 數據集（Zheng 等，2021）包含 488 道高中數學競賽題目，其中部分題目特別具有挑戰性，源自 AMC、AIME 和 IMO 競賽。我們在 MiniF2F 測試集劃分中的 244 道題目上進行基準測試。所有實驗均采用遞歸深度 D = 5
。對于證明器（Prover），我們在 HILBERT 中實例化了兩個 LLM：DeepSeek-Prover-V2-7B（Ren 等，2025），代表能力相對較弱的模型；以及 Goedel-Prover-V2-32B（Lin 等，2025b），代表能力更強的模型。這種配對使我們能夠比較不同能力水平下的性能表現。對于推理器（Reasoner），我們相應地采用了 Google 的 Gemini 2.5 Flash 和 Gemini 2.5 Pro（Comanici 等，2025）。結果見表 1。

HILBERT 在所有模型配置下均展現出強勁性能。我們表現最佳的配置組合為 Gemini 2.5 Pro 與 Goedel-Prover-V2-32B，達到了 99.2% 的通過率，僅在兩道題目上失敗（AMC 12A 2020 第 25 題和 IMO Shortlist 2007 A6 題）。即使使用較弱的形式化證明器，HILBERT 仍保持出色結果：將 DeepSeek-Prover-V2-7B 與 Gemini 2.5 Pro 配對可達到 98.4%，而使用 Gemini 2.5 Flash 則達到 96.7%。值得注意的是，非形式化推理器的選擇似乎比證明器強度更為關鍵。Gemini 2.5 Pro 在各類配置中始終比 Flash 版本高出 3–4%，這一差距大于不同證明器模型之間觀察到的性能差異。

與獨立的基礎證明器在 pass@4 指標下的表現相比，我們的方法帶來了顯著提升，改進幅度介于 20.1% 至 37.1% 之間。

PutnamBench。PutnamBench 是一個具有挑戰性的定理證明基準，包含 1962 年至 2024 年間威廉·洛厄爾·普特南數學競賽（William Lowell Putnam Mathematical Competition）的 660 道題目。該數據集涵蓋代數、分析、數論、幾何、線性代數、組合數學、抽象代數、概率論和集合論等本科水平的數學問題。鑒于在此數據集上評估的高昂計算成本，我們僅使用 HILBERT 的最強配置進行實驗（即 HILBERT 搭配 Gemini 2.5 Pro 和 Goedel-Prover-V2-32B）。如前所述，我們設定遞歸深度 D = 5
。結果見表 2。

HILBERT 在 PutnamBench 上取得了當前最優性能，成功解決了 660 道題中的 462 道（通過率為 70.0%）。這一結果比此前最佳方法——閉源的 SeedProver（50.4%）——高出近 20 個百分點。HILBERT 解決的問題數量超過最接近的公開基線模型 Goedel-Prover-V2-32B 達五倍以上。我們將這一成功歸因于 HILBERT 能夠組合長篇證明（見圖 9），而不會受到傳統 LLM 所面臨的長上下文推理問題的困擾（Zhou 等，2025a）。

4.2 推理時計算資源的擴展行為

與傳統證明器 LLM 將計算資源分配到大量從零開始的獨立證明嘗試不同，HILBERT 將推理時的計算資源分配到多個相互關聯的階段，從子目標分解到子目標證明生成。由于這種計算資源分配是自適應的，無法通過簡單的獨立嘗試次數來衡量。

為說明計算開銷與性能之間的權衡關系，我們繪制了 HILBERT 的通過率（pass rate）隨每樣本調用次數的變化曲線：(1) 僅調用推理器（Reasoner）的次數，以及 (2) 推理器與證明器（Reasoner + Prover）聯合調用的總次數（見圖 3）。結果顯示出清晰的擴展關系：每樣本的調用次數越多，通過率越高。我們表現最佳的配置（Gemini 2.5 Pro 搭配 Goedel Prover）最多需要約 4.5K 次推理器調用和 11.3K 次總調用，顯著少于 DeltaProver 在使用 Gemini 2.5 Pro 時所需的 16,384 次調用。

有趣的是，較弱的推理器（Gemini 2.5 Flash）為了在兩種證明器配置下達到相近的性能，需要明顯更高的推理計算預算。雖然 HILBERT + DeepSeek Prover 初始通過率較低，但在低計算預算場景下展現出更快的提升速度，最終能夠匹配 HILBERT + Goedel-Prover 的性能。

關于通過率與證明器/驗證器調用次數及總 token 使用量的更多分析，請參見附錄 A.6。

4.3 消融研究

性能（vs）遞歸深度。為評估子目標分解的有效性，我們在 MiniF2F 數據集上分析了使用 Gemini 2.5 Pro + Goedel-Prover-V2-32B 的 HILBERT 在不同遞歸深度 D D 下的通過率。基線（ D = 0
）對應無分解情形，此時我們報告獨立證明器（pass@4）的性能。我們比較兩種配置：完整的 HILBERT 系統，以及一個禁用淺層求解（shallow solving）的變體（即設 K informal passes = 0）。該變體僅依賴證明器來解決子目標。

圖 4 展示了不同 D D 值下的性能表現，清楚表明子目標分解帶來了顯著增益。兩種配置的性能均隨深度單調遞增，但呈現出不同的收斂模式。完整的 HILBERT 系統在較淺深度即獲得快速性能提升：在 D = 2
時達到 98.36%，到 D = 3 時已達 98.7%。相比之下，無淺層求解的變體需要更大的深度才能達到相近性能，凸顯了淺層求解機制的重要性。相較于 D = 0 基線（通過率 75%），性能持續提升，驗證了分層子目標分解的有效性；完整系統在相對較小的深度下即可實現接近最優的性能。

檢索消融實驗。為評估檢索器（Retriever）對性能和計算效率的影響，我們將 HILBERT 與一個省略檢索步驟的變體進行比較。我們在 MiniF2F 上針對兩種證明器配置進行實驗：DeepSeek-Prover-V2-7B 和 Goedel-Prover-V2-32B。結果見表 3。

啟用檢索時，HILBERT 在兩種配置下均取得更高的通過率：對于 DeepSeek Prover，98.4% 對比 97.1%；對于 Goedel Prover，99.2% 對比 97.9%。更重要的是，檢索顯著降低了推理時的計算資源消耗。對于 DeepSeek 模型，檢索將推理器調用次數從 426 降至 420，平均證明器調用次數從 290 降至 205，平均推理器 token 使用量從 210 萬降至 190 萬。在 Goedel Prover 上，效率提升更為顯著：檢索將平均推理器調用次數從 862 降至 548，平均推理器 token 使用量從 400 萬降至 230 萬。

這些結果表明，檢索通過提供有助于簡化證明的有用定理，并避免因引用錯誤定理名稱而導致的失敗，同時提升了性能與效率。

5 結論

我們提出了 HILBERT——一種分層的智能體框架，它將 Lean 中的形式化定理證明與通用大語言模型（LLM）的非形式化數學推理能力相結合。我們的方法通過遞歸地將復雜問題分解為可管理的子目標，并協調非形式化推理器（Gemini 2.5 Pro/Flash）與形式化證明器（DeepSeek-Prover-V2-7B 和 Goedel-Prover-V2-32B），共同解決任一組件單獨無法處理的定理。HILBERT 在 miniF2F 上取得了當前最優性能，通過率介于 94.7% 至 99.2%。在具有挑戰性的 PutnamBench 數據集上，HILBERT 達到 70.0% 的通過率，比此前最佳方法高出近 20 個百分點，并接近 Dekoninck 等人（2025）報告的 82% 的非形式化證明率。

未來，我們計劃利用該框架訓練能力日益增強的模型。HILBERT 生成的證明和推理軌跡可用于訓練更強大的證明器（Prover）和推理器（Reasoner）模型。這些改進后的模型將能夠解決比以往更復雜的問題，從而形成一個良性循環，有望持續推動形式化推理能力的進步。

原文鏈接： https://arxiv.org/pdf/2509.22819?