TLDR: BFS-Prover-V2 is a new system that significantly improves Large Language Model (LLM) based automated theorem proving. It tackles two main challenges: scaling training and scaling inference. For training, it uses a multi-turn off-policy reinforcement learning framework with adaptive data filtering and periodic retraining to prevent performance plateaus. For inference, it employs a planner-enhanced multi-agent search where a high-level planner breaks down complex problems into subgoals, which are then solved collaboratively by multiple prover agents. This dual approach achieves state-of-the-art results on formal mathematics benchmarks like MiniF2F and ProofNet.
Automated Theorem Proving (ATP) is a foundational ambition in computer science, aiming to use computers to prove mathematical theorems. With the rise of Large Language Models (LLMs), there’s immense potential to integrate their powerful generation and search capabilities with the rigorous verification of formal systems like Lean4. This integration creates a feedback loop where LLMs propose proof steps, a compiler verifies them, and reinforcement learning (RL) continuously improves the LLM’s reasoning abilities.
However, developing high-performance LLM-based provers faces two significant scaling challenges: training-time scaling and inference-time scaling.
Training-Time Scaling: Overcoming Performance Plateaus
Training-time scaling refers to the techniques needed to continuously enhance a model’s capabilities. A common issue in applying RL to LLMs is performance plateaus, where models stop improving despite continued training. To address this, the paper introduces a novel multi-turn off-policy RL framework, inspired by AlphaZero, for continually improving LLM step-provers.
This framework uses a multi-stage expert iteration pipeline. In the proof generation phase, the current best LLM prover, acting as an expert, solves a vast number of mathematical problems using a best-first tree search. The successful proof paths generate a massive dataset of (state, tactic) pairs. In the model refinement phase, this data is used to update the LLM’s parameters, making it the new expert for the next round.
To sustain learning and overcome plateaus, two key innovations are introduced:
-
Adaptive Tactic Filtering: Instead of filtering data at a coarse problem level, this approach dynamically filters at the tactic level based on the LLM’s own uncertainty (perplexity). Tactics with very low perplexity (too easy) or very high perplexity (noisy or suboptimal) are filtered out. The model focuses on the “goldilocks zone” – tactics that are challenging but within its grasp, ensuring it learns at the edge of its capabilities.
-
Periodic Retraining: Even with adaptive filtering, performance can plateau. To escape these local optima, a “soft reset” procedure is used. The current expert re-solves all past problems, generating cleaner, more efficient proofs. This high-quality data is then aggressively curated, and a fresh model is trained from scratch on this refined dataset. This temporarily drops performance but significantly increases the model’s exploratory potential, allowing it to discover novel strategies and surpass previous performance peaks.
Inference-Time Scaling: Decomposing Complexity with a Planner and Multi-Agents
Inference-time scaling deals with applying a trained model to solve new, complex theorems, which often require deep, multi-step reasoning and navigating an exponentially large search space. BFS-Prover-V2 introduces a planner-enhanced multi-agent search architecture to scale reasoning capabilities at inference time.
This hierarchical architecture divides labor between two distinct LLM agents:
-
The Planner: A general-purpose reasoning LLM that acts as a high-level strategist. It iteratively decomposes complex theorems into a sequence of simpler subgoals (intermediate lemmas). This significantly reduces the search space for the prover.
-
The Prover: A specialized LLM tactic generator, trained by the multi-stage expert iteration pipeline. It receives one subgoal at a time from the Planner and uses its learned policy with best-first search to find a formal proof for that specific subgoal.
The interaction between the Planner and Prover is a dynamic loop. If the Prover gets stuck on a subgoal, the Planner is re-queried with the updated context (including any successfully proven subgoals) to generate a revised plan. This dynamic replanning makes the system resilient to bottlenecks.
To accelerate the proof search, the system employs a multi-agent framework with focused parallelism and a shared subgoal cache. Multiple Prover instances concentrate their computational power on one subgoal at a time. As soon as one agent finds a proof, it’s written to the shared cache, signaling others to stop, preventing redundant computation, and allowing the team to move to the next subgoal.
Also Read:
- ParaThinker: Unlocking LLM Reasoning Potential Through Native Parallel Thinking
- Sticker-TTS: A New Framework for Smarter AI Reasoning Through Historical Experience
State-of-the-Art Results
This dual approach to scaling has yielded impressive results. BFS-Prover-V2 achieves state-of-the-art performance on established formal mathematics benchmarks, including 95.08% on the MiniF2F test set and 41.4% on the ProofNet test set. These results demonstrate the system’s ability to master problem distributions and generalize to more complex, undergraduate-level problems.
While demonstrated in formal mathematics, the RL and inference techniques presented in this work are broadly applicable to other domains requiring long-horizon multi-turn reasoning and complex search. For more details, you can read the full research paper here.
