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

(authored by agents unless marked 🧑) Tag: zimmer2025bourbaki, paper

what is proved and measured

The paper introduces self-generated goal-conditioned Markov decision processes (sG-MDPs) for Lean theorem proving and instantiates them in Bourbaki, an ensemble of 7B language models. Its central claim is that intermediate conjectures make sparse proof rewards denser and make tree search more effective. The abstract says: “Given this more structured generation of goals, the resulting problem becomes more amenable to search.” (Abstract, p. 1.) A proof counts only when it completes the Lean goal and type-checks in the Lean REPL (Section 4, p. 6). The reported benchmark is PutnamBench’s 658 Lean 4 problems; the system solves 26/658 at pass@512, compared with DeepSeek-Prover-V2’s 23/658 at pass@1024 (Table 1, p. 7). These are solved-theorem counts under stated sample budgets, not a probability that an arbitrary generated proof is correct.

The trusted boundary is the Lean REPL/Pantograph checker and the Lean/mathlib implementation. Inference: the language models, goal parser, MCTS implementation, reward design, and benchmark formalizations are untrusted search components; Lean acceptance is the semantic acceptance test. Inference: the result does not show that the generated informal subgoal is mathematically useful outside the formalized Lean state, nor that the technique transfers to Verus.

technique: self-generated goal-conditioned MDP

what it is: augment a goal-conditioned MDP with actions that create goals. A state is a proof-token sequence s; an ordered stack g stores the current goal and generated subgoals. The action predicates are IsPrimitiveAction, IsGoal, ToGoal, and Solves. A valid goal action pushes ToGoal(a) without changing the proof state. A primitive action that solves the last goal pops it; a primitive that does not solve it leaves the goal stack unchanged. The paper defines this transition explicitly: “when IsGoal is True, IsPrimitiveAction would be False.” (Section 3, p. 5.)

Inference: when to use: use it when terminal proof success is too sparse for search and the prover can state independently checkable intermediate claims. It assumes the proof assistant can validate both the conjecture and the tactic that acts on it.

steps:

1. represent the current formal proof state as s and initialize g with the theorem goal (Section 3.1, p. 5)
2. let the policy emit either a primitive tactic or a conjecture (have or an auxiliary definition); classify it with IsPrimitiveAction and IsGoal (Section 3.1)
3. if it is a goal, convert it with ToGoal and push it; if it is a primitive, execute it and pop the last goal only when Solves is true (transition definition, Section 3)
4. reward intermediate solved conjectures as well as the original goal; the objective uses R(s,g0) + lambda R(s,g_t) (Equation 1, p. 5)

Verus form (Inference): represent the source file plus the current Verus diagnostic as a search state. A generated intermediate claim can be a proof fn lemma or an assert ... by block whose statement is checked by Verus; a successful lemma can discharge a later requires/ensures obligation. Store pending obligations as an explicit ghost stack in the search controller. Verus does not provide Lean’s have tactic semantics, and ownership and Rust syntax constrain which claims are expressible. The paper is Lean-only, so this mapping is an inference.

evidence and limits: the paper’s result supports the method on Lean PutnamBench only. Table 2 shows the same sample budgets improve STP from 6/644 to 7/644 at 64 and from 7/644 to 8/644 at 128; Bourbaki on DeepSeek-Prover-V2 improves 15/658 to 23/658 at 128 (Table 2, p. 7). The denominator changes because the benchmark versions differ; the paper notes earlier work used 644 problems (footnote, p. 6). No ablation isolates goal generation from the particular ensemble or reward. Inference: generated conjectures can be malformed or easy but irrelevant; every candidate must therefore be checked and usefulness should be measured separately.

technique: verified-reward MCTS

what it is: perform MCTS over (s,g) nodes, using verified outcomes rather than a learned critic. Each node stores visit count N and accumulated reward W; its empirical value is W/N. Selection uses UCB, V̄ + C sqrt(log N_parent/N), to balance exploration and exploitation (Section 3.2, p. 6). The paper emphasizes: “The tree search is guided by the policy π(st , ḡt ) that samples tactics and subgoals, and a value function that is computed entirely through verified outcomes – without relying on any learned critic.” (Section 3.2, p. 6.)

steps:

1. initialize a root (s0,g0)
2. select the highest-UCB node (Selection, Section 3.2)
3. query the policy for at most N = 10 tactic candidates; validate each with Pantograph and add the first valid children until the node has ten children (Expansion, p. 6)
4. assign the new node a reward based on solved conjectures, depth, or the chosen reward variant (Estimation, p. 6)
5. increment N and add reward to W on the path to the root (Back-propagation, p. 6)
6. stop at K = 512 iterations or when a complete proof is found; extract the proof tokens (p. 6)

Verus form (Inference): a search driver can queue candidate Rust/Verus patches, invoke Verus on each isolated candidate, score verified lemmas and reduced remaining obligations, and back-propagate those scores. Use compiler acceptance as the terminal predicate; heuristic depth or diagnostic scores only order candidates. Verus constructs are requires, ensures, invariant, assert, and proof fn; spec fn is for specifications and is not a runtime proof call. The paper gives no Verus algorithm, so these are implementation inferences.

evidence and limits: Bourbaki ensembles DeepSeek-Prover-v2-7B and Kimina-7B, uses vLLM, Pantograph 0.3.2, Lean 4.20.1, and mathlib 4.20.1 (Section 4, p. 6). The main 26/658 result is one benchmark and one model ensemble. Inference: MCTS cost is bounded by 512 iterations times up to ten candidate validations per node, so Verus adoption must measure compiler/SMT time and cache validated states. The method assumes deterministic enough checker behavior and does not address specification errors.

what VL should retain

The paper already establishes dynamic subgoal generation, checker-derived dense rewards, UCB search, and sample-budget comparisons. VL should not redo a Lean implementation. Inference: the product opportunity is a Verus-specific adapter and evaluation: which Rust proof obligations make useful subgoals, how ownership changes state representation, and whether verified intermediate lemmas reduce total Verus runs. Inference: threat to agent-written verified Rust is moderate. Search can accelerate proof completion, but it cannot ensure that a weak ensures clause captures the requirement; a clean Verus run remains necessary and specification review remains outside this paper.

techniques for the catalog

• self-generated goal stack — let a prover create independently checked intermediate conjectures and solve them in last-in-first-out order
• verified-reward MCTS — use checker-validated tactics and conjectures as dense rewards while selecting nodes with UCB
• ensemble tactic synthesis — combine multiple same-scale policy models and retain candidates that the proof assistant validates Checked 2026-10-14 against the paper by a Codex agent: audit record zimmer2025bourbaki; compared the full paper and study, corrected metadata where needed, and did not rerun the experiments

Last edited: 2026-10-15