mlsanityData to 7 Oct 2026

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

arXiv 2502.03438 ↗First posted 5 Feb 2025cs.AIcited by 82

Not on the map. Why?

Cited by 29 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

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.

Key facts. Cited by 82 papers in the map (data through 7 Oct 2026). Builds on 23 of its 35 references that are in the map. First posted on arXiv 5 Feb 2025.

Builds on

23 of 35 references.

References · 23

  1. 2023GPT-4 Technical Reportcited by 18,132
  2. 2023Direct Preference Optimization: Your Language Model is Secretly a Reward Modelcited by 7,916
  3. 2023Efficient Memory Management for Large Language Model Serving with PagedAttentioncited by 5,767
  4. 2016OpenAI Gymcited by 1,684
  5. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  6. 2024Qwen2.5-Math Technical Report: Toward Mathematical Expert Model via Self-Improvementcited by 1,057
  7. 2017Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithmcited by 723
  8. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  9. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  10. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  11. 2022Autoformalization with Large Language Modelscited by 252
  12. 2017Thinking Fast and Slow with Deep Learning and Tree Searchcited by 245
11 more
  1. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  2. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  3. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  4. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  5. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  6. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  7. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  8. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  9. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
  10. 2024HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Provingcited by 32
  11. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2025: 45; 2026: 37.

82 papers.

Sort:

By area:

  1. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  2. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 173
  3. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
  4. 2025Seed-Prover: Deep and Broad Reasoning for Automated Theorem Provingcited by 96
  5. 2025Rewarding the Unlikely: Lifting GRPO Beyond Distribution Sharpeningcited by 78
  6. 2025Tree Search for LLM Agent Reinforcement Learningcited by 73
  7. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
  8. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  9. 2025FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Modelscited by 45
  10. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36
  11. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  12. 2025CombiBench: Benchmarking LLM Capability for Combinatorial Mathematicscited by 28
38 more
  1. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  2. 2025Leanabell-Prover: Posttraining Scaling in Formal Reasoningcited by 27
  3. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Proverscited by 26
  4. 2025ATLAS: Autoformalizing Theorems through Lifting, Augmentation, and Synthesis of Datacited by 23
  5. 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 23
  6. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  7. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19
  8. 2025REAL-Prover: Retrieval Augmented Lean Prover for Mathematical Reasoningcited by 18
  9. 2025Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Modelscited by 17
  10. 2025Generative AI Act II: Test Time Scaling Drives Cognition Engineeringcited by 14
  11. 2025Mathesis: Towards Formal Theorem Proving from Natural Languagescited by 14
  12. 2025miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forwardcited by 13
  13. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  14. 2025StepFun-Prover Preview: Let's Think and Verify Step by Stepcited by 12
  15. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 11
  16. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 11
  17. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curationcited by 10
  18. 2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verificationcited by 10
  19. 2025FormaRL: Enhancing Autoformalization with no Labeled Datacited by 9
  20. 2025Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalitiescited by 8
  21. 2025Towards Advanced Mathematical Reasoning for LLMs via First-Order Logic Theorem Provingcited by 8
  22. 2025Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Provingcited by 7
  23. 2025LeanGeo: Formalizing Competitional Geometry problems in Leancited by 7
  24. 2025EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficultycited by 7
  25. 2025HybridProver: Augmenting Theorem Proving with LLM-Driven Proof Synthesis and Refinementcited by 6
  26. 2026OProver: A Unified Framework for Agentic Formal Theorem Provingcited by 6
  27. 2025FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theorycited by 5
  28. 2025GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Provingcited by 5
  29. 2025Lean4Physics: Comprehensive Reasoning Framework for College-level Physics in Lean4cited by 5
  30. 2026DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agentcited by 4
  31. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidancecited by 3
  32. 2025Translating Informal Proofs into Formal Proofs Using a Chain of Statescited by 3
  33. 2026ConvexBench: Can LLMs Recognize Convex Functions?cited by 3
  34. 2026AI Planning Framework for LLM-Based Web Agentscited by 3
  35. 2026APPO: Agentic Procedural Policy Optimizationcited by 3
  36. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisationcited by 3
  37. 2025MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classificationcited by 2
  38. 2025Hierarchical Attention Generates Better Proofscited by 1

50 most cited of 82 All 82 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2025A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
  2. 2026TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science
  3. 2026TreeThink: A Modular Tree Search Library for Mathematical Reasoning with LLMs
  4. 2026On Reasoning-Centric LLM-based Automated Theorem Proving
  5. 2026Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs
  6. 2025LogicTree: Structured Proof Exploration for Coherent and Rigorous Logical Reasoning with Large Language Models
  7. 2025Scaling Natural-Language Graph-Based Test Time Compute for Automated Theorem Proving
  8. 2024ImProver: Agent-Based Automated Proof Optimization