Бурбаки: Самостоятельно генерируемые и целеориентированные марковские процессы принятия решений для доказательства теорем

Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving

July 3, 2025

Авторы: Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, Jun Wang, Haitham Bou Ammar

cs.AI

Аннотация

Логические рассуждения остаются сложной задачей для больших языковых моделей (LLM), особенно в рамках логически ограниченной среды автоматического доказательства теорем (ATP), из-за редких вознаграждений и огромного масштаба доказательств. Эти трудности усиливаются в тестах, таких как PutnamBench, которые содержат университетские задачи, требующие сложного, многошагового рассуждения. Для решения этой проблемы мы представляем самоформируемые марковские процессы принятия решений с условием цели (sG-MDP) — новый подход, в котором агенты генерируют и преследуют свои подцели на основе изменяющегося состояния доказательства. Благодаря более структурированному формированию целей, результирующая задача становится более подходящей для поиска. Затем мы применяем алгоритмы, подобные поиску по дереву Монте-Карло (MCTS), для решения sG-MDP, реализуя наш подход в системе Bourbaki (7B) — модульной системе, которая может объединять несколько 7B LLM для генерации подцелей и синтеза тактик. На тесте PutnamBench Bourbaki (7B) решает 26 задач, достигая новых наилучших результатов для моделей такого масштаба.

English

Reasoning remains a challenging task for large language models (LLMs), especially within the logically constrained environment of automated theorem proving (ATP), due to sparse rewards and the vast scale of proofs. These challenges are amplified in benchmarks like PutnamBench, which contains university-level problems requiring complex, multi-step reasoning. To address this, we introduce self-generated goal-conditioned MDPs (sG-MDPs), a new framework in which agents generate and pursue their subgoals based on the evolving proof state. Given this more structured generation of goals, the resulting problem becomes more amenable to search. We then apply Monte Carlo Tree Search (MCTS)-like algorithms to solve the sG-MDP, instantiating our approach in Bourbaki (7B), a modular system that can ensemble multiple 7B LLMs for subgoal generation and tactic synthesis. On PutnamBench, Bourbaki (7B) solves 26 problems, achieving new state-of-the-art results with models at this scale.