Research map / Multi-agent systems and games / LLM agents
Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Introduces BFS-Prover-V2, a Lean4 step-level prover trained with multi-stage expert iteration (adaptive perplexity-based tactic filtering and periodic soft-reset retraining) and inference via a Gemini-2.5-Pro planner with parallel prover agents sharing a subgoal cache, reporting 95.08% on miniF2F-test and 41.4% on ProofNet-test.
Problem
Scaling both training-time RL (avoiding performance plateaus) and inference-time search for step-level LLM theorem provers in Lean4.
Approach
Tactic-level perplexity filtering that keeps only the central part of the perplexity distribution as an automatic curriculum, periodic full retraining from a base checkpoint as a "soft reset" to escape plateaus, and a Planner LLM that decomposes theorems into subgoals solved by parallel BFS prover agents sharing a subgoal cache with dynamic replanning.
Key results
- BFS-Prover-V2 achieves 95.08% on miniF2F test (95.49% validation) with the planner-enhanced system.
- BFS-Prover-V2-32B reaches 41.4% on ProofNet-test, reported as a new state of the art.
- Without the planner, BFS-Prover-V2-7B reaches 82.4% and 32B reaches 86.1% on miniF2F-test.
Limitations
- Step-level proofs have poor readability compared with whole-proof outputs.
- Planner relies on a proprietary general-purpose model (Gemini-2.5-Pro).
- Training corpus is mainly high-school competition problems.
Experimental setup
Datasets: NuminaMath-CoT NuminaMath-1.5 Goedel-Prover data miniF2F ProofNet
Benchmarks: miniF2F-test miniF2F-valid ProofNet-test
Metrics: pass rate
Baselines: InternLM2.5-StepProver-7B Hunyuan-Prover-7B BFS-Prover-V1-7B MPS-Prover-7B DeepSeek-Prover-V2-671B Kimina-Prover-72B Goedel-Prover-32B Delta-Prover Seed-Prover
Builds on: BFS-Prover-V1 AlphaZero LeanDojo Qwen2.5-Math
Closest papers by meaning
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.91)
- T1: Advancing Language Model Reasoning through Reinforcement Learning and Inference Scaling (ICML 2025 · similarity 0.89)
- Subgoal-based Demonstration Learning for Formal Theorem Proving (ICML 2024 · similarity 0.89)
- Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models (NeurIPS 2025 · similarity 0.89)
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search (ICLR 2025 · similarity 0.89)
- APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning (NeurIPS 2025 · similarity 0.89)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.