What is BFS-Prover
BFS-Prover is an automatic theorem proving system based on large language models (LLM) launched by the ByteDanceDoubaolarge model team. By improving the traditional breadth-first search (BFS) algorithm and combining expert iteration, direct preference optimization, and other techniques, it achieves efficient proof search. Its core lies in a length-normalized scoring heuristic, which evaluates the priority of proof paths through cumulative log probabilities to optimize search efficiency. It adopts an expert iteration framework, focuses on solving complex theorems, and optimizes the policy model from compiler feedback based on direct preference optimization (DPO), avoiding invalid reasoning paths. BFS-Prover achieves large-scale parallel proof search through a distributed architecture and supports high-concurrency tasks.
Main Features of BFS-Prover
- Efficient Proof Search: BFS-Prover adopts an improved breadth-first search (BFS) algorithm and, through a length-normalized scoring mechanism, optimizes its ability to explore deep reasoning paths. It can dynamically allocate computational resources and balance exploration and exploitation during the search process.
- Continuous Improvement and Data Accumulation: The system forms a closed loop: LLM generates strategies → LeanDojo executes → obtain feedback → generate training data → optimize LLM. As iterations proceed, the model can learn more diverse proof strategies.
Technical Principles of BFS-Prover
- Length-Normalized Scoring Mechanism: BFS-Prover adopts a length-normalized scoring function. By dividing the cumulative log probability of a path by the path length raised to the power of α (α∈[0,1]), it alleviates the traditional BFS penalty on deep paths and can more effectively explore complex proofs.
- Expert Iteration and Self-Filtering: Through an expert iteration framework, the system selects more complex theorems round by round for proof. In each round of iteration, beam search is used to filter out theorems that are easy to solve, removing these simple problems from the training data and focusing on solving more challenging theorems. As iterations proceed, the model gradually learns more complex proof strategies, and the proof length distribution also shifts from shorter strategies to longer strategies.
- Direct Preference Optimization (DPO): BFS-Prover optimizes the policy model from compiler feedback based on DPO. By comparing successful and failed strategies under the same state, the model can avoid invalid reasoning paths and improve search efficiency.
- Distributed Proof Architecture: To achieve large-scale parallel proof, BFS-Prover adopts a distributed system design, using the Ray framework to run on multiple machines, with each machine equipped with multiple GPUs and CPU cores. It achieves near-linear scaling efficiency and maximizes hardware utilization.
- Deep Integration with Lean4: BFS-Prover interacts with Lean4 through LeanDojo, encoding mathematical problems into a formal system and generating verifiable machine proofs. It ensures the logical correctness of proofs.
Project Address of BFS-Prover
- HuggingFace Model Repository：https://huggingface.co/bytedance-research/BFS-Prover
- arXiv Technical Paper：https://arxiv.org/pdf/2502.03438
Application Scenarios of BFS-Prover
- Automatic Proof of Formal Mathematical Problems: BFS-Prover can encode mathematical problems into a formal language (such as Lean4) and generate verifiable machine proofs, making it suitable for theorem proving in various fields of mathematics.
- Solving Mathematical Competition Problems: It can prove complex International Mathematical Olympiad (IMO) problems, demonstrating strong capabilities in complex mathematical reasoning.
- Undergraduate and graduate-level mathematical research: BFS-Prover helps solve mathematical theorem proving problems at the undergraduate and graduate levels.
- Advancing the development of automated theorem proving technology: BFS-Prover set a new accuracy record on the MiniF2F test set, providing new methods and technical ideas for the field of automated theorem proving.