Mise à l'échelle de l'apprentissage par renforcement hors politique multi-tours et de la recherche arborescente multi-agents pour les prouveurs pas à pas basés sur des modèles de langage de grande taille

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

L'intégration des modèles de langage à grande échelle (LLMs) dans la démonstration automatique de théorèmes a montré un immense potentiel, mais elle est fondamentalement limitée par les défis liés à la montée en puissance de l'apprentissage par renforcement (RL) pendant l'entraînement et du calcul pendant l'inférence. Cet article présente BFS-Prover-V2, un système conçu pour résoudre ce double problème de montée en puissance. Nous présentons deux innovations principales. La première est un nouveau cadre de RL multi-tours hors politique pour améliorer continuellement les performances du démonstrateur pas-à-pas basé sur un LLM pendant l'entraînement. Inspiré des principes d'AlphaZero, ce cadre utilise un pipeline d'itération experte en plusieurs étapes, incluant un filtrage adaptatif des données au niveau tactique et un réentraînement périodique, pour surmonter les plateaux de performance qui limitent généralement le RL à long terme dans les agents basés sur des LLMs. La seconde innovation est une architecture de recherche multi-agents améliorée par un planificateur, qui permet de mettre à l'échelle les capacités de raisonnement pendant l'inférence. Cette architecture emploie un modèle de raisonnement général comme planificateur de haut niveau pour décomposer itérativement des théorèmes complexes en une séquence de sous-objectifs plus simples. Cette approche hiérarchique réduit considérablement l'espace de recherche, permettant à une équipe d'agents démonstrateurs parallèles de collaborer efficacement en exploitant un cache de preuves partagé. Nous démontrons que cette double approche de mise à l'échelle produit des résultats de pointe sur des benchmarks établis en mathématiques formelles. BFS-Prover-V2 atteint respectivement 95,08 % et 41,4 % sur les ensembles de test MiniF2F et ProofNet. Bien que démontrées dans le domaine des mathématiques formelles, les techniques de RL et d'inférence présentées dans ce travail ont un intérêt plus large et peuvent être appliquées à d'autres domaines nécessitant un raisonnement multi-tours à long terme et une recherche complexe.

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.