BFS-Prover – 字節豆包推出的自動定理證明系統

BFS-Prover是什麼

BFS-Prover 是字節跳動豆包大模型團隊推出的基於大語言模型（LLM）的自動定理證明系統，通過改進傳統的廣度優先搜索（BFS）算法，結合專家迭代、直接偏好優化等技術，實現了高效的證明搜索。核心在於長度歸一化的評分啓發式方法，通過累積對數概率評估證明路徑的優先級，優化搜索效率。採用專家迭代框架，專注於解決複雜定理，基於直接偏好優化（DPO）從編譯器反饋中優化策略模型，避免無效推理路徑。BFS-Prover 通過分佈式架構實現大規模並行證明搜索，支持高併發任務。

BFS-Prover的主要功能

• 高效的證明搜索：BFS-Prover 採用改進的廣度優先搜索（BFS）算法，通過長度歸一化的評分機制，優化了對深度推理路徑的探索能力。能動態分配計算資源，平衡搜索過程中的探索與利用。
• 持續改進與數據積累：系統形成閉環：LLM 生成策略 → LeanDojo 執行 → 獲取反饋 → 生成訓練數據 → 優化 LLM。隨着迭代的進行，模型能學習更多元化的證明策略。

BFS-Prover的技術原理

• 長度歸一化的評分機制：BFS-Prover 採用了長度歸一化的評分函數，通過將路徑的累積對數概率除以路徑長度的α次方（α∈[0,1]），緩解了傳統 BFS 對深度路徑的懲罰，能更有效地探索複雜證明。
• 專家迭代與自過濾：系統通過專家迭代框架，逐輪篩選出更復雜的定理進行證明。在每輪迭代中，使用束搜索（Beam Search）過濾掉容易解決的定理，將這些簡單問題從訓練數據中剔除，專注於解決更具挑戰性的定理。隨着迭代的進行，模型逐漸學習到更復雜的證明策略，證明長度分佈也從較短的策略向更長的策略轉移。
• 直接偏好優化（DPO）：BFS-Prover 基於 DPO 從編譯器反饋中優化策略模型。通過對比同一狀態下成功和失敗的策略，模型能避免無效的推理路徑，提高搜索效率。
• 分佈式證明架構：爲了實現大規模並行證明，BFS-Prover 採用分佈式系統設計，使用 Ray 框架在多台機器上運行，每台機器配備多個 GPU 和 CPU 核心。實現了近線性的擴展效率，最大化硬件利用率。
• 與 Lean4 的深度集成：BFS-Prover 通過 LeanDojo 與 Lean4 交互，將數學問題編碼爲形式化系統，生成可驗證的機器證明。確保證明的邏輯正確性。

BFS-Prover的項目地址

• HuggingFace模型庫：https://huggingface.co/bytedance-research/BFS-Prover
• arXiv技術論文：https://arxiv.org/pdf/2502.03438

BFS-Prover的應用場景

• 形式化數學問題的自動證明：BFS-Prover 可以將數學問題編碼爲形式化語言（如 Lean4），生成可驗證的機器證明，適用於各種數學領域的定理證明。
• 數學競賽題目的解決：能證明覆雜的國際數學奧林匹克競賽（IMO）題目，展示在複雜數學推理中的強大能力。
• 本科和研究生級別的數學研究：BFS-Prover 幫助解決本科和研究生階段的數學定理證明問題。
• 推動自動定理證明技術的發展：BFS-Prover 在 MiniF2F 測試集上刷新了準確率記錄，爲自動定理證明領域提供了新的方法和技術思路。