---
title: "Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search"
description: "The authors present BFS-Prover-V2, an open-source step-level prover that treats proving as a Markov… 43 references, cited by 7 papers here."
authors: ["Ran Xin", "Zeyu Zheng", "Yanchen Nie", "Kun Yuan", "Xia Xiao"]
year: 2025
venue: "arXiv:2509.06493"
source: "https://arxiv.org/abs/2509.06493"
doi: "10.48550/arxiv.2509.06493"
arxiv: "2509.06493"
licence: "arXiv — non-exclusive licence to distribute"
licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html"
summary_licence: "Elamur Cosmic License"
canonical: "https://research.elamur.ai/free/en/papers/xin-2025-scaling-up-multi-turn-off/"
---
[Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/xin-2025-scaling-up-multi-turn-off/)

[home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2025](https://md.research.elamur.ai/free/en/papers/2025/page/12/) / 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

**Authors:** [Ran Xin](https://md.research.elamur.ai/free/en/authors/ran-xin/), [Zeyu Zheng](https://md.research.elamur.ai/free/en/authors/zeyu-zheng/), Yanchen Nie, Kun Yuan and [Xia Xiao](https://md.research.elamur.ai/free/en/authors/xia-xiao/) · **Year:** 2025 · **Venue:** arXiv:2509.06493 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html)

**Links:** [Publisher's page](https://arxiv.org/abs/2509.06493) · [PDF](https://arxiv.org/pdf/2509.06493v2) · [DOI 10.48550/arxiv.2509.06493](https://doi.org/10.48550/arxiv.2509.06493) · [arXiv 2509.06493](https://arxiv.org/abs/2509.06493) · [OpenAlex](https://openalex.org/W4414756988)

**Citations:** 0 citations (OpenAlex, 2026-10-14) · [7](https://md.research.elamur.ai/free/en/papers/xin-2025-scaling-up-multi-turn-off/cited-by/) in our library, of the 149,439 papers whose bibliographies we read

## 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.*

📚 Shelves (3): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works

🧭 Topics (1): [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/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.

```bibtex
@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}
}
```

- [← previous Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://md.research.elamur.ai/free/en/papers/cao-2025-reviving-dsp-advanced-theorem-proving/)
- [next → StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusion](https://md.research.elamur.ai/free/en/papers/wu-2025-stepfun-formalizer-unlocking-autoformalization/)
- [↑ back to papers of 2025](https://md.research.elamur.ai/free/en/papers/2025/page/12/)

## 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](https://md.research.elamur.ai/free/en/papers/anthony-2017-thinking-fast-slow-deep-learning/). 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](https://md.research.elamur.ai/free/en/papers/baba-2025-prover-agent-agent-based-framework/). arXiv preprint arXiv:2506.19923, 2025.
3. Wolfgang Bibel, Steffen Hölldobler, and Gerd Neugebauer. Deduction: automated logic. Academic Press London, 1993. [find](https://scholar.google.com/scholar?q=Wolfgang+Bibel%2C+Steffen+H%C3%B6lldobler%2C+and+Gerd+Neugebauer%2E+Deduction%3A+automated+logic%2E+Academic+Press+London%2C+1993%2E)
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](https://scholar.google.com/scholar?q=Mark+Blokpoel%2E+mathlib%3A+A+scala+package+for+readable%2C+verifiable+and+sustainable+simulations+of+formal+theory%2E+Journal+of+Open+Source+Software%2C+9%2899%29%3A6049%2C+2024%2E)
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](https://md.research.elamur.ai/free/en/papers/cao-2025-reviving-dsp-advanced-theorem-proving/). 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](https://md.research.elamur.ai/free/en/papers/chen-2025-seed-prover-deep-broad-reasoning/). 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](https://md.research.elamur.ai/free/en/papers/comanici-2025-gemini-2-5-pushing-frontier/). arXiv preprint a…
8. Herman Geuvers. Proof assistants: History, ideas and future. Sadhana, 34(1):3–25, 2009. [find](https://scholar.google.com/scholar?q=Herman+Geuvers%2E+Proof+assistants%3A+History%2C+ideas+and+future%2E+Sadhana%2C+34%281%29%3A3%E2%80%9325%2C+2009%2E)
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](https://md.research.elamur.ai/free/en/papers/deepseek-ai-2025-deepseek-r1-incentivizing-reasoning-capability/). 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](https://md.research.elamur.ai/free/en/papers/han-2021-proof-artifact-co-training-theorem/). 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](https://md.research.elamur.ai/free/en/papers/jiang-2022-draft-sketch-prove-guiding-formal/). arXiv preprint arXiv:2210.12283, 2022.
12. Guillaume Lample, Timothée Lacroix, et al. [Hypertree proof search for neural theorem proving](https://md.research.elamur.ai/free/en/papers/lample-2022-hypertree-proof-search-neural-theorem/). 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](https://scholar.google.com/scholar?q=Jia+Li%2C+Edward+Beeching%2C+Lewis+Tunstall%2C+Ben+Lipkin%2C+Roman+Soletskyi%2C+Shengyi+Huang%2C+Kashif+Rasul%2C+Longhui+Yu%2C+Albert+Q+Jiang%2C+Ziju+Shen%2C+et+al%2E+Numinamath%3A+The+largest+public+dataset+in+ai4maths+with)
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](https://md.research.elamur.ai/free/en/papers/li-2024-hunyuanprover-scalable-data-synthesis/). 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](https://md.research.elamur.ai/free/en/papers/liang-2025-mps-prover-advancing-stepwise-theorem/). 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](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-frontier-model-open/). 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](https://md.research.elamur.ai/free/en/papers/lin-2025-goedel-prover-v2-scaling-formal/). 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](https://md.research.elamur.ai/free/en/papers/liu-2025-prorl-prolonged-reinforcement-learning-expands/). 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)](https://md.research.elamur.ai/free/en/papers/moura-2021-lean-4-theorem-prover-programming/)
20. OpenAI. [Gpt-4 technical report](https://md.research.elamur.ai/free/en/papers/openai-2023-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](https://md.research.elamur.ai/free/en/papers/polu-2022-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](https://scholar.google.com/scholar?q=Martin+L+Puterman%2E+Markov+decision+processes%2E+Handbooks+in+operations+research+and+management+science%2C+2%3A+331%E2%80%93434%2C+1990%2E)
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](https://md.research.elamur.ai/free/en/papers/ren-2025-deepseek-prover-v2-advancing-formal/). 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](https://md.research.elamur.ai/free/en/papers/bytedance-seed-2025-seed1-5-thinking-advancing/).
25. David Silver and Richard S Sutton. Welcome to the era of experience. Google AI, 1, 2025. [find](https://scholar.google.com/scholar?q=David+Silver+and+Richard+S+Sutton%2E+Welcome+to+the+era+of+experience%2E+Google+AI%2C+1%2C+2025%2E)
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](https://scholar.google.com/scholar?q=David+Silver%2C+Thomas+Hubert%2C+Julian+Schrittwieser%2C+Ioannis+Antonoglou%2C+Matthew+Lai%2C+Arthur+Guez%2C+Marc+Lanctot%2C+Laurent+Sifre%2C+Dharshan+Kumaran%2C+Thore+Graepel%2C+et+al%2E+A+general+reinforcement+learning+a)
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](https://md.research.elamur.ai/free/en/papers/song-2024-lean-copilot-large-language-models/).
28. Richard S Sutton. Reinforcement learning: An introduction. A Bradford Book, 2018. [find](https://scholar.google.com/scholar?q=Richard+S+Sutton%2E+Reinforcement+learning%3A+An+introduction%2E+A+Bradford+Book%2C+2018%2E)
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](https://md.research.elamur.ai/free/en/papers/kimi-team-2025-kimi-k1-5-scaling-reinforcement/).
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](https://md.research.elamur.ai/free/en/papers/wang-2025-kimina-prover-preview-large-formal/). arXiv preprint arXiv:2504.11354, 2025.
31. Sean Welleck and Rahul Saha. [Llmstep: Llm proofstep suggestions in lean](https://md.research.elamur.ai/free/en/papers/welleck-2023-llmstep-llm-proofstep-suggestions-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](https://md.research.elamur.ai/free/en/papers/wu-2024-internlm2-5-stepprover-advancing-automated/).
33. Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. [Lean-github: Compiling github lean repositories for a versatile lean prover](https://md.research.elamur.ai/free/en/papers/wu-2024-lean-github-compiling-github-lean/). 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](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-advancing-theorem-proving/). 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](https://md.research.elamur.ai/free/en/papers/xin-2024-deepseek-prover-v1-5-harnessing/).
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](https://md.research.elamur.ai/free/en/papers/xin-2025-bfs-prover-scalable-best-first/). 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](https://md.research.elamur.ai/free/en/papers/yang-2024-qwen2-5-math-technical-report/).
38. Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, and Dawn Song. [Formal mathematical reasoning: A new frontier in ai](https://md.research.elamur.ai/free/en/papers/yang-2024-formal-mathematical-reasoning-new-frontier/). 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](https://md.research.elamur.ai/free/en/papers/yang-2023-leandojo-theorem-proving-retrieval-augmented/). 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](https://md.research.elamur.ai/free/en/papers/ying-2024-lean-workbook-large-scale-lean/). 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](https://md.research.elamur.ai/free/en/papers/yu-2025-dapo-open-source-llm-reinforcement/). 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](https://md.research.elamur.ai/free/en/papers/yue-2025-vapo-efficient-reliable-reinforcement-learning/). 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](https://md.research.elamur.ai/free/en/papers/zhou-2025-solving-formal-math-problems-decomposition/). arXiv preprint arXiv:2507.15225, 2025.

*Updated 3 November 2026*