BFS-Prover：面向大語言模型自動定理證明的可擴展最佳優先樹搜索

BFS-Prover：面向大語言模型自動定理證明的可擴展最佳優先樹搜索

BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving

https://arxiv.org/pdf/2502.03438

摘要：

近期大語言模型（LLMs）的進展激發了利用 Lean4 進行自動定理證明的廣泛興趣，其中高效的樹搜索方法對于應對底層龐大的證明搜索空間至關重要。盡管現有方法主要依賴價值函數和/或蒙特卡洛樹搜索（MCTS），但更簡單的方法（如最佳優先樹搜索，BFS）的潛力尚未得到充分探索。本文研究了 BFS 是否能在大規模定理證明任務中實現具有競爭力的性能。

我們提出了 BFS-Prover，一個可擴展的專家迭代框架，包含三項關鍵創新：
第一，在每輪專家迭代中實施策略性數據過濾，排除那些通過束搜索節點擴展即可解決的問題，從而聚焦于更具挑戰性的案例；
第二，通過對狀態-策略對（state-tactic pairs）應用直接偏好優化（DPO），提升 BFS 的樣本效率——這些狀態-策略對利用編譯器錯誤反饋自動標注，從而優化 LLM 的策略，使其優先選擇更有成效的擴展；
第三，在 BFS 中引入長度歸一化，以鼓勵探索更深的證明路徑。

BFS-Prover 在 MiniF2F 測試集上取得了 72.95% 的當前最優成績，挑戰了復雜樹搜索方法必不可少的普遍認知，表明在適當擴展下，BFS 同樣能實現具有競爭力的性能。為促進該領域的進一步研究與發展，我們已在 https://huggingface.co/ByteDance-Seed/BFS-Prover-V1-7B 開源我們的模型。

1 引言

形式化語言中的自動定理證明（ATP）近期已成為評估大語言模型（LLMs）推理能力的關鍵基準。通過將數學問題編碼到如 Lean4 等形式系統中，ATP 能夠為復雜的數學命題生成機器可驗證的證明，從而確保邏輯正確性（Moura 和 Ullrich，2021；Polu 與 Sutskever，2020）。盡管 LLMs 在自然語言數學和推理任務中取得了顯著成功（Lewkowycz 等，2022；OpenAI，2023），但在形式化語言中的定理證明仍面臨獨特挑戰（Yang 等，2024b；Wu 等，2022；He 等，2024；Wang 等，2023，2024；Lin 等，2024；Xin 等，2024a）。與非形式化推理不同，形式系統要求嚴格遵守語法和語義，并且必須在高度受限的形式框架內生成有效步驟。此外，ATP 中的動作（策略，tactic）空間極為龐大——每個證明狀態都可能引出大量潛在策略，使得有效證明的搜索過程在計算上非常昂貴（Polu 等，2022）。

樹搜索算法是 ATP 的基礎，使策略模型能夠高效地在龐大而復雜的證明空間中導航（Polu 與 Sutskever，2020）。在這些方法中，蒙特卡洛樹搜索（MCTS）（Coulom，2006）因其能利用價值函數（評判模型）或內在獎勵在探索與利用之間取得平衡而廣受歡迎（Browne 等，2012；Silver 等，2016）。MCTS 在 AlphaZero 類框架中已展現出卓越成效，例如在國際象棋和圍棋等游戲中（Silver 等，2017），這些游戲的狀態空間雖大，但終止狀態定義明確。然而，將 MCTS 和/或價值函數應用于 ATP 時會遇到特殊困難。與游戲具有清晰的勝負條件不同，證明搜索缺乏此類明確的終止狀態：一次證明嘗試理論上可以無限進行下去，直到找到證明或反例為止，這使得評估中間進展變得極具挑戰性（Han 等，2021；Lample 等，2022）。此外，ATP 涉及更大且更動態的分支因子、稀疏且延遲的反饋，以及開放式推理過程。這些差異凸顯了 ATP 的獨特需求，也表明有必要對搜索方法進行專門適配，以應對其中的復雜性。

最佳優先樹搜索（BFS）（Pearl，1984）提供了一種比 MCTS 更簡單、更輕量的替代方案，其通過當前節點到根節點路徑上累積的對數概率來優先擴展節點。盡管其簡潔性和計算效率頗具吸引力，但現有文獻通常認為 BFS 在定理證明中表現欠佳（Wu 等，2024a；Li 等，2024b；Xin 等，2024b），主要基于以下假設：

• 缺乏高效探索能力：BFS 優先選擇高概率路徑，容易忽略那些概率較低但有效的解。由于缺乏諸如置信上限（UCB）或價值函數等探索機制，它難以在利用有希望的節點與探索多樣化路徑之間取得平衡。
• 對深度推理路徑存在偏見：BFS 依賴累積對數概率，本質上會懲罰較長路徑，因為更深的擴展往往累積更低的得分。這種偏見使其在處理需要深度證明的定理時效果較差——這類定理的中間狀態可能看似無望，卻是最終找到解的關鍵所在。

1.1 本文貢獻
本文挑戰了當前普遍認為 BFS 本質上不適用于大規模自動定理證明（ATP）的觀點。我們提出了 BFS-Prover 系統，通過有針對性的擴展策略，將 BFS 轉變為一種簡潔而強大的算法。我們的主要貢獻如下：

• 帶自過濾機制的專家迭代：我們構建了一個專家迭代（Anthony 等，2017）框架，在每輪迭代中策略性地過濾掉那些可通過束搜索（beam search）（Steinbiss 等，1994）節點擴展即可解決的問題。這種過濾至關重要，因為它引導訓練數據的積累聚焦于更困難的定理。隨著專家迭代的推進，策略大語言模型（LLM）持續改進，通過 BFS 學習到更多樣化的策略和更深的證明路徑。
• 基于編譯器反饋的直接偏好優化（DPO）：我們利用 DPO（Rafailov 等，2024）來優化策略 LLM，所用的偏好對是在樹搜索過程中自然生成的。對于給定的證明狀態，每個偏好對包含一個正向策略（位于正確證明路徑上）和一個負向策略（導致 Lean 編譯器報錯）。DPO 使策略分布更加銳化，使其能夠避免無效策略，從而提升 BFS 的樣本效率。
• 用于深度探索的長度歸一化：我們在 BFS 中引入了一種長度歸一化的評分函數，以緩解其對深度推理路徑的固有偏見。通過對路徑長度歸一化對數概率，BFS 能更有效地探索更深的證明路徑，從而解決那些需要長策略鏈的定理。
• 在 MiniF2F 上的實證結果：BFS-Prover 在 MiniF2F 測試集上取得了 72.95% 的累積得分，超越了文獻中所有當前最先進的定理證明系統，包括 DeepSeek-Prover-V1.5（Xin 等，2024b）、InternLM2.5-StepProver（Wu 等，2024a）和 HunyuanProver（Li 等，2024b）。這一結果表明，BFS-Prover 能在保持輕量級設計（無需 MCTS 和價值函數的復雜機制）的同時，在自動定理證明任務中達到具有競爭力的性能水平。

論文結構安排：本文其余部分組織如下。第 2 節概述 BFS-Prover 系統，詳細說明專家迭代框架、數據過濾機制、用于策略優化的 DPO 方法，以及 BFS 中的長度歸一化。第 3 節描述在 MiniF2F 基準上的實際實現細節與實驗結果，并與主流證明系統進行對比。第 4 節總結全文。

2 BFS-Prover 系統

本節詳細說明 BFS-Prover 系統的設計；圖 1 為系統示意圖。

2.1 Lean4 環境與策略大語言模型

我們采用 LeanDojo（Yang 等，2024c）作為 Lean4 與 BFS-Prover 集成的交互式 Python 接口。它將 Lean4 轉化為類似 Gym 的環境（Brockman，2016），便于策略大語言模型（LLM）與形式化證明助手之間的交互。具體而言，LeanDojo 通過在 Lean4 編譯器中執行策略 LLM 生成的策略（tactic）來管理狀態轉移。如果某策略無法執行，LeanDojo 會捕獲并返回相應的錯誤信息，為 DPO 提供關鍵反饋，用于優化策略 LLM。

2.2 長度歸一化的最佳優先樹搜索

BFS-Prover 采用一種最佳優先樹搜索（BFS）的變體，以在龐大的狀態-策略空間中進行證明搜索。該 BFS 引擎維護一個證明節點（即狀態）的優先隊列，其中每個節點（狀態）的優先級由一種長度歸一化的評分啟發函數定義：

該評分機制結合可調節的節點擴展寬度，使 BFS 能夠在證明空間中動態分配計算資源，在探索與利用之間取得平衡。例如，增大 α 值和/或減小擴展寬度會使搜索系統傾向于探索更深的路徑，從而促進發現那些可能需要長策略鏈的復雜證明。

在每次節點擴展步驟中，策略大語言模型（LLM）通過某種采樣機制生成一組策略（tactics），這些策略對應于證明樹中的邊。LeanDojo 隨后在 Lean4 編譯器中執行這些采樣的策略，并返回執行結果。對于每個策略的應用，可能出現三種結果：(1) 如果該策略產生一個有效的證明狀態，則創建一個常規樹節點并加入節點隊列；(2) 如果該策略完成了整個證明，則創建一個“證明完成”節點并返回該證明；(3) 否則，生成一個終止性錯誤節點，表示該路徑無效。

2.3 專家迭代
BFS-Prover 采用一個專家迭代（expert iteration）流程，以迭代方式增強策略大語言模型（LLM）在復雜證明空間中導航的能力。給定一個包含未解決 Lean4 形式化命題的語料庫，每輪專家迭代包含以下步驟：

1. 束搜索過濾（Beam Search Filtering）：識別出那些可通過 BFS 配合束搜索節點擴展即可證明的形式化命題。這些命題隨后從語料庫中移除，其對應的證明數據——盡管是新生成的——被有意不加入累積的訓練數據集中。束搜索具有確定性，能可靠地選擇當前策略 LLM 生成的置信度最高的策略。因此，能通過該方法解決的證明被視為相對簡單，因為它們與當前 BFS-Prover 系統的優勢高度一致。通過策略性地濾除這些較簡單的證明，訓練數據語料庫在迭代過程中不斷被更具挑戰性和多樣性的樣例所豐富。這種迭代式精煉確保策略 LLM 在后續迭代中逐步接觸越來越復雜的推理模式，從而提升其解決更難定理的能力。
2. 數據收集（Data Collection）：隨后，我們對語料庫中剩余未證明的形式化命題執行帶有溫度采樣的 BFS 擴展以搜索證明。任務完成后，系統收集所有在成功證明路徑上遇到的有效（證明狀態，策略）對，并將其加入累積的訓練數據集。相應已被證明的命題則從語料庫中移除。此外，導致 Lean 編譯器報錯的無效策略也被記錄下來，作為策略內（on-policy）的負樣本，用于支持 DPO 的優化。
3. 監督微調（Supervised Fine-Tuning, SFT）：在每次數據收集階段之后，使用基礎模型在全部累積的訓練數據語料庫上進行 SFT，訓練出一個新的策略 LLM。該語料庫包含此前所有專家迭代輪次中生成的（證明狀態，策略）對。
   

這一專家迭代流程使策略 LLM 能夠持續提升其生成有效策略的能力，同時隨著訓練數據語料庫的增長，逐步適應更具挑戰性的證明場景。

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

本節討論 BFS-Prover 系統的實際實現細節，并展示其在 MiniF2F 測試集上的基準測試結果。所有實驗均使用 Lean 4.7.0。

3.1 模型、數據與訓練設置

基礎模型與初始訓練數據：為便于說明，我們在 BFS-Prover 中采用 Qwen2.5-Math-7B（Yang 等，2024a）作為策略大語言模型（LLM）微調的基礎模型。為合理初始化專家迭代過程，我們利用 LeanDojo（Yang 等，2024c）從 Mathlib（Moura 和 Ullrich，2021）中提取的證明數據，作為冷啟動（cold-start）數據集。隨著專家迭代的推進，我們進一步整合來自 Lean-Github（Wu 等，2024b）——一個匯集 GitHub 上 Lean4 倉庫的數據集——以及 Lean-Workbook（Ying 等，2024）——專注于奧數級別代數與分析的數據集——的狀態-策略（state-tactic）數據。這些數據集覆蓋了廣泛的數學主題和形式化推理任務，為策略模型提供了生成有效策略和導航證明所需的基礎能力。

形式化命題語料庫：為構建專家迭代所用的數據語料庫，我們使用內部工具對 NuminaMath-CoT 數據集（Li 等，2024a）進行自動形式化（autoformalization）。我們還補充了來自 Mathlib 的未證明定理以及 Lean-Workbook 中的形式化命題。最終形成的語料庫包含約 90 萬條無證明的形式化數學命題，為專家迭代提供了全面而堅實的基礎。

專家迭代中的 BFS 配置。我們在整個專家迭代過程中將長度歸一化參數 α 設為 0.0，以盡量減少歸納偏置。在束搜索過濾階段，我們使用束寬（beam width）為 32，以識別容易求解的定理。在隨后的數據收集階段，我們采用基于溫度的采樣策略，溫度設為 1.0，核采樣（nucleus sampling）參數為 1.0，并設置采樣寬度（sampling width）為 2、4 或 8，以探索多樣化的證明路徑。

3.2 分布式最佳優先搜索基礎設施

為實現高效的大規模并行證明搜索，我們基于 Ray 構建了一個分布式系統，在多臺機器上進行分布式定理證明。每臺機器配備 8 塊 A100 80GB GPU 和 128 個 CPU 核心。目標定理被均勻分配到各臺機器上，每臺機器運行一個獨立的證明流水線。該系統由三個主要組件構成：

• 基于 GPU 的策略 LLM 池：每臺本地機器部署 8 個 7B 策略 LLM 實例，每個實例由一個專用 A100 GPU 上運行的異步 vLLM 引擎驅動。這些實例組成一個共享池，用于處理并發的策略生成請求。
• 基于 CPU 的證明器池：每臺機器運行 96 個并發的證明器實例，其余 CPU 核心保留用于常規系統操作。每個證明器實例對其分配到的定理獨立執行 BFS 搜索。為實現均衡的 GPU 利用率，各證明器根據其索引對 8 取模的結果，以輪詢（round-robin）方式將請求分發到不同的策略 LLM 實例上。每個證明器與其分配的策略 LLM 和 LeanDojo 環境進行異步交互。
• 異步交互機制：整個分布式搜索系統利用 asyncio 管理證明器與策略 LLM 之間的高并發工作流。策略 LLM 池和證明器池均以 Ray Actor 的形式實現，通過 Ray 運行時系統實現動態資源管理。為確保系統響應性，我們對策略執行（通過 LeanDojo）和模型推理（通過 vLLM）均設置了超時閾值。

該分布式基礎設施設計通過在機器間高效分配定理任務，實現了接近線性的擴展能力；同時在單機內部最大化硬件利用率，且無需承擔跨機器通信開銷。

3.3 專家迭代中的分布偏移

在本小節中，我們討論并展示在專家迭代過程中，證明層面和策略層面如何出現分布偏移（distribution shift），從而揭示 BFS-Prover 在定理證明能力上的逐步提升。

證明層面。評估一個證明系統（如 BFS-Prover）有效性的一個關鍵指標，是其發現深度證明的能力。我們將“證明長度”定義為系統完成一個證明所使用的策略（tactic）數量。我們觀察到，在每輪專家迭代中，證明長度的分布通常呈現高斯分布或高斯混合分布，這反映了形式化命題語料庫中定理復雜度的多樣性。有趣的是，隨著專家迭代的推進，平均證明長度趨于增加，表明隨著策略大語言模型（LLM）能力的提升，BFS 能夠發現越來越深、更具挑戰性的證明；參見圖 2 的示意圖。這一現象凸顯了專家迭代框架的有效性以及 BFS 的可擴展性——即通過迭代式策略優化和搜索能力的增強，逐步應對更復雜的證明任務。

策略層面。除了在證明層面的演化之外，我們在專家迭代過程中也觀察到策略層面有趣的分布偏移；參見圖 3。值得注意的是，BFS-Prover 系統中的策略 LLM 在整個訓練過程中維持著多樣化的策略長度分布，并未坍縮為單一狹窄分布——后者是強化學習中常見的失敗模式，即模型傾向于收斂于少數高獎勵動作（Sutton，2018）。相反，我們觀察到一種溫和但有意義的分布轉移：從極簡策略（1–10 個 token）向更常用、更實用的策略模式（11–50 個 token）過渡。這種轉移表明，通過專家迭代，BFS-Prover 中的策略 LLM 學會生成更復雜的策略，同時仍保留根據情境靈活使用簡單策略的能力。保持策略多樣性對于有效定理證明至關重要，因為不同的證明狀態需要不同復雜度的策略，從簡單的項重寫到復雜的代數操作不等。

3.4 MiniF2F 上的結果

本小節討論 BFS-Prover 在 MiniF2F 測試基準（Zheng 等，2021）上的表現。MiniF2F 是一個被廣泛認可的用于評估形式化數學系統性能的數據集，包含一系列多樣化的、源自數學競賽級別的形式化問題。用于評估的策略大語言模型（LLM）檢查點，是通過對 BFS-Prover 專家迭代流程中前 10 輪累積的所有狀態-策略對進行監督微調（SFT）獲得的，并在此基礎上額外進行了一輪 DPO 優化，所用的 Lean 編譯器錯誤信號如第 2.3 節所述。

3.4.1 與當前最先進方法的比較

我們現在將本文開發的 BFS-Prover 與文獻中的主流定理證明系統進行比較，包括 DeepSeek-Prover-V1.5（Xin 等，2024b）、InternLM2.5-StepProver（Wu 等，2024a）和 HunyuanProver（Li 等，2024b）。

3.4.2 BFS 的縮放規律與 DPO 負信號的優勢

最后，我們通過考察 BFS-Prover 在 MiniF2F 測試基準上的性能如何隨證明搜索遍數（passes）的增加而提升，來研究其搜索時間的縮放規律，并評估利用 DPO 從負信號中學習對系統性能提升所帶來的優勢。我們總共執行了 pass@4096 實驗，并在 pass@64、pass@128、pass@256、pass@1024 和 pass@2048 等中間節點評估性能。每個中間遍數的置信區間通過多次采樣 pass@64 的運行結果計算得出。實驗結果如圖 4 所示，其中橫軸采用對數刻度，陰影區域表示最小-最大范圍（即置信區間）。

以下是我們對形式化定理證明中 BFS 縮放特性的若干觀察。此處，SFT 指在專家迭代流程中累積的所有狀態-策略對上進行的監督微調；SFT+DPO 則指在 SFT 模型基礎上，額外應用一輪 DPO 優化，所用的策略內負樣本來自 Lean4 編譯器反饋（如第 2.3 節所述）。兩種方法均采用相同的 BFS 參數配置：采樣溫度為 1.1，擴展寬度為 2，長度歸一化因子 α = 0.5 。

• SFT 與 SFT+DPO 兩種訓練方法均表現出對數縮放規律：隨著證明搜索遍數的增加，性能提升逐漸放緩。具體而言，當遍數從 64 增至 2048 時，SFT 的得分從 64.58% 提升至 70.38%，而 SFT+DPO 從 64.98% 提升至 70.83%。這表明即使計算預算翻倍，性能增益也呈現持續但遞減的趨勢。
• SFT+DPO 方法始終優于 SFT 基線，證明了引入來自 Lean4 編譯器錯誤的負反饋的有效性。這種優化使模型能更好地區分成功與失敗的證明策略，從而提升證明搜索效率和成功率。
• 從最小-最大范圍來看，兩種方法的性能波動幅度相近（約 3–4%）。這表明，盡管 DPO 提高了整體成功率，但其在證明搜索中的穩定性與 SFT 基線相當。

4 結論與討論

本工作表明，最佳優先搜索（BFS）能夠高效擴展，并在自動定理證明（ATP）中取得當前最優的性能。我們的結果挑戰了傳統觀點——即在大規模形式化定理證明中，必須依賴蒙特卡洛樹搜索（MCTS）和/或價值函數等更復雜的搜索方法。通過開發 BFS-Prover，我們論證了：一個經過精心設計的 BFS 系統，若結合專家迭代框架，并融入策略性數據過濾、直接偏好優化（DPO）和長度歸一化等機制，不僅能在性能上超越現有方法，還能保持計算上的簡潔性。我們在 MiniF2F 基準上取得 72.95% 的當前最優得分，實證驗證了該方法的可擴展性。

BFS-Prover 的成功對 ATP 領域具有若干重要啟示。首先，它表明算法的簡潔性若輔以周密的擴展策略，完全可以勝過更復雜的方案。這一發現提示未來 ATP 研究或許應更多關注對簡單方法的精煉與擴展，而非一味追求日益復雜的架構。其次，我們觀察到 BFS 性能隨計算資源增加而呈現對數縮放規律，這說明盡管增加計算量總能帶來一定提升，但僅靠擴大搜索規模可能存在根本性局限。這一觀察激勵未來研究探索能夠實現優于對數縮放（better-than-logarithmic scaling）的新方法。

局限性

盡管 BFS-Prover 系統在自動定理證明中展現出強大的性能，但仍存在若干局限性，尤其體現在模型規模方面。我們當前的實現依賴于一個相對較小的 70 億參數（7B）策略模型，這可能會限制系統學習和運用更復雜數學推理模式的能力。雖然更大的模型（例如 32B 或 70B 參數）有可能捕捉更深刻的數學洞見并生成更精細的策略，但它們在樹搜索場景下會帶來顯著的計算挑戰，無論是在訓練還是推理階段。

這種權衡在實踐中尤為明顯：更大的模型通常需要更多的 GPU 顯存，并具有更長的推理延遲，這會顯著減少在固定時間預算內可探索的狀態數量。此外，復雜的數學證明可能生成非常冗長的狀態描述，這些描述可能超出 7B 模型的實際上下文窗口長度，從而導致模型遺漏生成恰當策略所必需的關鍵信息。

原文： https://arxiv.org/pdf/2502.03438