Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916824455577600 |
|---|---|
| author | Zimmer, Matthieu Ji, Xiaotong Tutunov, Rasul Bordg, Anthony Wang, Jun Ammar, Haitham Bou |
| author_facet | Zimmer, Matthieu Ji, Xiaotong Tutunov, Rasul Bordg, Anthony Wang, Jun Ammar, Haitham Bou |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_02726 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving Zimmer, Matthieu Ji, Xiaotong Tutunov, Rasul Bordg, Anthony Wang, Jun Ammar, Haitham Bou Artificial Intelligence Machine Learning 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. |
| title | Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving |
| topic | Artificial Intelligence Machine Learning |
| url | https://arxiv.org/abs/2507.02726 |