Bourbaki: MDP Autogenerati e Condizionati agli Obiettivi per la Dimostrazione di Teoremi

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

July 3, 2025

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

cs.AI

Abstract

Il ragionamento rimane un compito impegnativo per i grandi modelli linguistici (LLM), specialmente nell'ambiente logicamente vincolato della dimostrazione automatica di teoremi (ATP), a causa delle ricompense sparse e della vasta scala delle dimostrazioni. Queste sfide sono amplificate in benchmark come PutnamBench, che contiene problemi di livello universitario che richiedono un ragionamento complesso e multi-step. Per affrontare questo problema, introduciamo gli MDP condizionati da obiettivi auto-generati (sG-MDP), un nuovo framework in cui gli agenti generano e perseguono i loro sotto-obiettivi in base allo stato evolutivo della dimostrazione. Grazie a questa generazione più strutturata di obiettivi, il problema risultante diventa più adatto alla ricerca. Applichiamo quindi algoritmi simili al Monte Carlo Tree Search (MCTS) per risolvere gli sG-MDP, implementando il nostro approccio in Bourbaki (7B), un sistema modulare che può combinare più LLM da 7B per la generazione di sotto-obiettivi e la sintesi di tattiche. Su PutnamBench, Bourbaki (7B) risolve 26 problemi, raggiungendo nuovi risultati all'avanguardia per modelli di questa scala.

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.