Skalierung von Multi-Turn Off-Policy Reinforcement Learning und Multi-Agenten-Baumsuche für LLM-Schrittbeweiser

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

September 8, 2025

papers.authors: Ran Xin, Zeyu Zheng, Yanchen Nie, Kun Yuan, Xia Xiao

cs.AI

papers.abstract

Die Integration von Large Language Models (LLMs) in das automatisierte Theorembeweisen hat enormes Potenzial gezeigt, ist jedoch grundlegend durch Herausforderungen bei der Skalierung sowohl des Reinforcement Learning (RL) während des Trainings als auch der Rechenleistung während der Inferenz eingeschränkt. Dieses Papier stellt BFS-Prover-V2 vor, ein System, das entwickelt wurde, um dieses duale Skalierungsproblem zu adressieren. Wir präsentieren zwei primäre Innovationen. Die erste ist ein neuartiges Multi-Turn Off-Policy RL-Framework, das kontinuierlich die Leistung des LLM-Schrittbeweisers während des Trainings verbessert. Dieses Framework, inspiriert von den Prinzipien von AlphaZero, nutzt eine mehrstufige Expert-Iteration-Pipeline mit adaptiver Taktik-Level-Datenfilterung und periodischem Retraining, um die Leistungsplateaus zu überwinden, die typischerweise das langfristige RL in LLM-basierten Agenten begrenzen. Die zweite Innovation ist eine Planer-verstärkte Multi-Agenten-Sucharchitektur, die die Fähigkeiten zur logischen Schlussfolgerung während der Inferenz skaliert. Diese Architektur verwendet ein allgemeines Schlussfolgerungsmodell als hochrangigen Planer, um komplexe Theoreme iterativ in eine Sequenz einfacherer Teilziele zu zerlegen. Dieser hierarchische Ansatz reduziert den Suchraum erheblich und ermöglicht es einem Team paralleler Beweisagenten, effizient zusammenzuarbeiten, indem sie einen gemeinsamen Beweiscache nutzen. Wir zeigen, dass dieser duale Ansatz zur Skalierung state-of-the-art Ergebnisse auf etablierten Benchmarks für formale Mathematik liefert. BFS-Prover-V2 erreicht 95,08 % und 41,4 % auf den Testdatensätzen von MiniF2F und ProofNet. Obwohl im Bereich der formalen Mathematik demonstriert, sind die in dieser Arbeit vorgestellten RL- und Inferenztechniken von breiterem Interesse und können auf andere Domänen angewendet werden, die langfristige Multi-Turn-Schlussfolgerungen und komplexe Suchprozesse erfordern.

English

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.