擴(kuò)展多輪離策略強(qiáng)化學(xué)習(xí)與多智能體樹(shù)搜索用于大語(yǔ)言模型逐步證明器

擴(kuò)展多輪離策略強(qiáng)化學(xué)習(xí)與多智能體樹(shù)搜索用于大語(yǔ)言模型逐步證明器

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

https://arxiv.org/pdf/2509.06493

摘要：

大語(yǔ)言模型（LLMs）與自動(dòng)定理證明的結(jié)合展現(xiàn)出巨大潛力，但仍受限于訓(xùn)練階段強(qiáng)化學(xué)習(xí)（RL）和推理階段計(jì)算資源的擴(kuò)展難題。本文提出 BFS-Prover-V2——一個(gè)開(kāi)源的、面向步驟級(jí)定理證明的系統(tǒng)，旨在同時(shí)解決上述雙重?cái)U(kuò)展挑戰(zhàn)。我們提出了兩項(xiàng)核心創(chuàng)新：

第一，一種新穎的多輪離策略強(qiáng)化學(xué)習(xí)（multi-turn off-policy RL）框架，用于在訓(xùn)練階段持續(xù)提升 LLM 逐步證明器的性能。該框架受 AlphaZero 原理啟發(fā)，采用多階段專家迭代流程，包含自適應(yīng)的策略級(jí)數(shù)據(jù)過(guò)濾機(jī)制和周期性重訓(xùn)練，以突破 LLM 智能體在長(zhǎng)期強(qiáng)化學(xué)習(xí)中常見(jiàn)的性能平臺(tái)期。

第二，一種規(guī)劃器增強(qiáng)的多智能體系統(tǒng)，在推理階段擴(kuò)展推理能力。該架構(gòu)使用一個(gè)通用推理模型作為高層規(guī)劃器，將復(fù)雜定理迭代地分解為一系列更簡(jiǎn)單的子目標(biāo)。這種分層方法顯著縮小了搜索空間，使得一組并行的證明智能體能夠通過(guò)共享證明緩存高效協(xié)作。

我們證明，這種訓(xùn)練與推理雙重?cái)U(kuò)展的方法在已有的形式化數(shù)學(xué)基準(zhǔn)上取得了當(dāng)前最優(yōu)的結(jié)果：BFS-Prover-V2 在 miniF2F 和 ProofNet 測(cè)試集上分別達(dá)到 95.08% 和 41.4% 的求解率。盡管本工作在形式化數(shù)學(xué)領(lǐng)域進(jìn)行驗(yàn)證，但所提出的強(qiáng)化學(xué)習(xí)與推理技術(shù)具有更廣泛的適用性，可推廣至其他需要長(zhǎng)視野、多輪推理與復(fù)雜搜索的任務(wù)領(lǐng)域。我們的模型與代碼已在 https://github.com/ByteDance-Seed/BFS-Prover-V2 開(kāi)源。

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

涵蓋超過(guò)一百萬(wàn)行代碼，Mathlib 覆蓋了代數(shù)、分析、拓?fù)涞榷鄠€(gè)廣泛的數(shù)學(xué)領(lǐng)域，為前沿?cái)?shù)學(xué)研究和經(jīng)過(guò)驗(yàn)證的系統(tǒng)開(kāi)發(fā)提供了豐富的基礎(chǔ)。Lean4 的興起恰逢大語(yǔ)言模型（LLMs）能力的爆炸式增長(zhǎng)［7, 20, 24］，由此開(kāi)辟了神經(jīng)符號(hào)人工智能系統(tǒng)的新前沿。這一方向的目標(biāo)是將 LLM 直觀而強(qiáng)大的生成與搜索能力，與形式化系統(tǒng)的絕對(duì)邏輯驗(yàn)證能力相結(jié)合。該研究路徑的核心是一個(gè)關(guān)鍵的反饋循環(huán)：LLM 提出直觀的證明步驟，Lean 編譯器提供嚴(yán)格的驗(yàn)證，而強(qiáng)化學(xué)習(xí)（RL）［28］則利用該驗(yàn)證信號(hào)持續(xù)提升 LLM 的推理能力［10, 12, 21, 34, 38］。

1.1 LLM 證明器與推理智能體中的雙重?cái)U(kuò)展挑戰(zhàn)

高性能 LLM 證明器（或任何其他推理智能體）的發(fā)展，取決于對(duì)兩個(gè)根本性且緊密關(guān)聯(lián)的擴(kuò)展挑戰(zhàn)的解決。

訓(xùn)練階段的擴(kuò)展（Training-time scaling）：指通過(guò)訓(xùn)練持續(xù)增強(qiáng)模型基礎(chǔ)能力與策略直覺(jué)所需的技術(shù)。在 LLM 上應(yīng)用 RL 時(shí)，一個(gè)常見(jiàn)且重大的障礙是“性能平臺(tái)期”現(xiàn)象：在初始快速提升階段之后，模型往往陷入停滯，即使繼續(xù)訓(xùn)練，其能力也不再增長(zhǎng)［9, 18, 24, 29, 34, 35, 41, 42］。要克服這一限制，需要精心設(shè)計(jì)的算法，使其能在長(zhǎng)時(shí)間內(nèi)維持學(xué)習(xí)能力，推動(dòng)模型從掌握簡(jiǎn)單問(wèn)題逐步過(guò)渡到攻克日益復(fù)雜的定理。

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

1.2 本文貢獻(xiàn)

本文提出BFS-Prover-V2——一個(gè)面向 Lean4 神經(jīng)定理證明的完整訓(xùn)練與推理系統(tǒng)，針對(duì)上述雙重?cái)U(kuò)展挑戰(zhàn)提出了創(chuàng)新性解決方案。本工作的主要貢獻(xiàn)如下：

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

2 BFS-Prover-V2 系統(tǒng)
本節(jié)詳細(xì)描述 BFS-Prover-V2 的兩個(gè)核心組成部分：(i) 一個(gè)基于馬爾可夫決策過(guò)程（MDP）［22］的訓(xùn)練流程，通過(guò)自適應(yīng)過(guò)濾和周期性重訓(xùn)練實(shí)現(xiàn)擴(kuò)展；(ii) 一個(gè)推理引擎，采用規(guī)劃器增強(qiáng)的多智能體搜索機(jī)制進(jìn)行分層推理。這兩個(gè)組件在 BFS-Prover-V1［36］的基礎(chǔ)上進(jìn)一步發(fā)展，專門針對(duì)訓(xùn)練與推理階段的雙重?cái)U(kuò)展挑戰(zhàn)。圖 1 和圖 4 提供了這些組件的可視化概覽，具體的實(shí)現(xiàn)參數(shù)詳見(jiàn)第 3.2 節(jié)。

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

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

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

2.2 基于最佳優(yōu)先樹(shù)搜索的專家迭代

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

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

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

2.3.1 自適應(yīng)策略過(guò)濾：從“恰到好處”的數(shù)據(jù)中學(xué)習(xí)

我們沒(méi)有采用粗粒度的、基于問(wèn)題級(jí)別的過(guò)濾方法［29, 41］（這類方法通常依賴靜態(tài)的難度指標(biāo)），而是提出了一種在策略級(jí)別（tactic level）上更動(dòng)態(tài)、更細(xì)粒度的過(guò)濾策略。該策略基于一個(gè)經(jīng)驗(yàn)性觀察：LLM 生成的策略的困惑度（perplexity，即負(fù)對(duì)數(shù)概率）大致呈高斯分布。如圖 2 所示，該分布可分為三個(gè)截然不同的區(qū)域，每個(gè)區(qū)域?qū)W(xué)習(xí)具有不同的意義：

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

2.3.2 周期性重訓(xùn)練：“軟重啟”以逃離局部最優(yōu)

即使采用自適應(yīng)過(guò)濾策略，在經(jīng)過(guò)若干輪專家迭代更新后，模型性能仍可能開(kāi)始進(jìn)入平臺(tái)期。這是因?yàn)槟Ｐ偷摹白C明風(fēng)格”逐漸固化：它對(duì)某些類型的策略和證明方法形成了強(qiáng)烈偏好，從而在龐大的推理策略空間中陷入局部最優(yōu)。此時(shí)，模型雖能非常高效地以特定方式解決某些問(wèn)題，卻喪失了發(fā)現(xiàn)新方法的能力——而這些新方法對(duì)于解決更新、更難的問(wèn)題類別至關(guān)重要。

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

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

   
   使用當(dāng)前性能最佳的證明器，重新求解其在所有過(guò)往迭代中遇到的全部問(wèn)題語(yǔ)料庫(kù)。由于該證明器如今遠(yuǎn)比早期輪次強(qiáng)大，它常常能找到更短、更直接、更優(yōu)雅的證明。這一步實(shí)質(zhì)上是讓專家模型對(duì)其自身過(guò)去的工作進(jìn)行去噪和優(yōu)化，濾除初始證明中因信息不足而產(chǎn)生的冗余或迂回步驟。

2. 激進(jìn)的數(shù)據(jù)精選（Aggressive Data Curation）

   
   將上一步生成的新高質(zhì)量證明，再次應(yīng)用前述的策略級(jí)困惑度過(guò)濾策略，但采用更嚴(yán)格的標(biāo)準(zhǔn)。大量數(shù)據(jù)被舍棄，僅保留最關(guān)鍵、最具信息量的策略步驟。

3. 從基礎(chǔ)檢查點(diǎn)重新訓(xùn)練（Retrain from a Base Checkpoint）

   
   用這一全新、高度精選且緊湊的數(shù)據(jù)集完全替換原有訓(xùn)練數(shù)據(jù)。隨后，從一個(gè)通用的預(yù)訓(xùn)練檢查點(diǎn)初始化一個(gè)全新的模型實(shí)例，并在此精煉數(shù)據(jù)集上從頭開(kāi)始訓(xùn)練。

如圖 3 所示，所得新模型在基準(zhǔn)測(cè)試上的性能初期會(huì)出現(xiàn)暫時(shí)性下降。這是預(yù)期之中的現(xiàn)象：因?yàn)樗窃谝粋€(gè)更小、更聚焦的數(shù)據(jù)集上訓(xùn)練的，并且“遺忘”了此前的一些風(fēng)格化偏好。然而，該新模型具備顯著更強(qiáng)的探索潛力。當(dāng)它被重新投入專家迭代循環(huán)后，其增強(qiáng)的探索能力使其能夠發(fā)現(xiàn)此前過(guò)度專業(yè)化模型無(wú)法觸及的新型證明策略。因此，其性能迅速恢復(fù)并超越之前的峰值，建立起更高的性能上限。圖 3 中標(biāo)記的“retrain”事件所代表的周期性重訓(xùn)練，是確保在數(shù)十輪訓(xùn)練中實(shí)現(xiàn)長(zhǎng)期、單調(diào)性能提升的關(guān)鍵機(jī)制。

2.4 推理擴(kuò)展：規(guī)劃器增強(qiáng)的多智能體搜索

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

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

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

• 規(guī)劃器（Planner）

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

• 證明器（Prover）

  
  這是通過(guò)第 2.3 節(jié)所述多階段專家迭代流程訓(xùn)練出的專用 LLM 策略生成器。它一次接收一個(gè)來(lái)自規(guī)劃器的子目標(biāo)，并結(jié)合其習(xí)得的策略與最佳優(yōu)先搜索（BFS）［36］，為該特定子目標(biāo)尋找形式化證明。

這種分工模擬了人類數(shù)學(xué)家的認(rèn)知工作流：先通過(guò)識(shí)別關(guān)鍵引理勾勒出證明的高層結(jié)構(gòu)（規(guī)劃器角色），再逐步填充每個(gè)引理的詳細(xì)、逐步演繹（證明器角色）。這種分層結(jié)構(gòu)是應(yīng)對(duì)復(fù)雜推理任務(wù)的強(qiáng)大架構(gòu)模式。

2.4.2 規(guī)劃引導(dǎo)搜索的運(yùn)行機(jī)制

如圖 4 所示，規(guī)劃器與證明器系統(tǒng)在動(dòng)態(tài)循環(huán)中交互，使計(jì)劃可根據(jù)證明進(jìn)展進(jìn)行調(diào)整：

1. 初始規(guī)劃（Initial Planning）

   
   在證明嘗試開(kāi)始時(shí)，向規(guī)劃器輸入主定理陳述，它返回一個(gè)以 Leanhave語(yǔ)句格式表示的子目標(biāo)列表。

2. 子目標(biāo)的順序證明（Sequential Proof of Subgoals）

   
   證明器系統(tǒng)依次處理這些子目標(biāo)。它從隊(duì)列中取出第一個(gè)子目標(biāo)，并啟動(dòng)樹(shù)搜索以尋找其證明。

3. 上下文增強(qiáng)（Context Augmentation）

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

4. 動(dòng)態(tài)重規(guī)劃（Dynamic Replanning）

   
   若證明器在給定計(jì)算預(yù)算內(nèi)未能找到某子目標(biāo)的證明（即“卡住”），系統(tǒng)不會(huì)終止。相反，會(huì)重新查詢規(guī)劃器。此時(shí)，規(guī)劃器的輸入不僅包含原始定理陳述，還包含所有在卡住前已成功證明的子目標(biāo)。基于這一新上下文，規(guī)劃器生成一個(gè)修訂后的計(jì)劃，通常會(huì)將“卡住”的子目標(biāo)進(jìn)一步分解為更細(xì)粒度的中間步驟，從而優(yōu)化原證明策略。

這種規(guī)劃與證明之間的動(dòng)態(tài)、迭代循環(huán)，使 BFS-Prover-V2 系統(tǒng)具備抗“卡死”能力，有效擴(kuò)展了其推理階段的能力，使其能夠攻克單體樹(shù)搜索無(wú)法處理的復(fù)雜定理。

2.4.3 通過(guò)聚焦并行與共享子目標(biāo)緩存實(shí)現(xiàn)多智能體協(xié)作

為加速證明搜索過(guò)程并減少實(shí)際運(yùn)行時(shí)間（wall-clock time），規(guī)劃器-證明器架構(gòu)被部署在一個(gè)多智能體框架中。我們并非依賴單一的證明器智能體，而是部署多個(gè)并行的證明器實(shí)例，共同協(xié)作執(zhí)行由規(guī)劃器生成的計(jì)劃。這種協(xié)作由兩個(gè)核心原則協(xié)調(diào)：聚焦并行策略（focused parallelism）和共享子目標(biāo)緩存（shared subgoal cache）。

聚焦并行（Focused Parallelism）：我們的系統(tǒng)并非將不同子目標(biāo)分配給不同的證明器智能體，而是將所有證明器實(shí)例的全部計(jì)算資源集中用于一次僅一個(gè)子目標(biāo)。該策略旨在克服單個(gè)智能體可能無(wú)法解決的推理瓶頸。此外，這種順序處理方式確保了計(jì)算效率：它避免了智能體在后續(xù)子目標(biāo)上浪費(fèi)資源——因?yàn)槿绻缙诓襟E失敗并觸發(fā)重規(guī)劃，這些后續(xù)子目標(biāo)可能變得無(wú)效。

共享子目標(biāo)緩存（Shared Subgoal Cache）：該緩存是所有并行證明器實(shí)例共享的核心通信與狀態(tài)跟蹤機(jī)制，承擔(dān)以下關(guān)鍵功能：

• 存儲(chǔ)規(guī)劃器生成的完整子目標(biāo)序列；
• 實(shí)時(shí)追蹤每個(gè)子目標(biāo)的狀態(tài)（例如：待處理、正在證明、已證明）；
• 記錄任何已求解子目標(biāo)的證明。

這一架構(gòu)為計(jì)劃中的每個(gè)引理（子目標(biāo)）組織了一場(chǎng)“協(xié)作式?jīng)_刺”。當(dāng)某個(gè)子目標(biāo)變?yōu)榛钴S狀態(tài)時(shí)，所有證明器智能體同時(shí)對(duì)該同一個(gè)子目標(biāo)獨(dú)立啟動(dòng)并行的樹(shù)搜索。一旦任一智能體率先找到有效證明，子目標(biāo)緩存立即記錄該證明，并通知所有其他智能體終止其搜索，從而避免冗余計(jì)算。隨后，所有證明器智能體同步進(jìn)入序列中的下一個(gè)子目標(biāo)。

3 實(shí)踐實(shí)現(xiàn)與基準(zhǔn)測(cè)試結(jié)果

我們現(xiàn)在介紹 BFS-Prover-V2 系統(tǒng)的實(shí)際實(shí)現(xiàn)細(xì)節(jié)及其在標(biāo)準(zhǔn)基準(zhǔn)上的測(cè)試結(jié)果。

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

訓(xùn)練設(shè)置：
每輪專家迭代結(jié)束后，我們采用兩種監(jiān)督微調(diào)（SFT）策略之一對(duì)策略 LLM 進(jìn)行優(yōu)化，具體選擇取決于該輪結(jié)果：

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

基準(zhǔn)測(cè)試結(jié)果：我們?cè)趦蓚€(gè)關(guān)鍵基準(zhǔn)上評(píng)估了 BFS-Prover-V2：

• miniF2F：測(cè)試高中數(shù)學(xué)競(jìng)賽水平的問(wèn)題；
• ProofNet：挑戰(zhàn)基于大型本科級(jí)數(shù)學(xué)庫(kù)的推理能力。

本系統(tǒng)在 LLM 逐步證明器中創(chuàng)下新紀(jì)錄：在 miniF2F 測(cè)試集上達(dá)到95.08%（驗(yàn)證集達(dá) 95.49%），在 ProofNet 測(cè)試集上達(dá)到41.4%。miniF2F 上接近飽和的性能驗(yàn)證了我們迭代式強(qiáng)化學(xué)習(xí)流程對(duì)特定問(wèn)題分布的掌握能力；更重要的是，ProofNet 上的強(qiáng)勁表現(xiàn)表明系統(tǒng)能成功泛化——其訓(xùn)練語(yǔ)料主要來(lái)自高中競(jìng)賽題，卻能有效解決更復(fù)雜的、依賴大型數(shù)學(xué)庫(kù)的本科級(jí)問(wèn)題。與其他 LLM 證明器的詳細(xì)對(duì)比見(jiàn)表 1。

4 結(jié)論

本工作的主要貢獻(xiàn)在于設(shè)計(jì)、實(shí)現(xiàn)并實(shí)證驗(yàn)證了一套完整的系統(tǒng)，用于擴(kuò)展基于大語(yǔ)言模型的逐步證明器。

• 訓(xùn)練方面，我們的多階段專家迭代流程能夠克服常見(jiàn)的性能平臺(tái)期，支持在長(zhǎng)期訓(xùn)練中持續(xù)提升模型能力。
• 推理方面，我們提出了規(guī)劃器-證明器（Planner-Prover）范式，通過(guò)子目標(biāo)分解與并行樹(shù)搜索協(xié)同工作。借助高層規(guī)劃器生成子目標(biāo)，系統(tǒng)能夠攻克單體方法無(wú)法處理的復(fù)雜、多步定理。

BFS-Prover-V2 在 miniF2F 和 ProofNet 基準(zhǔn)上取得的當(dāng)前最優(yōu)結(jié)果，有力證明了這一集成方法的有效性。

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