Scalabilità dell'Apprendimento per Rinforzo Off-Policy Multi-Turn e della Ricerca ad Albero Multi-Agente per i Dimostratori Passo-Passo di LLM

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

September 8, 2025

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

cs.AI

Abstract

L'integrazione dei Large Language Models (LLM) nel campo del teorema automatico ha dimostrato un enorme potenziale, ma è fondamentalmente limitata dalle sfide legate alla scalabilità sia dell'apprendimento per rinforzo (RL) durante l'addestramento sia del calcolo durante l'inferenza. Questo articolo introduce BFS-Prover-V2, un sistema progettato per affrontare questo duplice problema di scalabilità. Presentiamo due innovazioni principali. La prima è un nuovo framework RL multi-turn off-policy per migliorare continuamente le prestazioni del passo-prover basato su LLM durante l'addestramento. Questo framework, ispirato ai principi di AlphaZero, utilizza una pipeline di iterazione esperta multi-stage che include un filtraggio adattivo dei dati a livello tattico e un riaddestramento periodico per superare i plateau di prestazione che tipicamente limitano l'RL a lungo termine negli agenti basati su LLM. La seconda innovazione è un'architettura di ricerca multi-agente potenziata da un pianificatore che scala le capacità di ragionamento durante l'inferenza. Questa architettura impiega un modello di ragionamento generale come pianificatore di alto livello per scomporre iterativamente teoremi complessi in una sequenza di sottobiettivi più semplici. Questo approccio gerarchico riduce sostanzialmente lo spazio di ricerca, consentendo a un team di agenti prover paralleli di collaborare in modo efficiente sfruttando una cache di prove condivisa. Dimostriamo che questo duplice approccio alla scalabilità produce risultati all'avanguardia su benchmark consolidati di matematica formale. BFS-Prover-V2 raggiunge il 95,08% e il 41,4% rispettivamente sui set di test MiniF2F e ProofNet. Sebbene dimostrato nel dominio della matematica formale, le tecniche di RL e inferenza presentate in questo lavoro sono di interesse più ampio e possono essere applicate ad altri domini che richiedono ragionamenti multi-turn a lungo termine e ricerche complesse.

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.