Elamur Research⌕
☰
home / papers / 2025 / Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers

Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers

Paper · 2025 · Ran Xin, Zeyu Zheng, Yanchen Nie et al.

Summary

The paper tackles two linked bottlenecks in LLM-based theorem proving for Lean4. In training, reinforcement learning tends to stall after early gains. At inference, the space of possible tactics grows explosively. The authors present BFS-Prover-V2, an open-source step-level prover that treats proving as a Markov Decision Process: the model proposes one tactic at a time, and the Lean compiler checks it.

Training uses a multi-stage expert iteration loop in the spirit of AlphaZero, run over roughly 3 million autoformalized problems. Two mechanisms keep it improving:

  • Perplexity-based filtering at the tactic level, which keeps examples of suitable difficulty.
  • Periodic retraining from a base checkpoint on re-synthesized, curated data whenever progress stalls.

At inference, a general reasoning model acts as a Planner. It splits a theorem into a chain of subgoals, which parallel prover agents then attack while sharing a subgoal cache.

The system scores 95.08% on miniF2F-test and 41.4% on ProofNet-test, the best results reported for step-level provers. The authors argue the training and search methods could carry over to other long-horizon reasoning tasks.

Key points

  • Base models and training data: the provers are built on Qwen2.5-Math-7B and Qwen2.5-32B, starting from the BFS-Prover-V1 checkpoint. The ~3M formal statements come from autoformalizing NuminaMath-CoT and NuminaMath-1.5, plus data from Goedel-Prover. Each expert-iteration round runs about 10^7 best-first tree searches.
  • Environment and search settings: experiments use Lean v4.10.0 with LeanDojo. Best-first search runs at temperature 1.3, expansion width 3, and length normalization 2.0.
  • Planner: Gemini2.5-Pro serves as the Planner. Once any agent proves the current subgoal, the cache records it and stops the other agents' redundant searches.
  • Results without the Planner: BFS-Prover-V2-7B reaches 82.4% on miniF2F-test. BFS-Prover-V2-32B reaches 86.1% on miniF2F-test, 85.5% on miniF2F-valid, and 41.4% on ProofNet-test, above DeepSeek-Prover-V2-671B's 37.1% on ProofNet.
  • Results with the Planner: the 32B system reaches 95.1% on miniF2F-test and 95.5% on miniF2F-valid. This is on par with the strongest whole-proof systems, though Seed-Prover still reports 99.6%. Code and models are released at github.com/ByteDance-Seed/BFS-Prover-V2.

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

 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, Zeyu Zheng, Yanchen Nie, Kun Yuan and Xia Xiao. 2025. Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers. arXiv:2509.06493.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2509.06493 · arXiv 2509.06493

@misc{xin2025scaling,
  title = {{Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers}},
  author = {Ran Xin, Zeyu Zheng, Yanchen Nie, Kun Yuan and Xia Xiao},
  year = {2025},
  doi = {10.48550/arxiv.2509.06493},
  eprint = {2509.06493},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2509.06493}
}

References

43 references, 35 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. Thinking fast and slow with deep learning and tree search. Advances in neural information processing systems, 30, 2017.
  2. Kaito Baba, Chaoran Liu, Shuhei Kurita, and Akiyoshi Sannai. Prover agent: An agent-based framework for formal mathematical proofs. arXiv preprint arXiv:2506.19923, 2025.
  3. Wolfgang Bibel, Steffen Hölldobler, and Gerd Neugebauer. Deduction: automated logic. Academic Press London, 1993. find
  4. Mark Blokpoel. mathlib: A scala package for readable, verifiable and sustainable simulations of formal theory. Journal of Open Source Software, 9(99):6049, 2024. find
  5. Chenrui Cao, Liangcheng Song, Zenan Li, Xinyi Le, Xian Zhang, Hui Xue, and Fan Yang. Reviving dsp for advanced theorem proving in the era of reasoning models. arXiv preprint arXiv:2506.11487, 2025.
  6. Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving. arXiv preprint arXiv:2507.23726, 2025.
  7. Gheorghe Comanici, Eric Bieber, Mike Schaekermann, Ice Pasupat, Noveen Sachdeva, Inderjit Dhillon, Marcel Blistein, Ori Ram, Dan Zhang, Evan Rosen, et al. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities. arXiv preprint a…
  8. Herman Geuvers. Proof assistants: History, ideas and future. Sadhana, 34(1):3–25, 2009. find
  9. Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning. arXiv preprint arXiv:2501.12948, 2025.
  10. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203, 2021.
  11. Albert Q Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. arXiv preprint arXiv:2210.12283, 2022.
  12. Guillaume Lample, Timothée Lacroix, et al. Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems, 35:26337–26349, 2022.
  13. Jia Li, Edward Beeching, Lewis Tunstall, Ben Lipkin, Roman Soletskyi, Shengyi Huang, Kashif Rasul, Longhui Yu, Albert Q Jiang, Ziju Shen, et al. Numinamath: The largest public dataset in ai4maths with 860k pairs of competition math problems and solutions. Hugging Face repository, 13(9):9, 2024. find
  14. Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, and Haitao Mi. Hunyuanprover: A scalable data synthesis framework and guided tree search for automated theorem proving. arXiv preprint arXiv:2412.20735, 2024.
  15. Zhenwen Liang, Linfeng Song, Yang Li, Tao Yang, Feng Zhang, Haitao Mi, and Dong Yu. Mps-prover: Advancing stepwise theorem proving by multi-perspective search and data curation. arXiv preprint arXiv:2505.10962, 2025.
  16. Yong Lin, Shange Tang, Bohan Lyu, Jiayun Wu, Hongzhou Lin, Kaiyu Yang, Jia Li, Mengzhou Xia, Danqi Chen, Sanjeev Arora, et al. Goedel-prover: A frontier model for open-source automated theorem proving. arXiv preprint arXiv:2502.07640, 2025.
  17. Yong Lin, Shange Tang, Bohan Lyu, Ziran Yang, Jui-Hui Chung, Haoyu Zhao, Lai Jiang, Yihan Geng, Jiawei Ge, Jingruo Sun, et al. Goedel-prover-v2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. arXiv preprint arXiv:2508.03613, 2025.
  18. Mingjie Liu, Shizhe Diao, Ximing Lu, Jian Hu, Xin Dong, Yejin Choi, Jan Kautz, and Yi Dong. Prorl: Prolonged reinforcement learning expands reasoning boundaries in large language models. arXiv preprint arXiv:2505.24864, 2025.
  19. Leonardo de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction (CADE), pages 625–635. Springer, 2021. — The Lean 4 Theorem Prover and Programming Language (System Description)
  20. OpenAI. Gpt-4 technical report. arXiv preprint arXiv:2303.08774, 2023.
  21. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, et al. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  22. Martin L Puterman. Markov decision processes. Handbooks in operations research and management science, 2: 331–434, 1990. find
  23. ZZ Ren, Zhihong Shao, Junxiao Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, et al. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition. arXiv preprint arXiv:2504.21801, 2025.
  24. ByteDance Seed, Jiaze Chen, Tiantian Fan, Xin Liu, Lingjun Liu, Zhiqi Lin, Mingxuan Wang, Chengyi Wang, Xiangpeng Wei, Wenyuan Xu, et al. Seed1. 5-thinking: Advancing superb reasoning models with reinforcement learning. arXiv preprint arXiv:2504.13914, 2025.
  25. David Silver and Richard S Sutton. Welcome to the era of experience. Google AI, 1, 2025. find
  26. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, et al. A general reinforcement learning algorithm that masters chess, shogi, and go through self-play. Science, 362(6419):1140–1144, 2018. find
  27. Peiyang Song, Kaiyu Yang, and Anima Anandkumar. Towards large language models as copilots for theorem proving in lean. arXiv preprint arXiv:2404.12534, 2024.
  28. Richard S Sutton. Reinforcement learning: An introduction. A Bradford Book, 2018. find
  29. Kimi Team, Angang Du, Bofei Gao, Bowei Xing, Changjiu Jiang, Cheng Chen, Cheng Li, Chenjun Xiao, Chenzhuang Du, Chonghua Liao, et al. Kimi k1. 5: Scaling reinforcement learning with llms. arXiv preprint arXiv:2501.12599, 2025.
  30. Haiming Wang, Mert Unsal, Xiaohan Lin, Mantas Baksys, Junqi Liu, Marco Dos Santos, Flood Sung, Marina Vinyes, Zhenzhe Ying, Zekai Zhu, et al. Kimina-prover preview: Towards large formal reasoning models with reinforcement learning. arXiv preprint arXiv:2504.11354, 2025.
  31. Sean Welleck and Rahul Saha. Llmstep: Llm proofstep suggestions in lean. arXiv preprint arXiv:2310.18457, 2023.
  32. Zijian Wu, Suozhi Huang, Zhejian Zhou, Huaiyuan Ying, Jiayu Wang, Dahua Lin, and Kai Chen. Internlm2. 5-stepprover: Advancing automated theorem proving via expert iteration on large-scale lean problems. arXiv preprint arXiv:2410.15700, 2024.
  33. Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. Lean-github: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.17227, 2024.
  34. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024.
  35. Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024.
  36. Ran Xin, Chenguang Xi, Jie Yang, Feng Chen, Hang Wu, Xia Xiao, Yifan Sun, Shen Zheng, and Kai Shen. Bfs-prover: Scalable best-first tree search for llm-based automatic theorem proving. arXiv preprint arXiv:2502.03438, 2025.
  37. An Yang, Beichen Zhang, Binyuan Hui, Bofei Gao, Bowen Yu, Chengpeng Li, Dayiheng Liu, Jianhong Tu, Jingren Zhou, Junyang Lin, et al. Qwen2. 5-math technical report: Toward mathematical expert model via self-improvement. arXiv preprint arXiv:2409.12122, 2024.
  38. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. Formal mathematical reasoning: A new frontier in ai. arXiv preprint arXiv:2412.16075, 2024.
  39. Kaiyu Yang, Aidan Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J Prenger, and Animashree Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. Advances in Neural Information Processing Systems, 36, 2024.
  40. Huaiyuan Ying, Zijian Wu, Yihan Geng, Jiayu Wang, Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. arXiv preprint arXiv:2406.03847, 2024.
  41. Qiying Yu, Zheng Zhang, Ruofei Zhu, Yufeng Yuan, Xiaochen Zuo, Yu Yue, Weinan Dai, Tiantian Fan, Gaohong Liu, Lingjun Liu, et al. Dapo: An open-source llm reinforcement learning system at scale. arXiv preprint arXiv:2503.14476, 2025.
  42. Yu Yue, Yufeng Yuan, Qiying Yu, Xiaochen Zuo, Ruofei Zhu, Wenyuan Xu, Jiaze Chen, Chengyi Wang, TianTian Fan, Zhengyin Du, et al. Vapo: Efficient and reliable reinforcement learning for advanced reasoning tasks. arXiv preprint arXiv:2504.05118, 2025.
  43. Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, et al. Solving formal math problems by decomposition and iterative reflection. arXiv preprint arXiv:2507.15225, 2025.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/xin-2025-scaling-up-multi-turn-off/