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

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

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

https://arxiv.org/pdf/2502.03438

摘要：

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

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

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

1 引言

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

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

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

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

1.1 本文貢獻
本文挑戰(zhàn)了當前普遍認為 BFS 本質(zhì)上不適用于大規(guī)模自動定理證明（ATP）的觀點。我們提出了 BFS-Prover 系統(tǒng)，通過有針對性的擴展策略，將 BFS 轉(zhuǎn)變?yōu)橐环N簡潔而強大的算法。我們的主要貢獻如下：

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

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

2 BFS-Prover 系統(tǒng)

本節(jié)詳細說明 BFS-Prover 系統(tǒng)的設(shè)計；圖 1 為系統(tǒng)示意圖。

2.1 Lean4 環(huán)境與策略大語言模型

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

2.2 長度歸一化的最佳優(yōu)先樹搜索

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

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

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

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

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

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

3 實踐實現(xiàn)與基準測試結(jié)果

本節(jié)討論 BFS-Prover 系統(tǒng)的實際實現(xiàn)細節(jié)，并展示其在 MiniF2F 測試集上的基準測試結(jié)果。所有實驗均使用 Lean 4.7.0。

3.1 模型、數(shù)據(jù)與訓(xùn)練設(shè)置

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

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

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

3.2 分布式最佳優(yōu)先搜索基礎(chǔ)設(shè)施

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

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

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

3.3 專家迭代中的分布偏移

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

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

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

3.4 MiniF2F 上的結(jié)果

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

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

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

3.4.2 BFS 的縮放規(guī)律與 DPO 負信號的優(yōu)勢

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

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

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

4 結(jié)論與討論

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

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

局限性

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

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

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