Source-linked AI summary
BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, Kai Shen
TL;DR
LLM theorem proving in Lean4 requires effective search through large, constrained proof spaces, while the suitability of simple BFS remains underexplored. BFS-Prover scales BFS with filtered expert iteration, compiler-feedback DPO, and length normalization, achieving a 72.95% state-of-the-art MiniF2F test score. The authors report that this challenges the perceived necessity of MCTS and value functions, though the current 7B model limits reasoning capacity and larger models raise computational costs.
Problem
The paper asks whether Best-First Tree Search can achieve competitive large-scale Lean4 theorem-proving performance despite limited exploration and bias against deep proofs.
Method
BFS-Prover combines expert-iteration filtering, DPO from Lean compiler-error preferences, and length-normalized BFS scoring to refine tactic generation and explore deeper proofs.
Results
72.95% on the MiniF2F test set is reported as BFS-Prover’s state-of-the-art score.
Takeaways & Limitations
The results challenge the perceived necessity of MCTS and value functions for scalable LLM-based formal theorem proving.
Takeaways & Limitations
The current implementation uses a 7B policy model, which may limit sophisticated mathematical reasoning, while larger models increase training and inference costs.
Abstract
from arXiv · showhide
Recent advancements in large language models (LLMs) have spurred growing interest in automatic theorem proving using Lean4, where effective tree search methods are crucial for navigating the underlying large proof search spaces. While the existing approaches primarily rely on value functions and/or Monte Carlo Tree Search (MCTS), the potential of simpler methods like Best-First Tree Search (BFS) remains underexplored. In this paper, we investigate whether BFS can achieve competitive performance in large-scale theorem proving tasks. We present BFS-Prover, a scalable expert iteration framework, featuring three key innovations. First, we implement strategic data filtering at each expert iteration round, excluding problems solvable via beam search node expansion to focus on harder cases. Second, we improve the sample efficiency of BFS through Direct Preference Optimization (DPO) applied to state-tactic pairs automatically annotated with compiler error feedback, refining the LLM's policy to prioritize productive expansions. Third, we employ length normalization in BFS to encourage exploration of deeper proof paths. BFS-Prover achieves a state-of-the-art score of $72.95\%$ on the MiniF2F test set and therefore challenges the perceived necessity of complex tree search methods, demonstrating that BFS can achieve competitive performance when properly scaled. To facilitate further research and development in this area, we have open-sourced our model at https://huggingface.co/ByteDance-Seed/BFS-Prover-V1-7B.
1 Introduction
BFS-Prover investigates whether lightweight Best-First Tree Search can scale to large formal theorem-proving tasks despite concerns about exploration and deep-proof bias. It combines targeted scaling strategies with expert iteration to achieve competitive MiniF2F performance.
- Motivation: Formal theorem proving requires syntactically and semantically valid steps within a highly constrained framework and offers a vast tactic space.These properties make navigating proof spaces especially challenging for LLM-based systems.
- Motivation: BFS prioritizes accumulated log probabilities, providing a simpler alternative to MCTS but potentially overlooking lower-probability valid solutions.Its lightweight design lacks mechanisms such as upper confidence bounds or value functions for balancing exploration and exploitation.
- Motivation: BFS also penalizes longer proof paths because cumulative log probabilities tend to decrease with depth.This can hinder theorems whose solutions require seemingly unpromising intermediate states.
- Contributions: BFS-Prover filters beam-search-solvable problems during expert iteration, directing accumulated training data toward harder theorems.The policy LLM can thereby learn diverse tactics and deeper proofs through successive rounds.
- Contributions: BFS-Prover combines compiler-feedback DPO with length normalization to avoid unproductive tactics and explore deeper proof paths.DPO compares proof-path tactics with error-causing tactics, while normalization mitigates BFS’s depth bias.
- Contributions: 72.95% on MiniF2F test is reported as an accumulative state-of-the-art score while retaining a lightweight design without MCTS and value functions.The paper presents this result as evidence that BFS can scale to competitive theorem-proving performance.
2 The BFS-Prover system
BFS-Prover integrates Lean4 through LeanDojo, uses a length-normalized priority queue for proof search, and improves its policy through expert iteration. The pipeline combines successful proof data, compiler-error preferences, and filtering of simpler problems.
- Lean4 Environment and Policy LLM: LeanDojo provides the Python interface between the policy LLM and Lean4, executing generated tactics and returning compiler errors.These errors supply feedback used to refine the policy through DPO.
- Length-Normalized Best-First Tree Search: BFS-Prover maintains a priority queue of proof states ordered by a length-normalized scoring heuristic.This mechanism guides node expansion through the state-tactic proof space.
- Length-Normalized Best-First Tree Search: The score uses proof-path tactic probabilities and path length to control exploration depth.Increasing α or reducing expansion width favors deeper paths and long tactic chains.
- Length-Normalized Best-First Tree Search: At each expansion, Lean4 classifies sampled tactics as valid-state nodes, proof-finish nodes, or terminal error nodes.Valid intermediate states enter the queue, successful proofs are returned, and invalid paths terminate.
- Expert Iteration: Each expert-iteration round filters beam-search-solvable statements before collecting BFS proof data from the remaining corpus.Successful state-tactic pairs are accumulated, while invalid tactics producing compiler errors are recorded as negative data.
- Expert Iteration: SFT trains on accumulated proof-path pairs, while DPO compares valid proof tactics with error-causing alternatives from the same proof states.The resulting preference refinement uses on-policy Lean error data to sharpen tactic selection and improve BFS sample efficiency.
3 Practical Implementation and Benchmark Results
BFS-Prover combines expert iteration, selective data collection, DPO refinement, length normalization, and distributed infrastructure for scalable Lean4 theorem proving. On MiniF2F, it achieves strong performance while showing deeper proofs, diverse tactics, logarithmic search scaling, and benefits from compiler-error feedback.
- Implementation: BFS-Prover uses approximately 900,000 formal statements, expanded training sources, and filtering to focus expert iteration on harder theorems.The corpus combines autoformalized NuminaMath-CoT statements with unproven Mathlib theorems and Lean-Workbook statements; beam search filtering identifies easily solvable theorems.
- Implementation: The system trains a policy LLM through SFT or DPO, using Lean4 compiler errors as negative signals for preference refinement.DPO uses one-round refinement over state-tactic data, while the training procedures specify separate SFT and DPO schedules.
- Implementation: Distributed Ray infrastructure achieves nearlinear scaling across machines by evenly distributing target theorems and avoiding cross-machine communication overhead.Each machine runs independent proving pipelines, with eight policy-LLM instances on dedicated A100 GPUs.
- Benchmark Results: Expert iteration shifts proof distributions toward longer proofs and tactic distributions toward moderate-length tactics while preserving tactic diversity.The reported shifts indicate increasing proof depth and more sophisticated tactics without collapsing the range of tactic lengths.
- Benchmark Results: 72.95% is BFS-Prover’s accumulative MiniF2F test score after searches using length-normalization factors α ∈ {0.0, 0.5, 1.0}.Under a fixed budget, BFS-Prover uses temperature 1.1, expansion width 2, and α = 0.5, achieving state-of-the-art performance without a critic model or MCTS.
- Benchmark Results: SFT improves from 64.58% to 70.38% and SFT+DPO from 64.98% to 70.83% as passes increase from 64 to 2048.Both methods show logarithmic scaling with consistent but diminishing returns, while SFT+DPO consistently outperforms SFT and has comparable variance.
4 Conclusion and Discussion
BFS-Prover shows that Best-First Search can scale efficiently to state-of-the-art automatic theorem proving performance while retaining a lightweight design. On MiniF2F, the system achieves 72.95% and motivates attention to simpler search methods and scaling limits.
- BFS-Prover achieves state-of-the-art automatic theorem proving performance while maintaining computational simplicity.The system challenges the perceived necessity of MCTS and value functions for large-scale formal theorem proving with LLMs.
- 72.95% is BFS-Prover’s state-of-the-art score on the MiniF2F benchmark.
- BFS-Prover combines expert iteration, strategic data filtering, DPO, and length normalization to scale Best-First Search.These strategies direct training toward harder theorems, refine tactic selection, and support deeper proof paths.
- The observed logarithmic scaling law suggests that additional computation improves BFS performance but may face fundamental limits from search alone.The paper identifies better-than-logarithmic scaling as a direction for future research.
Limitations
BFS-Prover’s main limitation concerns its relatively small 7B policy model. Larger models may represent more sophisticated reasoning, but their computational demands could reduce search coverage, while long proof states may exceed the 7B model’s practical context window.
- BFS-Prover relies on a relatively small 7B policy model, which may limit sophisticated mathematical reasoning.
- DPO refinement is reported to improve sample efficiency and overall accuracy relative to SFT alone.
- Larger models could capture more complex mathematical insights but would increase training and inference costs in tree search.Greater GPU-memory requirements and inference latency could reduce the number of states explored within a fixed time budget.
- Extensive proof-state descriptions may exceed a 7B model’s practical context window, causing crucial information to be missed when generating tactics.
Appendix: Lean Proofs for IMO Problems Found by BFS-Prover
The appendix presents Lean 4 proofs found by BFS-Prover for several MiniF2F IMO problems. These examples span number theory, inequalities, and geometric relationships, illustrating the system’s coverage of complex formal reasoning tasks.
- The examples cover complex formal reasoning in number theory, inequalities, and geometric relationships.
- Figure 5 shows a Lean 4 proof of IMO-1959-P1 found by BFS-Prover.
- Figure 6 shows BFS-Prover’s Lean 4 proof of IMO-1964-P2.
- Figure 7 shows a Lean 4 proof of IMO-1960-P2 found by BFS-Prover.
- The appendix includes the theorem statement for IMO-1962-P2 over the real numbers with square-root and interval constraints.