智能體的形式數學證明框架

Prover Agent：基于智能體的形式數學證明框架

PROVER AGENT: AN AGENT-BASED FRAMEWORK FOR FORMAL MATHEMATICAL PROOFS

https://arxiv.org/pdf/2506.19923

摘要：

我們提出了 Prover Agent——一種用于自動定理證明的新穎人工智能智能體，它將大語言模型（LLMs）與形式化證明助手 Lean 相結合。Prover Agent 協調一個非形式化推理 LLM、一個形式化證明模型以及來自 Lean 的反饋，同時還能生成輔助引理。這些輔助引理不僅限于形式化證明中的子目標，還可包括特殊情形或從假設中推導出的潛在有用事實，有助于發現可行的證明策略。它在 MiniF2F 基準上達到了 88.1% 的成功率，在使用小型語言模型（SLMs）的方法中創下新紀錄，且所需的樣本預算遠低于以往方法。我們還提供了理論分析和案例研究，闡明這些生成的引理如何助力解決具有挑戰性的問題。代碼已公開發布：https://github.com/kAIto47802/Prover-Agent。

1 引言

近年來，大語言模型（LLMs）在推理能力方面的進步推動了人工智能多個領域的顯著進展，包括數學定理證明與問題求解（OpenAI, 2024；DeepSeek-AI, 2025；Yang 等, 2025a；Lewkowycz 等, 2022）。然而，LLMs 容易產生錯誤和幻覺，從而削弱其可靠性（Ji 等, 2023；Huang 等, 2025；Xu 等, 2025）。推理時擴展技術（如思維鏈，chain-of-thought）通過讓模型反思并修正錯誤的推理步驟，大幅提升了其推理性能（Wei 等, 2022）。盡管如此，徹底消除錯誤仍然極具挑戰性，尤其對于更困難的問題（Wei 等, 2022；Zeng 等, 2025）。

形式化證明助手（如 Lean（Moura & Ullrich, 2021）、The Rocq Prover（原 Coq）（Barras 等, 1999）和 Isabelle（Paulson, 1994））基于 Curry–Howard 對應關系，通過計算機嚴格驗證用其語言書寫的數學證明中每一步推理的正確性。這幫助數學家確保證明的嚴謹性——在此過程中，不允許任何錯誤、細節遺漏、隱含假設或歧義。然而，使用形式化證明助手通常需要耗費大量人工精力并關注極致細節。因此，自動定理證明長期以來一直是人工智能與形式化方法領域的一項重大挑戰（Newell & Simon, 1956；Irving 等, 2016；Polu & Sutskever, 2020；Jiang 等, 2023；Lu 等, 2023）。

近年來，將 LLM 用于形式化定理證明變得日益重要，催生了大量相關研究（Wang 等, 2024b；Wu 等, 2024a；Xin 等, 2025b；Li 等, 2025；Xin 等, 2025a；Dong & Ma, 2025；Lin 等, 2025b；Zhang 等, 2025；Wang 等, 2025；Ren 等, 2025；Ji 等, 2025；Lin 等, 2025c；Cao 等, 2025；Zhou 等, 2025；Chen 等, 2025）。這不僅為保證 LLM 數學推理的正確性提供了途徑，也標志著自動定理證明的重大突破。關鍵在于 LLM 與形式化證明助手的互補優勢：LLM 擅長推理與生成，但可能出錯且缺乏正確性保證；而 Lean 等形式化證明助手則具備基于數理邏輯的完美驗證能力，卻不具備生成性。

然而，在非形式化推理與形式化證明之間仍存在顯著鴻溝（Yang 等, 2025b）。例如，即使 o3-mini（OpenAI, 2025）在自然語言數學競賽題上表現優異，若直接提示其為一道競賽級問題生成完整 Lean 證明，單次嘗試的成功率僅為 6.0%（Yousefzadeh & Cao, 2025）。即便在數學數據上微調、使用強化學習或引入思維鏈，純神經方法仍難以生成正確的形式化證明，其形式化證明能力遠落后于其自然語言中的非形式化推理能力。

為彌合這一差距，我們提出一種新穎的智能體框架（Prover Agent），協調非形式化推理 LLM、形式化證明模型與 Lean 驗證系統。針對無法直接求解的難題，該智能體生成輔助引理以協助發現可行的證明策略。這些引理不僅限于可直接插入形式化證明的子目標，還可包括特殊情形或從假設中推導出的潛在有用事實。當整體證明策略初始不明確時，這類引理尤其有效，有助于構建可行的證明計劃。在 MiniF2F 基準（Zheng 等, 2022）上，該方法達到 88.1% 的成功率，在使用小型語言模型（SLMs）的方法中創下新紀錄。值得注意的是，它僅使用 SLMs，且樣本預算遠低于以往高性能方法，推理成本顯著更低。此外，我們還提供了理論分析與案例研究，展示智能體生成輔助引理的有效性。

我們的貢獻總結如下：

• 結合非形式化與形式化推理，并利用 Lean 反饋：我們的智能體在 Lean 驗證下協同非形式化 LLM 與形式化證明器。LLM 生成自然語言推理與引理，證明器將其形式化，Lean 進行驗證。Lean 檢測到的錯誤立即反饋，支持對構造的證明進行迭代優化。
• 通過輔助引理生成實現策略發現：對于難以直接求解的問題，智能體生成輔助引理（如特殊情形、潛在有用事實或假設驅動的猜想），并對其進行形式化證明。通過結合已驗證引理重新審視整體證明，系統即使在初始路徑不明的情況下也能發現可行策略。
• 當前最優的定理證明性能：在 MiniF2F 基準（Zheng 等, 2022）——一個包含 488 道來自數學奧林匹克與高等數學的標準形式化定理證明基準——上，我們的智能體達到 88.1% 的通過率，在使用 SLMs 的方法中樹立了新標桿。
• 推理成本高效：88.1% 的成功率僅使用 SLMs 實現，且樣本預算遠低于以往高性能方法，凸顯了本方法在推理成本上的高效性。

2 相關工作

本節簡要概述自動形式化定理證明的近期進展，代表性系統的詳細信息見附錄 A。

基于樹搜索的形式化證明：樹搜索方法逐策略（tactic-by-tactic）構建 Lean 證明，通過顯式搜索（如最佳優先搜索或蒙特卡洛樹搜索 MCTS）導航證明空間（Lample 等, 2022；Wang 等, 2023；Wu 等, 2024a；Zhou 等, 2024；Li 等, 2025；Xin 等, 2025a,b）。該方向始于由目標狀態引導的逐步策略預測，現已發展為優化策略模型、搜索啟發函數和數據篩選以處理更長證明的成熟系統。

整體證明生成：與樹搜索互補的是整體證明生成（First 等, 2023），即模型一次性輸出完整 Lean 腳本，常伴隨長思維鏈推理軌跡。該方法通過專家迭代流程（將已驗證證明回流至訓練）（Polu 等, 2023；Wu 等, 2021, 2024a；Lin 等, 2025a,b,c；Dong & Ma, 2025）以及利用形式化驗證器反饋的強化學習（Kaliszyk 等, 2018；Xin 等, 2025a；Zhang 等, 2025；Wang 等, 2025；Ren 等, 2025；Gloeckle 等, 2024；Ji 等, 2025；Lin 等, 2025c）不斷進步。

結合檢索增強生成（RAG）的形式化定理證明：另一新興方向是將基于 LLM 的證明器與檢索增強生成結合，在推理時查詢外部知識源或證明庫以補充模型推理（Yang 等, 2023；Shen 等, 2025）。

證明精煉與子目標分解：部分工作探索了證明精煉——根據證明助手的反饋改進初始證明嘗試（Thakur 等, 2024；Zhou 等, 2025；Chen 等, 2025；Lin 等, 2025c）。另一方向涉及子目標分解——將復雜定理拆解為更易證明的簡單子目標（Dong 等, 2025；Wang 等, 2024a；Ren 等, 2025；Zhou 等, 2025），常由自然語言草圖引導（Jiang 等, 2023；Cao 等, 2025）。

子目標分解方法與我們的工作有一定相似之處，但我們的方法采用了更全面的策略，將其納入更廣框架。在前述工作中，必須預先正確構想完整的證明草圖，而這往往很難做到。相比之下，我們的方法并不要求從一開始就完全看清整體證明策略。我們不僅限于與預定義證明計劃直接對齊的子目標分解，還考慮特殊情形或潛在有用事實等輔助引理，以自底向上的方式逐步構建證明策略。

3 方法

整體工作流程如圖 2 所示，對應的偽代碼見算法 1。給定一個形式化數學問題，我們的智能體首先嘗試直接證明——這對較簡單的問題通常已足夠。對于無法直接求解的更難問題，它會生成輔助引理以揭示可行的證明策略。這些引理隨后被分別形式化并逐一證明，最終利用已證引理合成原問題的完整證明。在整個過程中，Lean 的反饋被用于對構造的證明進行迭代優化。下文將分階段描述該過程，重點說明非形式化 LLM、形式化證明模型與 Lean 如何協同構建形式化證明。

3.1 基于非形式化推理與迭代反饋的形式化證明構建

智能體首先嘗試在不進行分解的情況下直接證明給定問題或所生成的引理。為利用非形式化 LLM 相較于形式化證明模型更強的數學推理能力，我們首先使用非形式化 LLM 為該問題或引理生成一段自然語言的非形式化證明。隨后，形式化證明模型以此非形式化證明作為上下文引導，生成形式化證明，并交由 Lean 驗證。若驗證成功，則此步驟完成；若失敗，則重復上述過程，直至找到成功證明或達到最大嘗試次數 N init
。該過程有助于為后續的迭代精煉階段建立更優的初始證明草稿。

若證明仍失敗，智能體進入迭代精煉階段。從此前所有嘗試中選取 Lean 驗證錯誤最少的證明作為初始草稿。隨后，基于 Lean 的反饋對該草稿進行迭代修正：在每次迭代中，將上一次的證明嘗試、錯誤位置及對應的錯誤信息一并提供給證明模型，由其修改并生成修正后的證明版本。該過程持續進行，直到證明被 Lean 成功驗證，或達到最大精煉嘗試次數 N refine
。

這一迭代精煉過程利用 Lean 的驗證能力識別并修正錯誤，本質上是一種通過上下文學習實現的自糾錯機制，類似于人類如何從反饋中改進理解。這有效彌補了推理時擴展（如思維鏈）的一個關鍵局限：單純增加推理步數并不能保證更好結果，因為模型的自糾錯能力有限（Zeng 等, 2025；Song 等, 2025；Stechly 等, 2025；Huang 等, 2024）。

此外，若某個生成的引理無法被證明，系統可放棄該引理——這模擬了人類數學家的典型做法：當整體策略尚不清晰時，常會探索多個方向，其中一些最終被證明無效而被舍棄，轉而聚焦更有希望的路徑。或者，若引理本身仍過于困難，系統還可遞歸地引入更小的輔助引理，最多遞歸至深度上限 D 。

3.2 通過非形式化推理生成引理

當直接證明方法失敗時，智能體會生成若干輔助引理。這些引理不僅限于可直接插入最終證明的子目標，還可包括特殊情形或從假設中推導出的潛在有用事實，以幫助構建證明策略。這是與先前工作的關鍵區別：以往方法通常依賴于根據預定義的證明草圖將問題分解為子目標（Jiang 等, 2023；Wang 等, 2024a；Ren 等, 2025；Cao 等, 2025；Zhou 等, 2025）。這類方法要求事先構想出正確的整體證明策略，而這往往極具挑戰性。事實上，這些方法通常依賴 DeepSeek-V3（DeepSeek-AI, 2024）和 DeepSeek-R1（DeepSeek-AI, 2025）等更大、更強的模型，以期從一開始就準確預測整個證明計劃。

相比之下，我們的方法不要求從一開始就看清整體證明策略。通過生成輔助引理，智能體能夠以自底向上的方式逐步構建有效的證明策略，即使初始時完整結構并不明確。

這種方法模仿了人類數學家通常的工作方式：當整體策略在初始階段不清晰時，他們往往會探索特例或思考從假設中能推導出什么內容。通過這種試錯過程，他們逐步發現整體證明策略。

系統首先以自然語言生成引理，以利用非形式化大語言模型更強的數學推理能力。隨后，這些引理由一個形式化模型轉換為形式化語句——該模型僅形式化其前提和結論，而不嘗試構造證明。Lean 也在此用于驗證這些形式化語句的語法正確性，直至它們被重新生成為有效語句為止。這些經形式化后的引理隨后使用第 3.1 節所述的證明構建流程進行證明。

3.3 基于已驗證引理與迭代反饋的最終證明合成

4 理論分析

我們提出理論分析，以論證第 3 節所述方法的有效性。
引理的使用具有兩個關鍵作用：(i) 在給定策略下對證明步驟進行分解，使其更易處理；(ii) 在初始階段尚不明確合適證明策略時，輔助發現該策略（例如通過檢驗特殊情形）。以往工作主要聚焦于 (i)，通常依賴更大的模型來直接構思整體策略（Wang 等, 2024a；Jiang 等, 2023；Ren 等, 2025；Cao 等, 2025；Zhou 等, 2025），而我們的方法同時利用 (i) 和 (ii)，從而更有效地解決困難問題。第 4.1 節和第 4.2 節分別簡要呈現了針對情形 (i) 和 (ii) 中引理使用的理論分析結果。詳見附錄 C。

4.1 引理在結構化證明分解中的優勢

證明詳見附錄 C.1。定理 4.4 表明，基于引理的分解能在所需嘗試次數的數量級上帶來指數級提升；而定理 4.5 指出，對于較小的 p p （即困難問題），使用引理可減少所需的嘗試次數。這為我們的方法提供了理論支持：對難題生成引理，而對簡單題直接求解。此外，定理 4.6 表明，最優引理是那些能將原問題劃分為難度大致相等子問題的引理。

4.2 引理在發現證明策略（例如特殊情形）中的優勢

此外，該結果還意味著：不僅引理，任何與最終正確證明共享互信息的上下文信息，同樣可以提升成功概率，從而為我們使用自然語言證明和 Lean 反饋的做法提供了理論依據。

5 實驗

5.1 實驗設置

存在若干可能導致無效 Lean 證明被錯誤接受的漏洞，例如與 apply? 策略相關的用戶界面缺陷（Ren 等，2025），以及 REPL2 中的一個 bug。為避免這些問題、防止無效證明被誤判為正確，我們改用 lake build 而非 REPL 來驗證證明，并額外確認未使用 apply? 策略。此外，為規避該漏洞并獲得可靠的基線結果，我們重新運行了針對 Goedel-Prover-V2-8B 的實驗。

我們使用 GitHub3 和 Hugging Face? 上提供的官方提示詞，同時保持其他所有實驗設置與我們方法中的完全一致，從而確保公平比較。對于 DeepSeek-Prover-V2，我們依賴 Ren 等人（2025）報告的結果——其中該漏洞已被修復。更多細節請參見附錄 D。

5.2 主要結果：與先前最先進方法的比較

結果如表 1 和圖 1 所示。我們的智能體達到了 88.1% 的成功率，在使用小型語言模型（SLMs）的方法中創下新的當前最優紀錄。值得注意的是，我們的智能體僅使用 260 的樣本預算就取得了這一結果，遠低于以往工作，凸顯了其在推理成本方面的高效性。

5.3 模塊化與可擴展設計

為驗證我們方法的魯棒性，我們在多個模型上進行了實驗，包括 DeepSeek-Prover-V2 和 Goedel-Prover-V2。如表 1 所示，在兩種設置下，我們的方法均以更小的樣本預算取得了比原始模型更高的成功率。此外，我們的方法還能對這些模型進行集成：在樣本預算平均分配給兩個模型的實驗中，智能體取得了更高的成功率，表明模型之間能互補解決單個模型無法攻克的問題。
與端到端訓練單一大型模型的單體方法不同，我們的方法采用正交策略——無需任何訓練，直接組合現有的 LLM 與證明器模型。這種模塊化設計具有實際優勢：系統可通過簡單替換組件，立即受益于 LLM 和證明器模型的最新進展，并能輕松隨未來技術進步而擴展。

5.4 非形式化、形式化與 Lean 協同的有效性

表 1 顯示，在兩種模型設置下，即使在迭代精煉之前，我們的方法已優于對應的原始基線，凸顯了與非形式化 LLM 協作帶來的收益。此外，在引入迭代精煉后，性能進一步提升。

5.5 消融研究：分析各階段的貢獻

5.6 案例研究：引理引導證明的成功實例

接下來，我們通過一個案例研究來展示引入輔助引理的方法在實踐中確實有效。該問題的詳細討論及相關輸出（包括生成的引理、最終形式化證明及對應的推理過程）見附錄 E。我們分析了一個直接證明嘗試失敗、但借助輔助引理最終成功證明的問題。

在此案例中，我們的智能體生成了一個對應于將 n = 3 代入原問題的特殊情形引理，同時還生成了其他可能與求解相關的輔助引理。如在使用該引理時的思維鏈過程所見（參見附錄 E.5），智能體立即關注 n = 3 的情形，并迅速提出數學歸納法作為證明策略。這使其能夠快速轉入在清晰證明計劃下的細節填充階段，并最終完成證明。此外，在輔助引理中考慮的策略與證明技巧也重新出現在后續推理過程和最終證明中：即使某個引理本身未被直接使用，其生成過程中探索的技巧仍為整體證明構建提供了寶貴線索。

作為對比，我們進一步考察了不使用引理時的推理過程，聚焦于最終錯誤最少的軌跡（見附錄 E.6）。與成功使用引理的情形相比，此處的證明策略遠不夠清晰，模型在缺乏連貫計劃的情況下徘徊不定。結果，即便它最終想到了使用數學歸納法，也無法展開具體細節，導致證明失敗。這一對比凸顯了我們輔助引理方法的有效性——它超越了以往工作中簡單的子目標分解，真正助力發現并執行可行的證明策略。

5.7 在奧林匹克級別問題上的表現

表 2 展示了 MiniF2F 測試集上各子類別的結果。這些結果表明，在 DeepSeek-Prover-V2 設置下，我們的方法在奧林匹克級別問題上表現尤為出色，甚至超越了 Ren 等人（2025）提出的 DeepSeek-Prover-V2——后者使用了規模大得多的 671B 模型，并且樣本預算高達 8192。值得注意的是，即使我們僅使用無迭代精煉的直接證明方法，且樣本預算僅為 100，其性能已超過 DeepSeek-Prover-V2。這表明，與基于自然語言的非形式化推理協同工作可能是關鍵所在。

奧林匹克級別問題對數學推理能力要求極高，而非形式化 LLM 強大的推理能力很可能在此發揮了決定性作用。另一方面，在 MATH 和 Custom 類別中，我們的智能體并未超越 DeepSeek-Prover-V2。這些類別中持續存在的性能差距表明，模型規模和樣本預算在此可能更為重要。由于 DeepSeek-Prover-V2 本身已具備一定的數學推理能力，因此能獨立處理這些相對數學難度較低的問題。相比之下，在 Goedel-Prover-V2 設置下，各類別之間未觀察到顯著差異。這很可能是因為 Goedel-Prover-V2 已經具備處理所有這些類別所需的基本數學能力，因此類別間的差異并不明顯。

5.8 更廣泛的適用性與未來潛力

我們的流程中沒有任何部分是專為數學競賽問題設計的。只要 LLM 具備相關領域知識或被提供適當的知識庫，該方法同樣可應用于其他領域的形式化證明，例如學習理論或物理學。這為實現無幻覺、無邏輯錯誤的人工智能驅動的數學理論構建提供了潛在路徑。

6 結論

我們提出了 Prover Agent——一種模塊化框架，協調非形式化推理大語言模型（LLM）、形式化證明模型與 Lean 驗證系統。通過生成輔助引理并結合反饋驅動的精煉機制，我們的方法在 MiniF2F 基準上取得了使用小型語言模型（SLMs）方法中的當前最優性能。未來工作包括開發針對不同類型問題生成更有效引理的機制，并將本框架拓展至數學以外、但同樣需要形式化驗證的領域，例如軟件驗證。

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