Escalando el Aprendizaje por Refuerzo Off-Policy de Múltiples Turnos y la Búsqueda en Árbol Multiagente para Demostradores de Pasos con LLM

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

September 8, 2025

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

cs.AI

Resumen

La integración de los Modelos de Lenguaje a Gran Escala (LLMs, por sus siglas en inglés) en la demostración automática de teoremas ha mostrado un potencial inmenso, aunque está fundamentalmente limitada por los desafíos en la escalabilidad tanto del aprendizaje por refuerzo (RL, por sus siglas en inglés) durante el entrenamiento como del cómputo durante la inferencia. Este artículo presenta BFS-Prover-V2, un sistema diseñado para abordar este problema de escalabilidad dual. Presentamos dos innovaciones principales. La primera es un marco novedoso de RL fuera de política de múltiples turnos para mejorar continuamente el rendimiento del demostrador de pasos basado en LLMs durante el entrenamiento. Este marco, inspirado en los principios de AlphaZero, utiliza una canalización de iteración experta en múltiples etapas que incluye filtrado adaptativo de datos a nivel de táctica y reentrenamiento periódico para superar las mesetas de rendimiento que suelen limitar el RL a largo plazo en agentes basados en LLMs. La segunda innovación es una arquitectura de búsqueda multiagente mejorada con un planificador que escala las capacidades de razonamiento durante la inferencia. Esta arquitectura emplea un modelo de razonamiento general como planificador de alto nivel para descomponer iterativamente teoremas complejos en una secuencia de subobjetivos más simples. Este enfoque jerárquico reduce sustancialmente el espacio de búsqueda, permitiendo que un equipo de agentes demostradores paralelos colaboren de manera eficiente al aprovechar una caché de pruebas compartida. Demostramos que este enfoque dual de escalabilidad produce resultados de vanguardia en benchmarks establecidos de matemáticas formales. BFS-Prover-V2 logra un 95,08 % y un 41,4 % en los conjuntos de prueba de MiniF2F y ProofNet, respectivamente. Aunque se ha demostrado en el ámbito de las matemáticas formales, las técnicas de RL e inferencia presentadas en este trabajo son de interés más amplio y pueden aplicarse a otros dominios que requieran razonamiento de múltiples turnos a largo plazo y búsquedas complejas.

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.