Bourbaki: MDPs Autogerados e Condicionados por Objetivos para Prova de Teoremas

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

July 3, 2025

Autores: Matthieu Zimmer, Xiaotong Ji, Rasul Tutunov, Anthony Bordg, Jun Wang, Haitham Bou Ammar

cs.AI

Resumo

O raciocínio continua sendo uma tarefa desafiadora para grandes modelos de linguagem (LLMs), especialmente no ambiente logicamente restrito da prova automática de teoremas (ATP), devido à escassez de recompensas e à vasta escala das provas. Esses desafios são amplificados em benchmarks como o PutnamBench, que contém problemas de nível universitário que exigem raciocínio complexo e de múltiplas etapas. Para abordar isso, introduzimos MDPs condicionados a objetivos auto-gerados (sG-MDPs), um novo framework no qual os agentes geram e perseguem seus subobjetivos com base no estado evolutivo da prova. Dada essa geração mais estruturada de objetivos, o problema resultante torna-se mais passível de busca. Em seguida, aplicamos algoritmos semelhantes à Busca em Árvore de Monte Carlo (MCTS) para resolver o sG-MDP, instanciando nossa abordagem no Bourbaki (7B), um sistema modular que pode combinar múltiplos LLMs de 7B para geração de subobjetivos e síntese de táticas. No PutnamBench, o Bourbaki (7B) resolve 26 problemas, alcançando novos resultados de ponta com modelos nessa escala.

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.