Bourbaki : MDP auto-générés et conditionnés par des objectifs pour la démonstration de théorèmes

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

July 3, 2025

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

cs.AI

Résumé

Le raisonnement reste une tâche complexe pour les grands modèles de langage (LLMs), en particulier dans l'environnement logiquement contraint de la démonstration automatique de théorèmes (ATP), en raison des récompenses rares et de l'échelle considérable des preuves. Ces défis sont amplifiés dans des benchmarks comme PutnamBench, qui contient des problèmes de niveau universitaire nécessitant un raisonnement complexe et multi-étapes. Pour y remédier, nous introduisons les MDPs (Markov Decision Processes) auto-générés conditionnés par des objectifs (sG-MDPs), un nouveau cadre dans lequel les agents génèrent et poursuivent leurs sous-objectifs en fonction de l'état évolutif de la preuve. Grâce à cette génération plus structurée d'objectifs, le problème résultant devient plus accessible à la recherche. Nous appliquons ensuite des algorithmes similaires à la recherche arborescente Monte Carlo (MCTS) pour résoudre les sG-MDPs, en instanciant notre approche dans Bourbaki (7B), un système modulaire capable de combiner plusieurs LLMs de 7B pour la génération de sous-objectifs et la synthèse de tactiques. Sur PutnamBench, Bourbaki (7B) résout 26 problèmes, établissant de nouveaux résultats de pointe pour des modèles de cette échelle.

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.