Opschalen van Multi-Turn Off-Policy RL en Multi-Agent Tree Search voor LLM Stap-voor-Stap Bewijzers

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

September 8, 2025

Auteurs: Ran Xin, Zeyu Zheng, Yanchen Nie, Kun Yuan, Xia Xiao

cs.AI

Samenvatting

De integratie van Large Language Models (LLM's) in geautomatiseerd bewijzen van stellingen heeft enorme belofte getoond, maar wordt fundamenteel beperkt door uitdagingen in het opschalen van zowel reinforcement learning (RL) tijdens de training als de rekencapaciteit tijdens de inferentie. Dit artikel introduceert BFS-Prover-V2, een systeem ontworpen om dit dubbele schaalprobleem aan te pakken. We presenteren twee primaire innovaties. De eerste is een nieuw multi-turn off-policy RL-raamwerk voor het continu verbeteren van de prestaties van de LLM-stapbewijzer tijdens de training. Dit raamwerk, geïnspireerd door de principes van AlphaZero, maakt gebruik van een meerfasen expert-iteratiepijplijn met adaptieve tactiekniveau datafiltering en periodieke hertraining om de prestatieplateaus te overwinnen die doorgaans langdurige RL in LLM-gebaseerde agenten beperken. De tweede innovatie is een planner-versterkte multi-agent zoekarchitectuur die de redeneercapaciteiten tijdens de inferentie opschaalt. Deze architectuur gebruikt een algemeen redeneermodel als een hoog niveau planner om complexe stellingen iteratief te decomponeren in een reeks eenvoudigere subdoelen. Deze hiërarchische aanpak vermindert de zoekruimte aanzienlijk, waardoor een team van parallelle bewijzeragenten efficiënt kan samenwerken door gebruik te maken van een gedeelde bewijscache. We demonstreren dat deze dubbele aanpak tot state-of-the-art resultaten leidt op gevestigde benchmarks voor formele wiskunde. BFS-Prover-V2 behaalt 95,08% en 41,4% op respectievelijk de MiniF2F- en ProofNet-test sets. Hoewel gedemonstreerd in het domein van formele wiskunde, zijn de RL- en inferentietechnieken die in dit werk worden gepresenteerd van breder belang en kunnen ze worden toegepast op andere domeinen die langetermijn multi-turn redenering en complex zoeken vereisen.

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.