智能體的形式數(shù)學(xué)證明框架

Prover Agent：基于智能體的形式數(shù)學(xué)證明框架

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

https://arxiv.org/pdf/2506.19923

摘要：

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

1 引言

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

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

近年來，將 LLM 用于形式化定理證明變得日益重要，催生了大量相關(guān)研究（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 數(shù)學(xué)推理的正確性提供了途徑，也標(biāo)志著自動定理證明的重大突破。關(guān)鍵在于 LLM 與形式化證明助手的互補優(yōu)勢：LLM 擅長推理與生成，但可能出錯且缺乏正確性保證；而 Lean 等形式化證明助手則具備基于數(shù)理邏輯的完美驗證能力，卻不具備生成性。

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

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

我們的貢獻(xiàn)總結(jié)如下：

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

2 相關(guān)工作

本節(jié)簡要概述自動形式化定理證明的近期進(jìn)展，代表性系統(tǒng)的詳細(xì)信息見附錄 A。

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

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

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

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

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

3 方法

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

3.1 基于非形式化推理與迭代反饋的形式化證明構(gòu)建

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

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

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

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

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

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

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

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

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

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

4 理論分析

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

4.1 引理在結(jié)構(gòu)化證明分解中的優(yōu)勢

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

4.2 引理在發(fā)現(xiàn)證明策略（例如特殊情形）中的優(yōu)勢

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

5 實驗

5.1 實驗設(shè)置

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

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

5.2 主要結(jié)果：與先前最先進(jìn)方法的比較

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

5.3 模塊化與可擴展設(shè)計

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

5.4 非形式化、形式化與 Lean 協(xié)同的有效性

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

5.5 消融研究：分析各階段的貢獻(xiàn)

5.6 案例研究：引理引導(dǎo)證明的成功實例

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

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

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

5.7 在奧林匹克級別問題上的表現(xiàn)

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

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

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

我們的流程中沒有任何部分是專為數(shù)學(xué)競賽問題設(shè)計的。只要 LLM 具備相關(guān)領(lǐng)域知識或被提供適當(dāng)?shù)闹R庫，該方法同樣可應(yīng)用于其他領(lǐng)域的形式化證明，例如學(xué)習(xí)理論或物理學(xué)。這為實現(xiàn)無幻覺、無邏輯錯誤的人工智能驅(qū)動的數(shù)學(xué)理論構(gòu)建提供了潛在路徑。

6 結(jié)論

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

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