AIxiv專(zhuān)欄是機(jī)器之心發(fā)布學(xué)術(shù)、技術(shù)內(nèi)容的欄目。過(guò)去數(shù)年，機(jī)器之心AIxiv專(zhuān)欄接收?qǐng)?bào)道了2000多篇內(nèi)容，覆蓋全球各大高校與企業(yè)的頂級(jí)實(shí)驗(yàn)室，有效促進(jìn)了學(xué)術(shù)交流與傳播。如果您有優(yōu)秀的工作想要分享，歡迎投稿或者聯(lián)系報(bào)道。投稿郵箱：liyazhou@jiqizhixin.com；zhaoyunfeng@jiqizhixin.com
自動(dòng)形式化數(shù)學(xué)定理證明，是人工智能在數(shù)學(xué)推理領(lǐng)域的重要應(yīng)用方向。此類(lèi)任務(wù)需要將數(shù)學(xué)命題和證明步驟轉(zhuǎn)化為計(jì)算機(jī)可驗(yàn)證的代碼，這不僅能確保推理過(guò)程的絕對(duì)嚴(yán)謹(jǐn)性，還能構(gòu)建可復(fù)用的數(shù)學(xué)知識(shí)庫(kù)，為科學(xué)研究提供堅(jiān)實(shí)基礎(chǔ)。
早在上世紀(jì)中葉，戴維斯、明斯基等不少邏輯學(xué)家、數(shù)學(xué)家、人工智能先驅(qū)便已在探索相關(guān)問(wèn)題，其中，也不乏王浩、吳文俊等華人身影。
近些年在 LLM 能力加持下，自動(dòng)定理證明系統(tǒng)更多依賴(lài)于復(fù)雜的蒙特卡洛樹(shù)搜索 (MCTS) 或價(jià)值函數(shù) (Value Function) 來(lái)指導(dǎo)搜索過(guò)程。
然而，這些方法引入了額外計(jì)算成本，并增加系統(tǒng)復(fù)雜度，使模型在大規(guī)模推理任務(wù)中的可擴(kuò)展性受限。
字節(jié)跳動(dòng)豆包大模型團(tuán)隊(duì)推出的 BFS-Prover 挑戰(zhàn)了這一傳統(tǒng)范式。
作為一種更簡(jiǎn)單、更輕量但極具競(jìng)爭(zhēng)力的自動(dòng)定理證明系統(tǒng)，它引入了三項(xiàng)關(guān)鍵技術(shù)：1）專(zhuān)家迭代 (Expert Iteration) 與自適應(yīng)性數(shù)據(jù)過(guò)濾，2）直接偏好優(yōu)化 (DPO) 結(jié)合 Lean4 編譯器反饋，3）BFS 中的長(zhǎng)度歸一化。
從結(jié)果看，BFS-Prover 在形式化數(shù)學(xué)測(cè)試集 MiniF2F 上實(shí)現(xiàn)了 72.95% 的準(zhǔn)確率，創(chuàng)造了新的領(lǐng)域記錄。
該結(jié)果也首次證明：在合理的優(yōu)化策略下，簡(jiǎn)單的 BFS 方法能夠超越蒙特卡洛樹(shù)搜索（MCTS）和價(jià)值函數(shù)（Value Function）等主流的復(fù)雜搜索算法。
目前，論文成果已對(duì)外公開(kāi)，模型也最新開(kāi)源，期待與相關(guān)研究者做更進(jìn)一步交流。
- 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
Part1：主流方法蒙特卡洛樹(shù)搜索和價(jià)值函數(shù)真的必要么？
在形式化數(shù)學(xué)證明領(lǐng)域，將抽象的數(shù)學(xué)概念轉(zhuǎn)化為能夠用計(jì)算機(jī)驗(yàn)證的嚴(yán)格形式，是一項(xiàng)極具挑戰(zhàn)性的任務(wù)。
該過(guò)程要求每一步推理都符合嚴(yán)格的形式邏輯規(guī)則，且每個(gè)步驟都必須經(jīng)過(guò) Lean 證明助手驗(yàn)證。
在自動(dòng)形式化定理證明過(guò)程中，計(jì)算機(jī)面臨的核心挑戰(zhàn)是 —— 在龐大且高度結(jié)構(gòu)化的證明空間中，找出有效路徑。這一難點(diǎn)與傳統(tǒng)搜索問(wèn)題有本質(zhì)區(qū)別，具體表現(xiàn)如下：
- 搜索空間龐大：每一步推理可能有數(shù)十甚至上百種可能的策略選擇；
- 動(dòng)態(tài)變化的策略空間：不同于棋類(lèi)游戲的固定規(guī)則，數(shù)學(xué)定理證明中，每個(gè)狀態(tài)下可應(yīng)用的策略集合不斷變化，且規(guī)模龐大且無(wú)明確界限；
- 反饋稀疏與延遲：直到完成證明前，系統(tǒng)很難獲得有效的中間反饋；
- 開(kāi)放式推理過(guò)程：缺乏明確的終止條件，證明嘗試可能無(wú)限延續(xù)；
現(xiàn)有自動(dòng)定理證明系統(tǒng)如 DeepSeek-Prover-V1.5、InternLM2.5-StepProver 和 HunyuanProver，主要依賴(lài)復(fù)雜的蒙特卡洛樹(shù)搜索（MCTS）和價(jià)值函數(shù)（Value Function）解決上述問(wèn)題。
這些類(lèi) AlphaZero 算法框架在游戲中表現(xiàn)出色，尤其在圍棋領(lǐng)域大放異彩，推動(dòng)了強(qiáng)化學(xué)習(xí)概念破圈。但在自動(dòng)定理證明領(lǐng)域，由于狀態(tài)空間極其復(fù)雜以及缺乏明確的過(guò)程獎(jiǎng)勵(lì)信號(hào)，上述主流方法效果并不理想。此外，復(fù)雜的搜索算法還帶來(lái)了計(jì)算成本高、系統(tǒng)復(fù)雜度增加等問(wèn)題。
Part2：化繁為簡(jiǎn)，用機(jī)器證明數(shù)學(xué)定理可以更簡(jiǎn)單
人類(lèi)遇到問(wèn)題，往往優(yōu)先采用最可能解決的方法。最優(yōu)先樹(shù)搜索（Best-First Tree Search，即 BFS）與之類(lèi)似。
這是一種在 “樹(shù)” 或 “圖” 中搜索節(jié)點(diǎn)的算法。核心思想是根據(jù)某種啟發(fā)式函數(shù)，評(píng)估每個(gè)節(jié)點(diǎn)優(yōu)先級(jí)，按優(yōu)先級(jí)訪問(wèn)節(jié)點(diǎn)，常用于解決約束滿(mǎn)足問(wèn)題和組合優(yōu)化問(wèn)題，特別是在需要快速找到近似最優(yōu)解的情況下。
此前不少研究者認(rèn)為，簡(jiǎn)單的 BFS 算法缺乏有效的探索機(jī)制，尤其是對(duì)深度路徑的探索，難以勝任大規(guī)模定理證明任務(wù)，但豆包大模型團(tuán)隊(duì)的研究者發(fā)現(xiàn)了其中的突破口，并提出了 BFS-Prover 系統(tǒng)。
下圖展示了 BFS-Prover 系統(tǒng)的整體架構(gòu)和工作流程。
右側(cè)展示了訓(xùn)練數(shù)據(jù)生成過(guò)程，包括用于監(jiān)督微調(diào)的 SFT 數(shù)據(jù) (成功證明路徑上的狀態(tài) - 策略對(duì)) 和用于直接偏好優(yōu)化的 DPO 數(shù)據(jù) (從同一狀態(tài)出發(fā)的正確策略與錯(cuò)誤策略的對(duì)比)。
左側(cè)展示了 BFS 機(jī)制，通過(guò) LeanDojo 環(huán)境與 Lean4 交互，從根節(jié)點(diǎn)開(kāi)始，按照優(yōu)先級(jí)順序 (1→2→3...) 探索證明路徑，直到找到證明完成節(jié)點(diǎn) (綠色 A 點(diǎn))。
整個(gè)系統(tǒng)形成閉環(huán)：LLM 生成策略 → LeanDojo 執(zhí)行 → 獲取反饋 → 生成訓(xùn)練數(shù)據(jù)→優(yōu)化 LLM → 再次生成策略，實(shí)現(xiàn)了持續(xù)改進(jìn)的專(zhuān)家迭代機(jī)制。
團(tuán)隊(duì)認(rèn)為，BFS-Prover 系統(tǒng)不僅證明了經(jīng)過(guò)優(yōu)化的 BFS 方法性能方面可以超越復(fù)雜的 MCTS 和價(jià)值函數(shù)，并且能保持架構(gòu)的簡(jiǎn)潔性和計(jì)算效率。其技術(shù)特征如下：
- 讓模型既能深度思考策略，也能掌握最簡(jiǎn)證明方式
BFS-Prover 采用專(zhuān)家迭代框架，通過(guò)多輪迭代不斷增強(qiáng) LLM 能力。在每輪迭代中，系統(tǒng)會(huì)先使用確定性的束搜索 (Beam Search) 方法過(guò)濾掉容易解決的定理，將這些 “簡(jiǎn)單問(wèn)題” 從訓(xùn)練數(shù)據(jù)中剔除，再著手解決 “復(fù)雜問(wèn)題”。
這一數(shù)據(jù)過(guò)濾機(jī)制頗具創(chuàng)新性，確保了訓(xùn)練數(shù)據(jù)逐漸向更具挑戰(zhàn)性的定理證明任務(wù)傾斜，使 LLM 能夠?qū)W習(xí)更多元化的證明策略。
如下圖實(shí)驗(yàn)數(shù)據(jù)顯示，隨迭代進(jìn)行，系統(tǒng)能夠發(fā)現(xiàn)證明的平均長(zhǎng)度變長(zhǎng)，覆蓋面變廣，證明了這一方法的有效性。
與此同時(shí)，LLM 生成的策略分布也發(fā)生進(jìn)化。
如下圖所示，經(jīng)過(guò)多輪迭代，模型生成的策略長(zhǎng)度分布發(fā)生了顯著變化：非常短的策略（1-10 個(gè) token）比例下降，而中等長(zhǎng)度策略（11-50 個(gè) token）比例則有所增加。
這種分布變化表明，LLM “深度思考能力” 在加強(qiáng)，避免了常見(jiàn)的強(qiáng)化學(xué)習(xí)導(dǎo)致的分布坍縮問(wèn)題，并逐漸掌握了更復(fù)雜、更信息豐富的證明策略。
同時(shí)，模型生成簡(jiǎn)潔策略的能力并未摒棄。這種多樣策略生成能力的保持對(duì)于有效定理證明至關(guān)重要，因?yàn)椴煌淖C明狀態(tài)，需要不同復(fù)雜度的策略，涵蓋從簡(jiǎn)單的項(xiàng)重寫(xiě)到復(fù)雜的代數(shù)操作。
- 從過(guò)程中總結(jié) “錯(cuò)誤證明步驟”，提升證明能力
在證明搜索過(guò)程中，當(dāng) LLM 生成的某些策略導(dǎo)致 Lean4 編譯器錯(cuò)誤，系統(tǒng)將這些無(wú)效策略與成功策略配對(duì)，形成負(fù)反饋信號(hào)。
BFS-Prover 創(chuàng)新性地依靠這些數(shù)據(jù)，基于直接偏好優(yōu)化 (DPO) 技術(shù)優(yōu)化策略 LLM。此種方法顯著提高了模型識(shí)別有效策略的能力，優(yōu)化了策略分布，提高 BFS 的采樣效率。
如下圖實(shí)驗(yàn)結(jié)果，在各種計(jì)算量級(jí)下，經(jīng)過(guò) DPO 優(yōu)化的模型均取得了性能提升，證明了負(fù)面信號(hào)在定理證明中的重要價(jià)值。
- 避免對(duì)深度推理的打壓，實(shí)現(xiàn)對(duì)高難度定理證明的突破
為解決 BFS 對(duì)深度推理路徑的天然打壓?jiǎn)栴}，BFS-Prover 系統(tǒng)引入了可調(diào)節(jié)的長(zhǎng)度歸一化評(píng)分函數(shù)：
其中，L 表示路徑長(zhǎng)度，α 是可調(diào)節(jié)的長(zhǎng)度歸一化參數(shù)。通過(guò)適當(dāng)調(diào)整 α 值，系統(tǒng)可以平衡對(duì)高概率路徑的利用與對(duì)深層路徑的探索，使 BFS 能夠更有效地探索長(zhǎng)鏈證明。
Part3：BFS-Prover 取得 MiniF2F 新 SOTA
團(tuán)隊(duì)在 MiniF2F 測(cè)試集上，對(duì) BFS-Prover 進(jìn)行了全面評(píng)估。該測(cè)試集是形式化數(shù)學(xué)領(lǐng)域公認(rèn)的基準(zhǔn)測(cè)試集，包含高難度的競(jìng)賽級(jí)數(shù)學(xué)問(wèn)題，被廣泛用于衡量自動(dòng)定理證明系統(tǒng)的能力。
- 超越現(xiàn)有最優(yōu)系統(tǒng)
在與領(lǐng)先的定理證明系統(tǒng)的對(duì)比中，BFS-Prover 展現(xiàn)出顯著優(yōu)勢(shì)。
在固定策略生成的計(jì)算量下 (2048×2×600 次推理調(diào)用)，BFS-Prover 實(shí)現(xiàn)了 70.83% 的準(zhǔn)確率，超過(guò)所有現(xiàn)有系統(tǒng)，包括使用價(jià)值函數(shù)的 InternLM2.5-StepProver (65.9%) 、HunyuanProver (68.4%)，以及基于 MCTS 的 DeepSeek-Prover-V1.5 (63.5%)。
在累積評(píng)估中，BFS-Prover 進(jìn)一步將準(zhǔn)確率提升至 72.95%，成為了形式化定理證明領(lǐng)域的 SOTA。
這一結(jié)果不僅證明了 BFS 方法的潛力，更展示了通過(guò)精心設(shè)計(jì)可以使簡(jiǎn)單算法超越復(fù)雜方法。
- 成功證明多個(gè) IMO 題目
值得一提的是，BFS-Prover 成功證明了 MiniF2F-test 中的多個(gè) IMO 問(wèn)題，包括 imo_1959_p1，imo_1960_p2, imo_1962_p2, imo_1964_p2 和 imo_1983_p6。
這些證明展示了系統(tǒng)在處理復(fù)雜數(shù)學(xué)推理方面的強(qiáng)大能力，涵蓋數(shù)論、不等式和幾何關(guān)系等。
比如，對(duì)于 imo_1983_p6 不等式問(wèn)題，BFS-Prover 能夠生成簡(jiǎn)潔而優(yōu)雅的形式化證明：
團(tuán)隊(duì)認(rèn)為，BFS-Prover 的成功，暗含了自動(dòng)定理證明領(lǐng)域的一項(xiàng)重要啟示：簡(jiǎn)潔的算法結(jié)合精心設(shè)計(jì)的優(yōu)化策略，同樣有助于 AI4Math 邊界拓展。
隨著大語(yǔ)言模型能力的不斷提升，BFS-Prover 開(kāi)創(chuàng)的簡(jiǎn)潔高效路線(xiàn)有望進(jìn)一步推動(dòng)自動(dòng)形式化定理證明領(lǐng)域發(fā)展，為數(shù)學(xué)研究提供更強(qiáng)大的自動(dòng)化工具支持。
展望未來(lái)，團(tuán)隊(duì)計(jì)劃進(jìn)一步提升 BFS 方法在處理更復(fù)雜數(shù)學(xué)問(wèn)題上的能力，特別是針對(duì)本科和研究生級(jí)別的數(shù)學(xué)定理。同時(shí)，團(tuán)隊(duì)也將基于推理模型和其他前沿路線(xiàn)，持續(xù)挖掘模型潛力。
團(tuán)隊(duì)期望，通過(guò)持續(xù)優(yōu)化數(shù)據(jù)和訓(xùn)練策略，讓相關(guān)工具為數(shù)學(xué)研究提供強(qiáng)大輔助，加速數(shù)學(xué)發(fā)現(xiàn)過(guò)程，最終實(shí)現(xiàn)人機(jī)協(xié)作解決前沿?cái)?shù)學(xué)挑戰(zhàn)的愿景。
熱門(mén)跟貼