Bourbaki: Zelfgegenereerde en Doelgerichte MDP's voor Stellingen Bewijzen

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

Samenvatting

Redeneren blijft een uitdagende taak voor grote taalmodellen (LLMs), vooral binnen de logisch beperkte omgeving van automatisch theorema bewijzen (ATP), vanwege schaarse beloningen en de enorme omvang van bewijzen. Deze uitdagingen worden versterkt in benchmarks zoals PutnamBench, die universiteitsniveau problemen bevatten die complexe, meerstaps redenering vereisen. Om dit aan te pakken, introduceren we zelf gegenereerde doel-conditie MDPs (sG-MDPs), een nieuw raamwerk waarin agenten hun subdoelen genereren en nastreven op basis van de evoluerende bewijsstaat. Door deze meer gestructureerde generatie van doelen wordt het resulterende probleem beter geschikt voor zoekalgoritmen. Vervolgens passen we Monte Carlo Tree Search (MCTS)-achtige algoritmen toe om de sG-MDP op te lossen, waarbij we onze aanpak implementeren in Bourbaki (7B), een modulair systeem dat meerdere 7B LLMs kan samenbrengen voor subdoelgeneratie en tactieksynthese. Op PutnamBench lost Bourbaki (7B) 26 problemen op, waarmee het nieuwe state-of-the-art resultaten behaalt met modellen van deze schaal.

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.