Bourbaki: MDPs Autogenerados y Condicionados por Objetivos para la Demostración 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

Resumen

El razonamiento sigue siendo una tarea desafiante para los modelos de lenguaje de gran escala (LLMs, por sus siglas en inglés), especialmente en el entorno lógicamente restringido de la demostración automática de teoremas (ATP, por sus siglas en inglés), debido a las recompensas escasas y la gran escala de las demostraciones. Estos desafíos se amplifican en puntos de referencia como PutnamBench, que contiene problemas de nivel universitario que requieren un razonamiento complejo y de múltiples pasos. Para abordar esto, introducimos los MDPs condicionados por objetivos autogenerados (sG-MDPs, por sus siglas en inglés), un nuevo marco en el que los agentes generan y persiguen sus subobjetivos basándose en el estado evolutivo de la demostración. Dada esta generación más estructurada de objetivos, el problema resultante se vuelve más susceptible a la búsqueda. Luego aplicamos algoritmos similares a la Búsqueda de Árbol de Monte Carlo (MCTS, por sus siglas en inglés) para resolver el sG-MDP, implementando nuestro enfoque en Bourbaki (7B), un sistema modular que puede ensamblar múltiples LLMs de 7B para la generación de subobjetivos y la síntesis de tácticas. En PutnamBench, Bourbaki (7B) resuelve 26 problemas, logrando nuevos resultados de vanguardia con modelos de esta 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.