mlsanityData to 14 Oct 2026

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

arXiv 2507.02726 ↗First posted 3 Jul 2025cs.AI cs.LGcited by 12

On the map: Synthetic data and self-improvement for LLMs → Self-play RL for reasoning

Abstract (arXiv)

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.

Key facts. Cited by 12 papers in the map (data through 14 Oct 2026). Placed in Self-play RL for reasoning, one of 13 directions in Synthetic data and self-improvement for LLMs. Builds on 7 of its 16 references that are in the map. First posted on arXiv 3 Jul 2025.

Builds on

7 of 16 references.

Closest ancestors · 1

Same direction, newest first

  1. 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving31 Jan

Other references · 6

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  2. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 287
  3. 2025Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learningcited by 180
  4. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  5. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  6. 2024Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4cited by 18

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 1; 2026: 11.

12 papers.

  1. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
  2. 2026Scalable Power Sampling: Unlocking Efficient, Training-Free Reasoning for LLMs via Distribution Sharpeningcited by 31
  3. 2026A Minimal Agent for Automated Theorem Provingcited by 18
  4. 2026OProver: A Unified Framework for Agentic Formal Theorem Provingcited by 7
  5. 2026The Y-Combinator for LLMs: Solving Long-Context Rot with λ-Calculuscited by 3
  6. 2026Decoding as Optimisation on the Probability Simplex: From Top-K to Top-P (Nucleus) to Best-of-K Samplerscited by 2
  7. 2026Why Agentic Theorem Prover Works: A Statistical Provability Theory of Mathematical Reasoning Modelscited by 1
  8. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  9. 2026The Topological Dual of a Dataset: A Logic-to-Topology Encoding for AlphaGeometry-Style Datacited by 0
  10. 2026Self-Supervised Theorem Discovery in a Formal Axiomatic Systemcited by 0
  11. 2026iSDFT: Information-Proximal Self-Distillation for Continual Learning in LLMscited by 0
  12. 2026A Critical Look at Power Sampling when Test Time Sharpening LLMscited by 0

Similar, not cited

Close in wording, no citation either way

  1. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation
  2. 2026Reward-Oracle MCTS for Formal Theorem Proving: Sample-Efficient Search and the Need for Kernel-Level Proof Auditing
  3. 2025Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving
  4. 2025Scaling up Multi-Turn Off-Policy RL and Multi-Agent Tree Search for LLM Step-Provers
  5. 2025BFS-Prover: Scalable Best-First Tree Search for LLM-based Automatic Theorem Proving
  6. 2026On Reasoning-Centric LLM-based Automated Theorem Proving
  7. 2025LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
  8. 2026Direct Optimization of Generators for Search in Automated Theorem Proving