Papers with BFS-Prover
BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving (2025.acl-long)
Copied to clipboard
| Challenge: | Existing approaches to theorem proving in large language models rely on value functions and/or Monte Carlo Tree Search (MCTS), but the potential of simpler methods like Best-First Tree Search remains underexplored. |
| Approach: | They propose a scalable expert iteration framework that implements strategic data filtering at each expert iteration round, excluding problems solvable via beam search node expansion to focus on harder cases. |
| Outcome: | The proposed framework achieves a state-of-the-art score of 72.95 on the MiniF2F test set and challenges the perceived necessity of complex tree search methods. |