Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM
  Step-Provers
The integration of Large Language Models (LLMs) into automated theorem
proving has shown immense promise, yet is fundamentally constrained by
challenges in scaling up both training-time reinforcement learning (RL) and
inference-time compute. This paper introduces BFS-Prover-V2, a system
designed to address this dual scaling problem. We present two primary
innovations. The first is a novel multi-turn off-policy RL framework for
continually improving the performance of LLM step-prover at training time. This
framework, inspired by the principles of AlphaZero, utilizes a multi-stage
expert iteration pipeline featuring adaptive tactic-level data filtering and
periodic retraining to surmount the performance plateaus that typically curtail
long-term RL in LLM-based agents. The second innovation is a planner-enhanced
multi-agent search architecture that scales reasoning capabilities at inference
time. This architecture employs a general reasoning model as a high-level
planner to iteratively decompose complex theorems into a sequence of simpler
subgoals. This hierarchical approach substantially reduces the search space,
enabling a team of parallel prover agents to collaborate efficiently by
leveraging a shared proof cache. We demonstrate that this dual approach to
scaling yields state-of-the-art results on established formal mathematics
benchmarks. BFS-Prover-V2 achieves 95.08\% and 41.4\% on the MiniF2F
and ProofNet test sets respectively. While demonstrated in the domain of formal
mathematics, the RL and inference techniques presented in this work are of
broader interest and may be applied to other domains requiring long-horizon
multi-turn reasoning and complex search.
68bf940c207285de11b07b8d
Ran Xin
68bf940c207285de11b07b8e
Zeyu Zheng
claimed_verified
2025-09-19T06:50:42.014Z
67cffe31d6f5c181e523610c
/avatars/8706e09fc4397456baeddb8942c8b0ee.svg
Zeyu Zheng
user
zeyu-zheng
68bf940c207285de11b07b8f
Yanchen Nie
68bf940c207285de11b07b90
Kun Yuan
68bf940c207285de11b07b91
Xia Xiao
Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM
  Step-Provers
The integration of Large Language Models (LLMs) into automated theorem
proving has shown immense promise, yet is fundamentally constrained by
challenges in scaling up both training-time reinforcement learning (RL) and
inference-time compute. This paper introduces BFS-Prover-V2, a system
designed to address this dual scaling problem. We present two primary
innovations. The first is a novel multi-turn off-policy RL framework for
continually improving the performance of LLM step-prover at training time. This
framework, inspired by the principles of AlphaZero, utilizes a multi-stage
expert iteration pipeline featuring adaptive tactic-level data filtering and
periodic retraining to surmount the performance plateaus that typically curtail
long-term RL in LLM-based agents. The second innovation is a planner-enhanced
multi-agent search architecture that scales reasoning capabilities at inference
time. This architecture employs a general reasoning model as a high-level
planner to iteratively decompose complex theorems into a sequence of simpler
subgoals. This hierarchical approach substantially reduces the search space,
enabling a team of parallel prover agents to collaborate efficiently by
leveraging a shared proof cache. We demonstrate that this dual approach to
scaling yields state-of-the-art results on established formal mathematics
benchmarks. BFS-Prover-V2 achieves 95.08\% and 41.4\% on the MiniF2F
and ProofNet test sets respectively. While demonstrated in the domain of formal
mathematics, the RL and inference techniques presented in this work are of
broader interest and may be applied to other domains requiring long-horizon
multi-turn reasoning and complex search.
BFS-Prover-V2 addresses scaling challenges in automated theorem proving by integrating a multi-turn off-policy RL framework and a planner-enhanced multi-agent search architecture, achieving state-of-the-art results on formal mathematics benchmarks.
Large Language Models automated theorem proving reinforcement learning off-policy RL AlphaZero multi-stage expert iteration adaptive tactic-level data filtering periodic retraining planner-enhanced multi-agent search general reasoning model high-level planner subgoals shared proof cache MiniF2F ProofNet