Elamur Research⌕
☰
home / papers / 2025 / BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving

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

Paper · 2025 · Ran Xin, Chenguang Xi, Jie Yang et al.

Summary

Proof search in Lean4 involves a huge space of possible tactics, so automated provers have mostly relied on MCTS and learned value (critic) models. This paper asks whether plain Best-First Tree Search (BFS) can compete if it is scaled properly. The authors build BFS-Prover, an expert-iteration system that uses LeanDojo to connect a 7B policy LLM to the Lean4 compiler.

The system makes three changes to standard BFS:

  • Filtering easy statements: In each round, statements already provable with beam-search expansions are dropped, so new training data comes from harder problems.
  • Learning from compiler errors: Tactics that make the compiler fail become negative examples for DPO, paired with tactics that lie on successful proof paths.
  • Length-normalized scoring: Path scores are adjusted for length, so the search no longer penalizes long proofs.

Without any critic or MCTS, BFS-Prover reaches a cumulative 72.95% on the MiniF2F test set, ahead of earlier step-level and whole-proof systems. The result suggests that simpler search methods deserve renewed attention in formal reasoning.

Key points

  • Results on MiniF2F-test: BFS-Prover scores 72.95% cumulatively and 70.83% ± 0.89% with a 2048 × 2 × 600 tactic budget. Reported scores for other systems are 63.5% for DeepSeek-Prover-V1.5, 65.9% for InternLM2.5-StepProver and 68.4% for HunyuanProver.
  • Scoring rule: A node's priority is the sum of tactic log-probabilities divided by Lᵅ, where L is the path length. Raising α or narrowing the expansion width pushes the search toward deeper paths.
  • Search settings used: sampling temperature 1.1, expansion width 2, and α = 0.5.
  • Scaling behaviour: As search passes grow from 64 to 2048, accuracy rises roughly logarithmically, from 64.58% to 70.38% with SFT alone and from 64.98% to 70.83% with SFT+DPO. DPO gives a consistent advantage at similar variance.
  • Stated limitations: The 7B policy may limit how complex the learned reasoning can be, and long proof states may not fit in its context window. Larger models would reduce how many states can be explored in a fixed time.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Stanford UniversityStanford · United States567 works · 335,190 citations🏢ByteDanceBeijing · China54 works · 4,494 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng and Ming Ding. 2025. BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving. Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2025.acl-long.1565 · arXiv 2502.03438

@inproceedings{xin2025bfs,
  title = {{BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving}},
  author = {Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng and Ming Ding},
  booktitle = {Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)},
  year = {2025},
  doi = {10.18653/v1/2025.acl-long.1565},
  eprint = {2502.03438},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.18653/v1/2025.acl-long.1565}
}

References

32 references, 23 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Thomas Anthony, Zheng Tian, and David Barber. 2017. Thinking fast and slow with deep learning and tree search. Advances in neural information processing systems, 30.
  2. G Brockman. 2016. Openai gym. arXiv preprint arXiv:1606.01540. find
  3. Cameron B Browne, Edward Powley, Daniel Whitehouse, Simon M Lucas, Peter I Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez, Spyridon Samothrakis, and Simon Colton. 2012. A survey of monte carlo tree search methods. IEEE Transactions on Computational Intelligence and AI in Games, 4(1):1–43… find
  4. Rémi Coulom. 2006. Efficient selectivity and backup operators in monte-carlo tree search. In International conference on computers and games, pages 72–83. Springer. find
  5. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. 2021. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203.
  6. Yuhang He, Jihai Zhang, Jianzhu Bao, Fangquan Lin, Cheng Yang, Bing Qin, Ruifeng Xu, and Wotao Yin. 2024. Bc-prover: Backward chaining prover for formal theorem proving. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, pages 3059–3077. find
  7. Guillaume Lample, Timothée Lacroix, and 1 others. 2022. Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems, 35:26337–26349.
  8. Aitor Lewkowycz and 1 others. 2022. Solving quantitative reasoning problems with language models. arXiv preprint arXiv:2206.14858.
  9. Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, and 1 others. 2024a. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face repository, 13. find
  10. Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. 2024b. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. preprint arXiv:2412.20735. arXiv Haohan Lin, Zhiqing Sun, Sean Welleck, and Yiming Yang. 2024. Lean-star: Le…
  11. Leonardo de Moura and Sebastian Ullrich. 2021. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction (CADE), pages 625–635. Springer.
  12. OpenAI. 2023. Gpt-4 technical report. arXiv preprint arXiv:2303.08774.
  13. Judea Pearl. 1984. Heuristics: intelligent search strategies for computer problem solving. Addison-Wesley Longman Publishing Co., Inc. find
  14. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, and 1 others. 2022. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344.
  15. Stanislas Polu and Ilya Sutskever. 2020. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393.
  16. Rafael Rafailov, Archit Sharma, Eric Mitchell, Christopher D Manning, Stefano Ermon, and Chelsea Finn. 2024. Direct preference optimization: Your language model is secretly a reward model. Advances in Neural Information Processing Systems, 36.
  17. David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, and 1 others. 2016. Mastering the game of go with deep neural networks and tree search. Nature, 529(7587):484–489. find
  18. David Silver, Thomas Hubert, and 1 others. 2017. Mastering chess and shogi by self-play with a general reinforcement learning algorithm. In Advances in Neural Information Processing Systems, volume 30.
  19. Volker Steinbiss, Bach-Hiep Tran, and Hermann Ney. 1994. Improvements in beam search. In ICSLP, volume 94, pages 2143–2146. find
  20. Richard S Sutton. 2018. Reinforcement learning: An introduction. A Bradford Book. find
  21. Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, and 1 others. 2023. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656.
  22. Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. 2024. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203.
  23. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353–32368.
  24. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. 2024a. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700.
  25. Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. 2024b. Lean-github: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.17227.
  26. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. 2024a. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333.
  27. Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, and 1 others. 2024b. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152.
  28. An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, and 1 others. 2024a. Qwen2. 5-math technical report: Toward mathematical expert model via self-improvement. arXiv preprint arXiv:2409.12122. — Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvement
  29. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. 2024b. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075.
  30. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. 2024c. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36.
  31. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. 2024. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847.
  32. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2021. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/xin-2025-bfs-prover-scalable-best-first/