Масштабирование многократного обучения с подкреплением вне политики и поиска по дереву для многоагентных систем в задачах пошагового доказательства для больших языковых моделей

Аннотация

Интеграция крупных языковых моделей (LLM) в автоматизированное доказательство теорем демонстрирует огромный потенциал, однако сталкивается с фундаментальными ограничениями, связанными с масштабированием как обучения с подкреплением (RL) на этапе тренировки, так и вычислительных ресурсов на этапе вывода. В данной статье представлена система BFS-Prover-V2, разработанная для решения этой двойной проблемы масштабирования. Мы предлагаем два ключевых нововведения. Первое — это новый многократный off-policy RL-фреймворк, предназначенный для постоянного улучшения производительности LLM-шагового доказателя на этапе обучения. Этот фреймворк, вдохновленный принципами AlphaZero, использует многоэтапный конвейер экспертной итерации с адаптивной фильтрацией данных на уровне тактик и периодическим переобучением, чтобы преодолеть плато производительности, которые обычно ограничивают долгосрочное RL в агентах на основе LLM. Второе нововведение — это архитектура многозадачного поиска с усилением планировщика, которая масштабирует возможности рассуждений на этапе вывода. Эта архитектура использует общую модель рассуждений в качестве высокоуровневого планировщика для итеративного разложения сложных теорем на последовательность более простых подцелей. Такой иерархический подход существенно сокращает пространство поиска, позволяя команде параллельных агентов-доказывателей эффективно сотрудничать, используя общий кэш доказательств. Мы показываем, что этот двойной подход к масштабированию обеспечивает передовые результаты на установленных бенчмарках формальной математики. BFS-Prover-V2 достигает 95,08% и 41,4% на тестовых наборах MiniF2F и ProofNet соответственно. Хотя результаты продемонстрированы в области формальной математики, представленные в работе методы RL и вывода имеют более широкое применение и могут быть использованы в других областях, требующих многократных рассуждений на длинных горизонтах и сложного поиска.

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.

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

Аннотация

Support