擴展多輪離策略強化學習與多智能體樹搜索用于大語言模型逐步證明器

擴展多輪離策略強化學習與多智能體樹搜索用于大語言模型逐步證明器

Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers

https://arxiv.org/pdf/2509.06493

摘要：

大語言模型（LLMs）與自動定理證明的結合展現出巨大潛力，但仍受限于訓練階段強化學習（RL）和推理階段計算資源的擴展難題。本文提出 BFS-Prover-V2——一個開源的、面向步驟級定理證明的系統，旨在同時解決上述雙重擴展挑戰。我們提出了兩項核心創新：

第一，一種新穎的多輪離策略強化學習（multi-turn off-policy RL）框架，用于在訓練階段持續提升 LLM 逐步證明器的性能。該框架受 AlphaZero 原理啟發，采用多階段專家迭代流程，包含自適應的策略級數據過濾機制和周期性重訓練，以突破 LLM 智能體在長期強化學習中常見的性能平臺期。

第二，一種規劃器增強的多智能體系統，在推理階段擴展推理能力。該架構使用一個通用推理模型作為高層規劃器，將復雜定理迭代地分解為一系列更簡單的子目標。這種分層方法顯著縮小了搜索空間，使得一組并行的證明智能體能夠通過共享證明緩存高效協作。

我們證明，這種訓練與推理雙重擴展的方法在已有的形式化數學基準上取得了當前最優的結果：BFS-Prover-V2 在 miniF2F 和 ProofNet 測試集上分別達到 95.08% 和 41.4% 的求解率。盡管本工作在形式化數學領域進行驗證，但所提出的強化學習與推理技術具有更廣泛的適用性，可推廣至其他需要長視野、多輪推理與復雜搜索的任務領域。我們的模型與代碼已在 https://github.com/ByteDance-Seed/BFS-Prover-V2 開源。

1 引言
自動定理證明（Automated Theorem Proving, ATP）是數理邏輯與自動推理的一個子領域，代表了計算機科學的一項基礎性追求［3］。在當代形式化數學的格局中，交互式定理證明器（Interactive Theorem Provers, ITPs）或稱證明助手正日益占據主導地位。這類系統（如 Coq、Isabelle 和 Lean）需要人類用戶引導證明過程，但它們能自動完成大量演繹任務，并且最重要的是，能夠提供機器可驗證的正確性保證［8］。其中，Lean4 編程語言［19］已發展成為一個尤為活躍的生態系統。其成功的關鍵因素之一是 Mathlib［4］——一個龐大而全面、由社區驅動的形式化數學庫。

涵蓋超過一百萬行代碼，Mathlib 覆蓋了代數、分析、拓撲等多個廣泛的數學領域，為前沿數學研究和經過驗證的系統開發提供了豐富的基礎。Lean4 的興起恰逢大語言模型（LLMs）能力的爆炸式增長［7, 20, 24］，由此開辟了神經符號人工智能系統的新前沿。這一方向的目標是將 LLM 直觀而強大的生成與搜索能力，與形式化系統的絕對邏輯驗證能力相結合。該研究路徑的核心是一個關鍵的反饋循環：LLM 提出直觀的證明步驟，Lean 編譯器提供嚴格的驗證，而強化學習（RL）［28］則利用該驗證信號持續提升 LLM 的推理能力［10, 12, 21, 34, 38］。

1.1 LLM 證明器與推理智能體中的雙重擴展挑戰

高性能 LLM 證明器（或任何其他推理智能體）的發展，取決于對兩個根本性且緊密關聯的擴展挑戰的解決。

訓練階段的擴展（Training-time scaling）：指通過訓練持續增強模型基礎能力與策略直覺所需的技術。在 LLM 上應用 RL 時，一個常見且重大的障礙是“性能平臺期”現象：在初始快速提升階段之后，模型往往陷入停滯，即使繼續訓練，其能力也不再增長［9, 18, 24, 29, 34, 35, 41, 42］。要克服這一限制，需要精心設計的算法，使其能在長時間內維持學習能力，推動模型從掌握簡單問題逐步過渡到攻克日益復雜的定理。

推理階段的擴展（Inference-time scaling）：指如何利用已訓練好的模型求解先前未見過的定理。現實中的數學問題通常需要深度、多步推理，中間引理的構造，以及在指數級龐大的策略空間中進行探索。一個強大的基礎模型雖是必要條件，但并不充分。若缺乏有效的搜索策略，即便是能力較強的模型也會被組合爆炸式的搜索復雜度所壓垮。因此，挑戰在于設計一種推理架構，能夠高效地將復雜問題分解為更簡單的子問題，并戰略性地將計算資源分配給最有希望的探索路徑［2, 5, 6, 11, 43］。

1.2 本文貢獻

本文提出BFS-Prover-V2——一個面向 Lean4 神經定理證明的完整訓練與推理系統，針對上述雙重擴展挑戰提出了創新性解決方案。本工作的主要貢獻如下：

• 訓練階段的新型 RL 擴展技術：我們開發了一種無需蒸餾（distillation-free）的多階段專家迭代框架［1, 26］，這是一種專為形式化定理證明領域定制的離策略強化學習（off-policy RL）方法。為維持長期學習并突破性能平臺期，我們在 RL 流程中引入了一套專門技術：包括一種基于困惑度（perplexity-based）、自適應的策略級數據過濾策略，可為智能體自動生成課程（curriculum）；以及一種周期性重訓練機制，作為模型參數空間中的“軟重啟”（soft reset），幫助逃離局部最優，提升模型的擴展潛力。
• 推理階段的規劃器增強型多智能體樹搜索系統：為實現推理階段的擴展，我們引入了一種分層推理架構。一個通用推理模型（稱為“規劃器”，Planner）迭代地將復雜定理/目標分解為一系列更易處理的子目標。這些子目標隨后由一組并行的證明智能體協同處理，它們共享一個公共的子目標緩存（subgoal cache），從而大幅降低系統整體的搜索復雜度，使其能夠解決單體證明器無法處理的問題。
• 當前最優的實證結果：我們在標準基準上驗證了該雙重擴展方法的有效性與泛化能力。BFS-Prover-V2 在 miniF2F 測試集上達到95.08%的求解率，大幅超越此前的逐步證明器［32, 36］，并與當前最優的整體證明模型［17, 23, 30］性能相當。在 ProofNet 測試集上，它取得了41.4%的成績，創下新的當前最優紀錄，展現出跨分布的強健泛化能力。

2 BFS-Prover-V2 系統
本節詳細描述 BFS-Prover-V2 的兩個核心組成部分：(i) 一個基于馬爾可夫決策過程（MDP）［22］的訓練流程，通過自適應過濾和周期性重訓練實現擴展；(ii) 一個推理引擎，采用規劃器增強的多智能體搜索機制進行分層推理。這兩個組件在 BFS-Prover-V1［36］的基礎上進一步發展，專門針對訓練與推理階段的雙重擴展挑戰。圖 1 和圖 4 提供了這些組件的可視化概覽，具體的實現參數詳見第 3.2 節。

2.1 步驟級建模：將定理證明形式化為馬爾可夫決策過程

我們將 Lean4 策略模式（tactic mode）下的證明搜索建模為智能體與環境之間的多輪交互過程，并將其形式化為一個馬爾可夫決策過程（MDP）。在此框架中，LLM 證明器作為智能體，而 Lean 編譯器及其當前策略狀態則構成環境。該建模方式準確捕捉了形式化證明逐步構建時所具有的序列性和狀態依賴特性［19, 39］。我們 MDP 的各組成部分定義如下：

這種步驟級、交互式的建模方式與整體證明生成模型［17, 23, 30］形成鮮明對比——后者將定理證明視為從定理陳述到完整證明腳本的一次性代碼生成任務。盡管整體方法更簡單，但現有整體證明模型無法對證明過程中的中間狀態作出響應，也難以融入人類數學家的交互式工作流［27, 31］。相比之下，我們基于 MDP 的方法從設計上就訓練出一個真正的 Lean 協作助手（copilot），能夠在證明過程的任意時刻建議下一步合乎邏輯的策略［39］。

2.2 基于最佳優先樹搜索的專家迭代

BFS-Prover-V2 的核心訓練循環是一個專家迭代（expert iteration）流程，可視為 AlphaZero 算法的一種變體［1, 26］。該方法使系統能夠從自身經驗中學習并不斷提升其定理證明能力［25］。如圖 1 內環所示，該流程包含兩個交替進行的主要階段：證明生成（Proof Generation）與模型精煉（Model Refinement）。

階段 1：證明生成在此階段，當前最優版本的 LLM 證明器（稱為“專家”）被指派求解一個大規模的數學問題語料庫。本文工作中，我們自動形式化了約 300 萬個問題［4, 13, 16, 33, 36, 40］，作為訓練基礎。該專家模型與 BFS-Prover-V1［36］中使用的最佳優先樹搜索（Best-First Search, BFS）算法相結合，以探索龐大的可能證明路徑空間。神經策略與系統性搜索的結合，使系統能夠解決單靠模型本身無法處理的問題。此階段發現的每個成功證明都構成一條由（狀態，策略）對組成的軌跡。在每一輪專家迭代中，系統執行約次樹搜索，生成海量的合成數據集。

階段 2：模型精煉第一階段生成的經驗數據隨后用于改進 LLM 證明器。具體而言，成功證明軌跡中的狀態-策略對被用于更新模型參數。更新后的模型隨即成為下一輪迭代中的新“專家”。

2.3.1 自適應策略過濾：從“恰到好處”的數據中學習

我們沒有采用粗粒度的、基于問題級別的過濾方法［29, 41］（這類方法通常依賴靜態的難度指標），而是提出了一種在策略級別（tactic level）上更動態、更細粒度的過濾策略。該策略基于一個經驗性觀察：LLM 生成的策略的困惑度（perplexity，即負對數概率）大致呈高斯分布。如圖 2 所示，該分布可分為三個截然不同的區域，每個區域對學習具有不同的意義：

• 低困惑度尾部（The Low-Perplexity Tail）：這一區域對應模型置信度極高的策略。這些通常是簡單、“顯而易見”的步驟，例如基本化簡或直接應用某個明確的前提。將這類樣本納入訓練批次無法提供新的學習信號，只會強化模型已經掌握良好的知識，可能導致過擬合，并削弱其探索能力。
• 高困惑度尾部（The High-Perplexity Tail）：這一區域代表模型感到高度意外的策略。我們的案例研究表明，這些策略通常并非源于巧妙或非平凡的推理，而往往是噪聲較大或次優的選擇。例如，在一個簡單問題上使用一個功能強大但參數繁多的通用策略，而實際上一個更直接的策略就已足夠。這類“花哨”的操作可能對訓練有害，因為它們可能誘導模型生成過度復雜或無關的策略，引發幻覺（hallucinations），并損害其核心推理能力。
• 中心分布區域（The Central Distribution）：這是“恰到好處”（Goldilocks）的學習區域。該區域中的策略既不太簡單，也不過于嘈雜，代表了對模型而言具有挑戰性但仍在其能力范圍內的步驟——即其“最近發展區”（zone of proximal development）。通過僅選擇該中心區域的數據進行訓練，我們確保模型始終在其能力邊界上持續學習，從而實現穩定而高效的提升。

2.3.2 周期性重訓練：“軟重啟”以逃離局部最優

即使采用自適應過濾策略，在經過若干輪專家迭代更新后，模型性能仍可能開始進入平臺期。這是因為模型的“證明風格”逐漸固化：它對某些類型的策略和證明方法形成了強烈偏好，從而在龐大的推理策略空間中陷入局部最優。此時，模型雖能非常高效地以特定方式解決某些問題，卻喪失了發現新方法的能力——而這些新方法對于解決更新、更難的問題類別至關重要。

為逃離局部最優并重新激活學習過程，我們引入了一種周期性的“軟重啟”（soft reset）機制。這是一種多階段專家迭代流程，旨在提升模型的熵（即多樣性）并重置其探索潛力，同時不丟失已獲得的核心能力。該流程具體如下：

1. 重新合成與去噪（Re-synthesis and De-noise）

   
   使用當前性能最佳的證明器，重新求解其在所有過往迭代中遇到的全部問題語料庫。由于該證明器如今遠比早期輪次強大，它常常能找到更短、更直接、更優雅的證明。這一步實質上是讓專家模型對其自身過去的工作進行去噪和優化，濾除初始證明中因信息不足而產生的冗余或迂回步驟。

2. 激進的數據精選（Aggressive Data Curation）

   
   將上一步生成的新高質量證明，再次應用前述的策略級困惑度過濾策略，但采用更嚴格的標準。大量數據被舍棄，僅保留最關鍵、最具信息量的策略步驟。

3. 從基礎檢查點重新訓練（Retrain from a Base Checkpoint）

   
   用這一全新、高度精選且緊湊的數據集完全替換原有訓練數據。隨后，從一個通用的預訓練檢查點初始化一個全新的模型實例，并在此精煉數據集上從頭開始訓練。

如圖 3 所示，所得新模型在基準測試上的性能初期會出現暫時性下降。這是預期之中的現象：因為它是在一個更小、更聚焦的數據集上訓練的，并且“遺忘”了此前的一些風格化偏好。然而，該新模型具備顯著更強的探索潛力。當它被重新投入專家迭代循環后，其增強的探索能力使其能夠發現此前過度專業化模型無法觸及的新型證明策略。因此，其性能迅速恢復并超越之前的峰值，建立起更高的性能上限。圖 3 中標記的“retrain”事件所代表的周期性重訓練，是確保在數十輪訓練中實現長期、單調性能提升的關鍵機制。

2.4 推理擴展：規劃器增強的多智能體搜索

盡管強化學習流程提升了 LLM 的內在能力，但要真正解決高難度數學定理，仍需在推理階段采用復雜的策略來管理龐大的搜索空間。許多復雜數學證明并非通過一連串簡單演繹線性獲得，而是通過分層過程——識別并證明關鍵的中間結果（即引理）來完成的。

2.4.1 面向分層推理的規劃器-證明器范式

我們提出一種分層推理架構（如圖 4 所示），將定理證明任務分配給兩個不同的 LLM 智能體：高層規劃器（Planner）與低層證明器（Prover）。

• 規劃器（Planner）

  
  這是一個通用推理 LLM，負責戰略分解。給定當前定理陳述及證明進展，它的任務不是生成具體策略，而是提出一個包含若干中間子目標（subgoals）的高層計劃。這些子目標即為引理——若能證明它們，將簡化主定理的證明。通過構建這些子目標，規劃器有效地將一個單一、整體且可能不可解的搜索問題，轉化為一系列結構清晰、更易處理的小問題，從而大幅降低證明器所需探索的搜索空間維度。

• 證明器（Prover）

  
  這是通過第 2.3 節所述多階段專家迭代流程訓練出的專用 LLM 策略生成器。它一次接收一個來自規劃器的子目標，并結合其習得的策略與最佳優先搜索（BFS）［36］，為該特定子目標尋找形式化證明。

這種分工模擬了人類數學家的認知工作流：先通過識別關鍵引理勾勒出證明的高層結構（規劃器角色），再逐步填充每個引理的詳細、逐步演繹（證明器角色）。這種分層結構是應對復雜推理任務的強大架構模式。

2.4.2 規劃引導搜索的運行機制

如圖 4 所示，規劃器與證明器系統在動態循環中交互，使計劃可根據證明進展進行調整：

1. 初始規劃（Initial Planning）

   
   在證明嘗試開始時，向規劃器輸入主定理陳述，它返回一個以 Leanhave語句格式表示的子目標列表。

2. 子目標的順序證明（Sequential Proof of Subgoals）

   
   證明器系統依次處理這些子目標。它從隊列中取出第一個子目標，并啟動樹搜索以尋找其證明。

3. 上下文增強（Context Augmentation）

   
   一旦某個子目標被成功證明，其陳述即被“植入”到主定理的上下文中。此后，該已證子目標被視為一個已知事實（等同于前提），可用于后續所有子目標及主定理本身的證明。

4. 動態重規劃（Dynamic Replanning）

   
   若證明器在給定計算預算內未能找到某子目標的證明（即“卡住”），系統不會終止。相反，會重新查詢規劃器。此時，規劃器的輸入不僅包含原始定理陳述，還包含所有在卡住前已成功證明的子目標。基于這一新上下文，規劃器生成一個修訂后的計劃，通常會將“卡住”的子目標進一步分解為更細粒度的中間步驟，從而優化原證明策略。

這種規劃與證明之間的動態、迭代循環，使 BFS-Prover-V2 系統具備抗“卡死”能力，有效擴展了其推理階段的能力，使其能夠攻克單體樹搜索無法處理的復雜定理。

2.4.3 通過聚焦并行與共享子目標緩存實現多智能體協作

為加速證明搜索過程并減少實際運行時間（wall-clock time），規劃器-證明器架構被部署在一個多智能體框架中。我們并非依賴單一的證明器智能體，而是部署多個并行的證明器實例，共同協作執行由規劃器生成的計劃。這種協作由兩個核心原則協調：聚焦并行策略（focused parallelism）和共享子目標緩存（shared subgoal cache）。

聚焦并行（Focused Parallelism）：我們的系統并非將不同子目標分配給不同的證明器智能體，而是將所有證明器實例的全部計算資源集中用于一次僅一個子目標。該策略旨在克服單個智能體可能無法解決的推理瓶頸。此外，這種順序處理方式確保了計算效率：它避免了智能體在后續子目標上浪費資源——因為如果早期步驟失敗并觸發重規劃，這些后續子目標可能變得無效。

共享子目標緩存（Shared Subgoal Cache）：該緩存是所有并行證明器實例共享的核心通信與狀態跟蹤機制，承擔以下關鍵功能：

• 存儲規劃器生成的完整子目標序列；
• 實時追蹤每個子目標的狀態（例如：待處理、正在證明、已證明）；
• 記錄任何已求解子目標的證明。

這一架構為計劃中的每個引理（子目標）組織了一場“協作式沖刺”。當某個子目標變為活躍狀態時，所有證明器智能體同時對該同一個子目標獨立啟動并行的樹搜索。一旦任一智能體率先找到有效證明，子目標緩存立即記錄該證明，并通知所有其他智能體終止其搜索，從而避免冗余計算。隨后，所有證明器智能體同步進入序列中的下一個子目標。

3 實踐實現與基準測試結果

我們現在介紹 BFS-Prover-V2 系統的實際實現細節及其在標準基準上的測試結果。

模型與數據：
LLM 證明器智能體基于 Qwen2.5-Math-7B 和 Qwen2.5-32B 模型［37］構建，作為策略優化的基礎。多階段專家迭代流程以 BFS-Prover-V1 的檢查點［36］為初始狀態。為構建大規模訓練語料庫，我們使用精心設計的提示（prompts）對通用大模型進行調用，將 NuminaMath-CoT 和 NuminaMath-1.5 數據集［13］自動形式化為 Lean4 語句，并結合 Lean4 編譯器反饋進行增強。再結合 Goedel-Prover［16］提供的數據，該過程共生成約 300 萬條形式化命題。用于自動形式化的提示見附錄 C.1。所有實驗均在 Lean v4.10.0 環境下，通過 LeanDojo［39］完成。

訓練設置：
每輪專家迭代結束后，我們采用兩種監督微調（SFT）策略之一對策略 LLM 進行優化，具體選擇取決于該輪結果：

推理配置：我們的推理流程結合了低層證明器與高層規劃器（詳見第 2.4 節）。證明器智能體采用最佳優先搜索（BFS）算法，其實現沿用 BFS-Prover-V1［36］，設置采樣溫度為 1.3、擴展寬度為 3、長度歸一化因子為 2.0。高層戰略規劃器采用 Gemini2.5-Pro；若提示得當，其他通用推理模型也可達到相近性能。規劃器所用提示見附錄 C.2。

基準測試結果：我們在兩個關鍵基準上評估了 BFS-Prover-V2：

• miniF2F：測試高中數學競賽水平的問題；
• ProofNet：挑戰基于大型本科級數學庫的推理能力。

本系統在 LLM 逐步證明器中創下新紀錄：在 miniF2F 測試集上達到95.08%（驗證集達 95.49%），在 ProofNet 測試集上達到41.4%。miniF2F 上接近飽和的性能驗證了我們迭代式強化學習流程對特定問題分布的掌握能力；更重要的是，ProofNet 上的強勁表現表明系統能成功泛化——其訓練語料主要來自高中競賽題，卻能有效解決更復雜的、依賴大型數學庫的本科級問題。與其他 LLM 證明器的詳細對比見表 1。

4 結論

本工作的主要貢獻在于設計、實現并實證驗證了一套完整的系統，用于擴展基于大語言模型的逐步證明器。

• 訓練方面，我們的多階段專家迭代流程能夠克服常見的性能平臺期，支持在長期訓練中持續提升模型能力。
• 推理方面，我們提出了規劃器-證明器（Planner-Prover）范式，通過子目標分解與并行樹搜索協同工作。借助高層規劃器生成子目標，系統能夠攻克單體方法無法處理的復雜、多步定理。

BFS-Prover-V2 在 miniF2F 和 ProofNet 基準上取得的當前最優結果，有力證明了這一集成方法的有效性。

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