Escalonando o Aprendizado por Reforço Off-Policy de Múltiplos Turnos e a Busca em Árvore Multiagente para Provadores de Passos em LLMs

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

Resumo

A integração de Modelos de Linguagem de Grande Escala (LLMs) na prova automática de teoremas tem mostrado um imenso potencial, mas é fundamentalmente limitada pelos desafios de escalonamento tanto no aprendizado por reforço (RL) durante o treinamento quanto no poder computacional durante a inferência. Este artigo apresenta o BFS-Prover-V2, um sistema projetado para abordar esse problema duplo de escalonamento. Apresentamos duas inovações principais. A primeira é uma nova estrutura de RL multi-turn off-policy para melhorar continuamente o desempenho do provador de passos baseado em LLM durante o treinamento. Essa estrutura, inspirada nos princípios do AlphaZero, utiliza um pipeline de iteração especializada em múltiplos estágios, com filtragem adaptativa de dados em nível tático e retreinamento periódico, para superar os platôs de desempenho que normalmente limitam o RL de longo prazo em agentes baseados em LLM. A segunda inovação é uma arquitetura de busca multiagente aprimorada por planejamento que escala as capacidades de raciocínio durante a inferência. Essa arquitetura emprega um modelo de raciocínio geral como um planejador de alto nível para decompor iterativamente teoremas complexos em uma sequência de subobjetivos mais simples. Essa abordagem hierárquica reduz substancialmente o espaço de busca, permitindo que uma equipe de agentes provadores paralelos colaborem de forma eficiente, aproveitando um cache de provas compartilhado. Demonstramos que essa abordagem dupla para escalonamento produz resultados de ponta em benchmarks estabelecidos de matemática formal. O BFS-Prover-V2 alcança 95,08% e 41,4% nos conjuntos de teste MiniF2F e ProofNet, respectivamente. Embora demonstrado no domínio da matemática formal, as técnicas de RL e inferência apresentadas neste trabalho têm um interesse mais amplo e podem ser aplicadas a outros domínios que exigem raciocínio multi-turn de longo horizonte e busca complexa.

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.