近日，豆包大模型團隊提出 BFS-Prover，一個基于大語言模型 (LLM) 和最優(yōu)先樹搜索 (BFS) 的高效自動形式化定理證明系統(tǒng)。

團隊通過該成果發(fā)現(xiàn)，簡單的 BFS 方法經(jīng)過系統(tǒng)優(yōu)化后，可在大規(guī)模定理證明任務中展現(xiàn)卓越性能與效率，無需復雜的蒙特卡洛樹搜索和價值函數(shù)。

在數(shù)學定理證明基準 MiniF2F 測試集上，BFS-Prover 取得了 72.95% 準確率，超越此前所有方法。

自動形式化數(shù)學定理證明，是人工智能在數(shù)學推理領域的重要應用方向。此類任務需要將數(shù)學命題和證明步驟轉化為計算機可驗證的代碼，這不僅能確保推理過程的絕對嚴謹性，還能構建可復用的數(shù)學知識庫，為科學研究提供堅實基礎。

早在上世紀中葉，戴維斯、明斯基、王浩等不少邏輯學家、數(shù)學家、人工智能先驅便已在探索相關問題。

近些年在 LLM 能力加持下，自動定理證明系統(tǒng)更多依賴于復雜的蒙特卡洛樹搜索 (MCTS) 或價值函數(shù) (Value Function) 來指導搜索過程。

然而，這些方法引入了額外計算成本，并增加系統(tǒng)復雜度，使模型在大規(guī)模推理任務中的可擴展性受限。

字節(jié)跳動豆包大模型團隊推出的 BFS-Prover 挑戰(zhàn)了這一傳統(tǒng)范式。

作為一種更簡單、更輕量但極具競爭力的自動定理證明系統(tǒng)，它引入了三項關鍵技術：專家迭代 (Expert Iteration) 與自適應性數(shù)據(jù)過濾、直接偏好優(yōu)化 (DPO) 結合 Lean4 編譯器反饋、BFS 中的長度歸一化。

從結果看，BFS-Prover 在形式化數(shù)學測試集 MiniF2F 上實現(xiàn)了 72.95% 的準確率，創(chuàng)造了新的領域記錄。

該結果也首次證明：在合理的優(yōu)化策略下，簡單的 BFS 方法能夠超越蒙特卡洛樹搜索和價值函數(shù)等主流的復雜搜索算法。

目前，論文成果已對外公開，模型也最新開源，期待與相關研究者做更進一步交流。

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

論文鏈接：https://arxiv.org/abs/2502.03438

HuggingFace 鏈接：https://huggingface.co/bytedance-research/BFS-Prover

1. 主流方法蒙特卡洛樹搜索和價值函數(shù)真的必要么？ 

在形式化數(shù)學證明領域，將抽象的數(shù)學概念轉化為能夠用計算機驗證的嚴格形式，是一項極具挑戰(zhàn)性的任務。

該過程要求每一步推理都符合嚴格的形式邏輯規(guī)則，且每個步驟都必須經(jīng)過 Lean 證明助手驗證。

在自動形式化定理證明過程中，計算機面臨的核心挑戰(zhàn)是——在龐大且高度結構化的證明空間中，找出有效路徑。這一難點與傳統(tǒng)搜索問題有本質區(qū)別，具體表現(xiàn)如下：

1）搜索空間龐大：每一步推理可能有數(shù)十甚至上百種可能的策略選擇；

2）動態(tài)變化的策略空間：不同于棋類游戲的固定規(guī)則，數(shù)學定理證明中，每個狀態(tài)下可應用的策略集合不斷變化，且規(guī)模龐大，無明確界限；

3）反饋稀疏與延遲：直到完成證明前，系統(tǒng)很難獲得有效的中間反饋；

4）開放式推理過程：缺乏明確的終止條件，證明嘗試可能無限延續(xù)；

自動定理證明系統(tǒng)如 DeepSeek-Prover-V1.5、InternLM2.5-StepProver，主要依賴復雜的蒙特卡洛樹搜索和價值函數(shù)解決上述問題。

這些類 AlphaZero 算法框架在游戲中表現(xiàn)出色，尤其在圍棋領域大放異彩，推動了強化學習概念破圈。但在自動定理證明領域，由于狀態(tài)空間極其復雜以及缺乏明確的過程獎勵信號，上述主流方法效果并不理想。此外，復雜的搜索算法還帶來了計算成本高、系統(tǒng)復雜度增加等問題。

2. 化繁為簡，用機器證明數(shù)學定理可以更簡單 

人類遇到問題，往往優(yōu)先采用最可能解決的方法。最優(yōu)先樹搜索（BFS）與之類似。

這是一種在“樹”或“圖”中搜索節(jié)點的算法。核心思想是根據(jù)某種啟發(fā)式函數(shù)，評估每個節(jié)點優(yōu)先級，按優(yōu)先級訪問節(jié)點，常用于解決約束滿足問題和組合優(yōu)化問題，特別是在需要快速找到近似最優(yōu)解的情況下。

此前不少研究者認為，簡單的 BFS 算法缺乏有效的探索機制，尤其是對深度路徑的探索，難以勝任大規(guī)模定理證明任務，但豆包大模型團隊的研究者發(fā)現(xiàn)了其中的突破口，并提出了 BFS-Prover 系統(tǒng)。

下圖展示了 BFS-Prover 系統(tǒng)的整體架構和工作流程。

圖右側展示了訓練數(shù)據(jù)生成過程，包括用于監(jiān)督微調的 SFT 數(shù)據(jù) (成功證明路徑上的狀態(tài)-策略對) 和用于直接偏好優(yōu)化的 DPO 數(shù)據(jù) (從同一狀態(tài)出發(fā)的正確策略與錯誤策略的對比)。

圖左側展示了 BFS 機制，通過 LeanDojo 環(huán)境與 Lean4 交互，從根節(jié)點開始，按照優(yōu)先級順序 (1→2→3...) 探索證明路徑，直到找到證明完成節(jié)點 (綠色 A 點)。

整個系統(tǒng)形成閉環(huán)：LLM 生成策略 → LeanDojo 執(zhí)行 → 獲取反饋 → 生成訓練數(shù)據(jù)→優(yōu)化 LLM → 再次生成策略，實現(xiàn)了持續(xù)改進的專家迭代機制。

團隊認為，BFS-Prover 系統(tǒng)不僅證明了經(jīng)過優(yōu)化的 BFS 方法性能方面可以超越復雜的蒙特卡洛樹搜索和價值函數(shù)，并且能保持架構的簡潔性和計算效率。其技術特征如下：

• 讓模型既能深度思考策略，也能掌握最簡證明方式

BFS-Prover 采用專家迭代框架，通過多輪迭代不斷增強 LLM 能力。在每輪迭代中，系統(tǒng)會先使用確定性的束搜索 (Beam Search) 方法過濾掉容易解決的定理，將這些“簡單問題”從訓練數(shù)據(jù)中剔除，再著手解決“復雜問題”。

這一數(shù)據(jù)過濾機制頗具創(chuàng)新性，確保了訓練數(shù)據(jù)逐漸向更具挑戰(zhàn)性的定理證明任務傾斜，使 LLM 能夠學習更多元化的證明策略。

如下圖實驗數(shù)據(jù)顯示，隨迭代進行，系統(tǒng)能夠發(fā)現(xiàn)證明的平均長度變長，覆蓋面變廣，證明了這一方法的有效性。

與此同時，LLM 生成的策略分布也發(fā)生進化。

如下圖所示，經(jīng)過多輪迭代，模型生成的策略長度分布發(fā)生了顯著變化：非常短的策略（1-10 個 token）比例下降，而中等長度策略（11-50 個 token）比例則有所增加。

這種分布變化表明，LLM “深度思考能力”在加強，避免了常見的強化學習導致的分布坍縮問題，并逐漸掌握了更復雜、更信息豐富的證明策略。

同時，模型生成簡潔策略的能力并未摒棄。這種多樣策略生成能力的保持，對于有效定理證明至關重要。因為不同的證明狀態(tài)，需要不同復雜度的策略，涵蓋從簡單的項重寫，到復雜的代數(shù)操作。

• 從過程中總結“錯誤證明步驟”，提升證明能力

在證明搜索過程中，當 LLM 生成的某些策略導致 Lean4 編譯器錯誤，系統(tǒng)將這些無效策略與成功策略配對，形成負反饋信號。

BFS-Prover 創(chuàng)新性地依靠這些數(shù)據(jù)，基于直接偏好優(yōu)化(DPO)技術優(yōu)化策略 LLM。此種方法顯著提高了模型識別有效策略的能力，優(yōu)化了策略分布，提高 BFS 的采樣效率。

如下圖實驗結果，在各種計算量級下，經(jīng)過 DPO 優(yōu)化的模型均取得了性能提升，證明了負面信號在定理證明中的重要價值。

• 避免對深度推理的打壓，實現(xiàn)對高難度定理證明的突破

為解決 BFS 對深度推理路徑的天然打壓問題，BFS-Prover 系統(tǒng)引入了可調節(jié)的長度歸一化評分函數(shù)：

其中，L 表示路徑長度，α 是可調節(jié)的長度歸一化參數(shù)。通過適當調整 α 值，系統(tǒng)可以平衡對高概率路徑的利用與對深層路徑的探索，使 BFS 能夠更有效地探索長鏈證明。

3. 成果取得 MiniF2F 新 SOTA 

團隊在 MiniF2F 測試集上，對 BFS-Prover 進行了全面評估。該測試集是形式化數(shù)學領域公認的基準測試集，包含高難度的競賽級數(shù)學問題，被廣泛用于衡量自動定理證明系統(tǒng)的能力。

• 超越現(xiàn)有最優(yōu)系統(tǒng)

在與此前定理證明系統(tǒng)的對比中，BFS-Prover 展現(xiàn)出顯著優(yōu)勢。

在固定策略生成的計算量下(2048×2×600 次推理調用)，BFS-Prover 實現(xiàn)了 70.83% 的準確率，超過所有現(xiàn)有系統(tǒng)，包括使用價值函數(shù)的 InternLM2.5-StepProver (65.9%) 、HunyuanProver (68.4%)，以及基于蒙特卡洛樹搜索的 DeepSeek-Prover-V1.5（63.5%）。

在累積評估中，BFS-Prover 進一步將準確率提升至 72.95%，成為了形式化定理證明領域的 SOTA。

這一結果不僅證明了 BFS 方法的潛力，更展示了通過精心設計可以使簡單算法超越復雜方法。

• 成功證明多個 IMO 題目

值得一提的是，BFS-Prover 成功證明了 MiniF2F-test 中的多個 IMO 問題，包括 imo_1959_p1，imo_1960_p2, imo_1962_p2, imo_1964_p2 和  imo_1983_p6。

這些證明展示了該系統(tǒng)在處理復雜數(shù)學推理方面的強大能力，涵蓋數(shù)論、不等式和幾何關系等。

比如，對于 imo_1983_p6 不等式問題，BFS-Prover 能夠生成簡潔而優(yōu)雅的形式化證明：

4. 寫在最后 

團隊認為，BFS-Prover 的成功，暗含了自動定理證明領域的一項重要啟示：簡潔的算法結合精心設計的優(yōu)化策略，同樣有助于 AI4Math 邊界的拓展。

隨著大語言模型能力的不斷提升，BFS-Prover 開創(chuàng)的簡潔高效路線有望進一步推動自動形式化定理證明領域發(fā)展，為數(shù)學研究提供更強大的自動化工具支持。

展望未來，團隊計劃進一步提升 BFS 方法在處理更復雜數(shù)學問題上的能力，特別是針對本科和研究生級別的數(shù)學定理。同時，團隊也將基于推理模型和其他前沿路線，持續(xù)挖掘模型潛力。