Bourbaki: Selbstgenerierte und zielbedingte MDPs für den Beweis von Theoremen

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

July 3, 2025

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

cs.AI

Zusammenfassung

Das logische Schließen bleibt eine herausfordernde Aufgabe für große Sprachmodelle (LLMs), insbesondere in der logisch eingeschränkten Umgebung des automatisierten Theorembeweises (ATP), aufgrund von spärlichen Belohnungen und der enormen Komplexität von Beweisen. Diese Herausforderungen werden in Benchmarks wie PutnamBench noch verstärkt, die universitätsrelevante Probleme enthalten, die komplexes, mehrstufiges Denken erfordern. Um dies zu bewältigen, führen wir selbstgenerierte zielbedingte Markov-Entscheidungsprozesse (sG-MDPs) ein, ein neues Framework, in dem Agenten ihre Teilziele basierend auf dem sich entwickelnden Beweisstatus generieren und verfolgen. Durch diese strukturiertere Generierung von Zielen wird das resultierende Problem besser für die Suche geeignet. Anschließend wenden wir Monte-Carlo-Baumsuchalgorithmen (MCTS) an, um das sG-MDP zu lösen, und implementieren unseren Ansatz in Bourbaki (7B), einem modularen System, das mehrere 7B-LLMs für die Generierung von Teilzielen und die Synthese von Taktiken kombinieren kann. Auf PutnamBench löst Bourbaki (7B) 26 Probleme und erzielt damit neue state-of-the-art Ergebnisse mit Modellen dieser Größenordnung.

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.