HILBERT:結(jié)合非形式化推理遞歸構(gòu)建形式化證明

HILBERT: RECURSIVELY BUILDING FORMAL PROOFS WITHINFORMAL REASONING

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

摘要

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

1 引言

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

然而，幾個(gè)根本性限制嚴(yán)重制約了它們的實(shí)際效用。這些系統(tǒng)經(jīng)常產(chǎn)生幻覺(jué)，輸出聽(tīng)起來(lái)自信但最終錯(cuò)誤的解答。即使最終答案正確，其底層推理也常常包含嚴(yán)重缺陷：例如“舉例證明”、邏輯謬誤、未經(jīng)證實(shí)的假設(shè)以及計(jì)算錯(cuò)誤（Petrov 等，2025；Guo 等，2025；Mahdavi 等，2025；Balunovi? 等，2025）。人工驗(yàn)證生成的證明既耗時(shí)又困難，且容易出錯(cuò)。盡管近期進(jìn)展表明基于 LLM 的驗(yàn)證器可接近人類(lèi)水平（Guo 等，2025；Dekoninck 等，2025），但由于幻覺(jué)和靜默失�。╯ilent failures），它們?nèi)圆豢煽浚∕ahdavi 等，2025；Petrov 等，2025）。

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

盡管取得上述進(jìn)展，專(zhuān)用證明器 LLM 與通用推理 LLM 之間仍存在顯著性能差距。例如，Dekoninck 等（2025）通過(guò)人工驗(yàn)證發(fā)現(xiàn)，推理型 LLM 可非形式化地解決約 83% 的 PutnamBench 問(wèn)題，而當(dāng)前最佳公開(kāi)的證明器 LLM 僅能用形式化證明解決其中的 13%。通用 LLM 擅長(zhǎng)非形式化數(shù)學(xué)推理，并且對(duì)形式化語(yǔ)言語(yǔ)法的理解足以寫(xiě)出有效的證明草稿和簡(jiǎn)短證明（Ren 等，2025；Liang 等，2025）。然而，它們?cè)谕暾男问交绦蚝铣煞矫姹憩F(xiàn)不佳，在 miniF2F 上即使嘗試 16384 次也僅達(dá)到 49.1% 的通過(guò)率（Zhou 等，2025b）。相反，專(zhuān)用證明器 LLM 擅長(zhǎng)為獨(dú)立定理生成語(yǔ)法正確的形式化證明，但在依賴(lài)語(yǔ)言能力的任務(wù)（如利用已有定理或錯(cuò)誤修正）上表現(xiàn)脆弱（Liang 等，2025）。

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

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

• 我們?cè)O(shè)計(jì)了 HILBERT——一個(gè)多輪次智能體框架，系統(tǒng)性地結(jié)合非形式化數(shù)學(xué)推理與形式化證明驗(yàn)證，彌合了這兩種范式之間的性能差距。
• 我們?cè)?MiniF2F 和 PutnamBench 上進(jìn)行了全面實(shí)驗(yàn)，在兩個(gè)基準(zhǔn)上均取得當(dāng)前最優(yōu)性能：HILBERT 在 miniF2F 上達(dá)到 99.2% 的通過(guò)率（比最佳公開(kāi)方法高 6.6 個(gè)百分點(diǎn)），并在 PutnamBench 上解決了 462/660 道題（70.0%），優(yōu)于 SeedProver 等閉源系統(tǒng)（50.4%），相比最佳開(kāi)源基線提升超過(guò) 4 倍。
• 通過(guò)廣泛的消融實(shí)驗(yàn)，我們驗(yàn)證了關(guān)鍵技術(shù)的有效性：用于分解復(fù)雜證明的遞歸分解流程，以及用于增強(qiáng)推理能力的檢索增強(qiáng)生成機(jī)制。

2 相關(guān)工作

自動(dòng)定理證明器（ATPs） 是旨在自動(dòng)發(fā)現(xiàn)數(shù)學(xué)定理證明的計(jì)算系統(tǒng)。傳統(tǒng)方法主要依賴(lài)符號(hào)推理方法（Robinson, 1965；McCune, 2003；Schulz, 2002）以及像 Sledgehammer 這樣的集成工具，后者將 ATPs 與交互式證明助手連接起來(lái)（Blanchette 等，2013；Czajka 和 Kaliszyk，2018）。近期，大語(yǔ)言模型（LLMs）作為一種有前景的新工具被引入自動(dòng)定理證明領(lǐng)域（Polu 和 Sutskever，2020；Yang 等，2024）。

證明器 LLMs。其基本原理是在大規(guī)模形式化證明數(shù)據(jù)集上訓(xùn)練專(zhuān)用的證明器 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）。這些模型通過(guò)整理大量形式化證明語(yǔ)料庫(kù)，并結(jié)合監(jiān)督微調(diào)和強(qiáng)化學(xué)習(xí)進(jìn)行訓(xùn)練。若干方法通過(guò)在訓(xùn)練過(guò)程中引入子目標(biāo)分解來(lái)增強(qiáng)這些模型（Zhao 等，2023, 2024；Ren 等，2025），而 POETRY（Wang 等，2024）和 ProD-RL（Dong 等，2024）則采用遞歸問(wèn)題分解策略。閉源的證明器 LLM 如 AlphaProof（AlphaProof 和 AlphaGeometry，2024）和 SeedProver（Chen 等，2025）進(jìn)一步推動(dòng)了該領(lǐng)域的前沿，在國(guó)際數(shù)學(xué)奧林匹克（IMO）問(wèn)題上取得了銀牌水平的表現(xiàn)。盡管如此，專(zhuān)用證明器模型與通用 LLM 在數(shù)學(xué)推理能力方面仍存在顯著性能差距（Dekoninck 等，2025）。

使用非形式化 LLM 進(jìn)行形式化定理證明。若干先前工作嘗試?yán)猛ㄓ?LLM 的非形式化推理能力來(lái)提升形式化推理能力。DSP（Jiang 等，2022）使用 Codex LLM 在 Isabelle 中提出證明草稿，中間步驟由 Sledgehammer 填充。LEGO-Prover（Wang 等，2023）將該框架擴(kuò)展至處理一個(gè)不斷增長(zhǎng)的中間定理技能庫(kù)，用于檢索增強(qiáng)的證明。Liang 等（2025）指出，通用推理型 LLM 在將問(wèn)題分解為更簡(jiǎn)單子目標(biāo)方面比證明器 LLM 更有效。我們的工作在此觀察基礎(chǔ)上進(jìn)一步推進(jìn)，利用非形式化推理器遞歸地構(gòu)建證明草稿，將問(wèn)題分解為可由證明器或推理型 LLM 處理的更簡(jiǎn)單子問(wèn)題。

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

3 HILBERT 系統(tǒng)

在本節(jié)中，我們?cè)敿?xì)介紹 HILBERT——一種多智能體系統(tǒng)，通過(guò)協(xié)調(diào)通用推理型大語(yǔ)言模型（LLM）與專(zhuān)用證明器 LLM，彌合非形式化數(shù)學(xué)推理與形式化驗(yàn)證之間的鴻溝。我們的方法采用遞歸子目標(biāo)分解策略，將復(fù)雜定理拆解為更簡(jiǎn)單的子目標(biāo)，這些子目標(biāo)可被分別證明并組合起來(lái)，從而實(shí)現(xiàn)超越任一方法單獨(dú)使用時(shí)的性能。

3.1 組件

在描述推理算法之前，我們首先介紹 HILBERT 所協(xié)調(diào)的各個(gè)組件。

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

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

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

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

3.2 算法

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

3.2.1 子目標(biāo)分解

步驟 1（定理檢索）給定形式化陳述，我們提示推理器生成 s = 5 個(gè)搜索查詢(xún)，以查找可能有助于簡(jiǎn)化證明策略的定理。對(duì)于每個(gè)搜索查詢(xún)，我們使用 檢索器（Retriever） 從 Mathlib 中檢索前 m = 5
個(gè)語(yǔ)義最相似的定理和策略（tactics）。隨后，我們?cè)俅翁崾就评砥鲝臋z索到的結(jié)果中僅選擇相關(guān)的定理。

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

步驟 3（子目標(biāo)提�。�推理器從證明草稿中提取子目標(biāo)，將其轉(zhuǎn)換為獨(dú)立的定理陳述，并附加上原始問(wèn)題及先前子目標(biāo)的相關(guān)上下文。如前所述，證明部分仍使用 sorry。我們通過(guò)統(tǒng)計(jì)證明草稿中的 have 語(yǔ)句數(shù)量并確保全部被提取，來(lái)驗(yàn)證提取的完整性。若發(fā)現(xiàn)缺失，我們提示推理器提取遺漏的子目標(biāo)。每個(gè)提取出的定理均通過(guò)驗(yàn)證器進(jìn)行語(yǔ)法驗(yàn)證。當(dāng)出現(xiàn)錯(cuò)誤時(shí)，我們將錯(cuò)誤信息作為上下文提供給推理器以進(jìn)行修正。該方法比直接解析源代碼或從 Lean 4 的證明狀態(tài)數(shù)據(jù)結(jié)構(gòu)（InfoTree）中提取子目標(biāo)更為可靠（Liang 等，2025）。

步驟 4（基于子目標(biāo)的證明組裝）我們將提取出的子目標(biāo)定理陳述（包含 sorry 占位符）和已驗(yàn)證的證明草稿提供給推理器。推理器通過(guò)將證明草稿中的每個(gè) sorry 占位符替換為對(duì)應(yīng)子目標(biāo)定理的調(diào)用，生成目標(biāo)定理的完整組裝證明。隨后，我們使用驗(yàn)證器同時(shí)驗(yàn)證子目標(biāo)定理陳述和組裝后的證明，以確保整體結(jié)構(gòu)正確。我們通過(guò)驗(yàn)證器檢查錯(cuò)誤，并通過(guò)與推理器的迭代反饋進(jìn)行修正。這保證了：一旦所有子目標(biāo)被證明，我們就得到了給定定理的完整證明。

3.2.2 子目標(biāo)驗(yàn)證

至此，我們已獲得一個(gè)有效的定理證明結(jié)構(gòu)，以及一組子目標(biāo)——只要這些子目標(biāo)被證明，即可完成原始證明。然而，這些子目標(biāo)的數(shù)學(xué)正確性與可證性尚未驗(yàn)證。針對(duì)每個(gè)子目標(biāo)，我們執(zhí)行以下驗(yàn)證與證明流程：

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

個(gè)候選證明，并用驗(yàn)證器進(jìn)行驗(yàn)證。若任一生成的證明有效，則接受該證明并繼續(xù)處理下一個(gè)子目標(biāo)。

步驟 2（正確性驗(yàn)證）對(duì)于無(wú)法直接證明的子目標(biāo)，我們提示推理器評(píng)估該子目標(biāo)在數(shù)學(xué)上是否正確，以及其形式化陳述是否表述恰當(dāng)且可證。如果推理器判定該子目標(biāo)在數(shù)學(xué)上不正確、不可證或表述不當(dāng)，我們將其標(biāo)記為需修正，并返回以?xún)?yōu)化原始證明草稿，從第 3.2.1 節(jié)開(kāi)始重復(fù)所有步驟，并將識(shí)別出的問(wèn)題作為反饋納入。除數(shù)學(xué)錯(cuò)誤外，推理器在此階段檢測(cè)到的一些常見(jiàn)失敗模式包括：子目標(biāo)定理陳述中缺少假設(shè)或條件，以及由 Lean 類(lèi)型系統(tǒng)引起的異常行為（例如自然數(shù)截?cái)啵?。

我們優(yōu)先采用證明器嘗試而非推理器驗(yàn)證，因?yàn)樽C明器模型計(jì)算成本更低，且一個(gè)有效的證明可自動(dòng)確認(rèn)數(shù)學(xué)正確性。經(jīng)驗(yàn)表明，大量生成的子目標(biāo)可被證明器成功證明。步驟 1 確保我們?cè)诔晒ψC明的子目標(biāo)上節(jié)省了昂貴的推理器模型用于驗(yàn)證的計(jì)算開(kāi)銷(xiāo)。

步驟 3（淺層求解）在步驟 1 失敗且步驟 2 確認(rèn)子目標(biāo)正確的前提下，我們采用推理器模型進(jìn)行“淺層求解”（shallow solve）：為證明器無(wú)法直接解決的子目標(biāo)編寫(xiě)簡(jiǎn)短證明。我們從 Mathlib 庫(kù)中檢索相關(guān)定理，并要求推理器為該子目標(biāo)編寫(xiě)形式化證明。推理器根據(jù)驗(yàn)證器反饋?zhàn)疃噙M(jìn)行 K proof correction = 6

輪迭代修正。當(dāng)編譯錯(cuò)誤表明缺少或引用了錯(cuò)誤的定理時(shí)，我們會(huì)檢索額外的相關(guān)定理。為節(jié)省計(jì)算資源，若某錯(cuò)誤證明超過(guò)長(zhǎng)度閾值 K max shallow solve length = 30 行，我們即終止此步驟——因?yàn)檫^(guò)長(zhǎng)的證明表明需要進(jìn)一步分解。整個(gè)淺層求解過(guò)程最多重復(fù) K informal passes = 6
次，直至獲得成功證明或耗盡所有嘗試次數(shù)。

步驟 4（遞歸分解與證明組裝）若經(jīng)過(guò)步驟 1–3 后仍有子目標(biāo)未被證明，我們遞歸地應(yīng)用子目標(biāo)分解流程（第 3.2.1 節(jié)）對(duì)其進(jìn)行進(jìn)一步拆分。每個(gè)子目標(biāo)被持續(xù)細(xì)分，直至被成功證明，或達(dá)到最大遞歸深度 D 。一旦所有子目標(biāo)均被證明，我們通過(guò)拼接所有子目標(biāo)的證明與第 3.2.1 節(jié)步驟 4 中生成的組裝證明大綱，構(gòu)建給定定理的完整證明。具體做法是將子目標(biāo)的證明與第 3.2.1 節(jié)步驟 4 產(chǎn)生的組裝證明進(jìn)行拼接。若此時(shí)仍有未解決的子目標(biāo)，則觸發(fā)證明失敗，促使我們重新啟動(dòng)該定理的子目標(biāo)分解流程。

完整算法見(jiàn)算法 1。關(guān)于實(shí)現(xiàn)細(xì)節(jié)，特別是并行化策略，請(qǐng)參見(jiàn)附錄 A.3。

4 實(shí)驗(yàn)結(jié)果

4.1 主要結(jié)果

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

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

與獨(dú)立的基礎(chǔ)證明器在 pass@4 指標(biāo)下的表現(xiàn)相比，我們的方法帶來(lái)了顯著提升，改進(jìn)幅度介于 20.1% 至 37.1% 之間。

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

HILBERT 在 PutnamBench 上取得了當(dāng)前最優(yōu)性能，成功解決了 660 道題中的 462 道（通過(guò)率為 70.0%）。這一結(jié)果比此前最佳方法——閉源的 SeedProver（50.4%）——高出近 20 個(gè)百分點(diǎn)。HILBERT 解決的問(wèn)題數(shù)量超過(guò)最接近的公開(kāi)基線模型 Goedel-Prover-V2-32B 達(dá)五倍以上。我們將這一成功歸因于 HILBERT 能夠組合長(zhǎng)篇證明（見(jiàn)圖 9），而不會(huì)受到傳統(tǒng) LLM 所面臨的長(zhǎng)上下文推理問(wèn)題的困擾（Zhou 等，2025a）。

4.2 推理時(shí)計(jì)算資源的擴(kuò)展行為

與傳統(tǒng)證明器 LLM 將計(jì)算資源分配到大量從零開(kāi)始的獨(dú)立證明嘗試不同，HILBERT 將推理時(shí)的計(jì)算資源分配到多個(gè)相互關(guān)聯(lián)的階段，從子目標(biāo)分解到子目標(biāo)證明生成。由于這種計(jì)算資源分配是自適應(yīng)的，無(wú)法通過(guò)簡(jiǎn)單的獨(dú)立嘗試次數(shù)來(lái)衡量。

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

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

關(guān)于通過(guò)率與證明器/驗(yàn)證器調(diào)用次數(shù)及總 token 使用量的更多分析，請(qǐng)參見(jiàn)附錄 A.6。

4.3 消融研究

性能（vs）遞歸深度。為評(píng)估子目標(biāo)分解的有效性，我們?cè)?MiniF2F 數(shù)據(jù)集上分析了使用 Gemini 2.5 Pro + Goedel-Prover-V2-32B 的 HILBERT 在不同遞歸深度 D D 下的通過(guò)率�；�（ D = 0
）對(duì)應(yīng)無(wú)分解情形，此時(shí)我們報(bào)告獨(dú)立證明器（pass@4）的性能。我們比較兩種配置：完整的 HILBERT 系統(tǒng)，以及一個(gè)禁用淺層求解（shallow solving）的變體（即設(shè) K informal passes = 0）。該變體僅依賴(lài)證明器來(lái)解決子目標(biāo)。

圖 4 展示了不同 D D 值下的性能表現(xiàn)，清楚表明子目標(biāo)分解帶來(lái)了顯著增益。兩種配置的性能均隨深度單調(diào)遞增，但呈現(xiàn)出不同的收斂模式。完整的 HILBERT 系統(tǒng)在較淺深度即獲得快速性能提升：在 D = 2
時(shí)達(dá)到 98.36%，到 D = 3 時(shí)已達(dá) 98.7%。相比之下，無(wú)淺層求解的變體需要更大的深度才能達(dá)到相近性能，凸顯了淺層求解機(jī)制的重要性。相較于 D = 0 基線（通過(guò)率 75%），性能持續(xù)提升，驗(yàn)證了分層子目標(biāo)分解的有效性；完整系統(tǒng)在相對(duì)較小的深度下即可實(shí)現(xiàn)接近最優(yōu)的性能。

檢索消融實(shí)驗(yàn)。為評(píng)估檢索器（Retriever）對(duì)性能和計(jì)算效率的影響，我們將 HILBERT 與一個(gè)省略檢索步驟的變體進(jìn)行比較。我們?cè)?MiniF2F 上針對(duì)兩種證明器配置進(jìn)行實(shí)驗(yàn)：DeepSeek-Prover-V2-7B 和 Goedel-Prover-V2-32B。結(jié)果見(jiàn)表 3。

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

這些結(jié)果表明，檢索通過(guò)提供有助于簡(jiǎn)化證明的有用定理，并避免因引用錯(cuò)誤定理名稱(chēng)而導(dǎo)致的失敗，同時(shí)提升了性能與效率。

5 結(jié)論

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

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

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