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

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

https://arxiv.org/pdf/2502.03438

摘要：

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

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

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

1 引言

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

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

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

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

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

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

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

2 BFS-Prover 系統(tǒng)

本節(jié)詳細(xì)說明 BFS-Prover 系統(tǒng)的設(shè)計(jì)；圖 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 會(huì)捕獲并返回相應(yīng)的錯(cuò)誤信息，為 DPO 提供關(guān)鍵反饋，用于優(yōu)化策略 LLM。

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

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

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

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

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

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

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

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

本節(jié)討論 BFS-Prover 系統(tǒng)的實(shí)際實(shí)現(xiàn)細(xì)節(jié)，并展示其在 MiniF2F 測試集上的基準(zhǔn)測試結(jié)果。所有實(shí)驗(yàn)均使用 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ù)，作為冷啟動(dòng)（cold-start）數(shù)據(jù)集。隨著專家迭代的推進(jìn)，我們進(jìn)一步整合來自 Lean-Github（Wu 等，2024b）——一個(gè)匯集 GitHub 上 Lean4 倉庫的數(shù)據(jù)集——以及 Lean-Workbook（Ying 等，2024）——專注于奧數(shù)級(jí)別代數(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）進(jìn)行自動(dòng)形式化（autoformalization）。我們還補(bǔ)充了來自 Mathlib 的未證明定理以及 Lean-Workbook 中的形式化命題。最終形成的語料庫包含約 90 萬條無證明的形式化數(shù)學(xué)命題，為專家迭代提供了全面而堅(jiān)實(shí)的基礎(chǔ)。

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

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

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

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

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

3.3 專家迭代中的分布偏移

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

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

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

3.4 MiniF2F 上的結(jié)果

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

3.4.1 與當(dāng)前最先進(jìn)方法的比較

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

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

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

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

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

4 結(jié)論與討論

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

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

局限性

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

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

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