{"id":"bc13c47f-4b37-4e56-a35e-579206bfc1c6","arxiv_id":"2507.02726","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"Bourbaki (7B), an MCTS-based system with self-generated subgoal rewards, solves 26/658 PutnamBench problems, beating the prior 7B best of 23 at a larger sample budget.","lead":"A theorem-proving system that lets AI models create their own intermediate lemmas inside Lean solves 26 Putnam competition problems, a new record for 7-billion-parameter models. The system, Bourbaki, combines two open 7B models with tree search and gives the model a reward whenever a self-proposed subgoal is proved.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Missing ensemble/no-search control means the sG-MDP+MCTS gain is unsubstantiated, and comparing 512 MCTS iterations to pass@1024 is not a matched sample budget.","rationale":"The paper is a plausible and honestly written preprint: the sG-MDP formalism is a coherent repackaging of goal-conditioned RL with dynamically generated subgoals, the implementation details are mostly clear, and the authors openly flag the heuristic-tactic soundness question and the benchmark version mismatch. The main empirical claim, however, is that the sG-MDP formulation plus MCTS with subgoal rewards yields more completed Lean proofs per sample than the base models. For that claim to hold, the search wrapper must be responsible for the improvement. The paper never runs the critical ablation: the same two base models in a simple ensemble without Bourbaki's MCTS and subgoal generation, at the same total number of model calls. Since Bourbaki's policy is an ensemble of DeepSeek-Prover-v2-7B and Kimina-7B, its 26 solved problems could be the union of what those two models already produce when given enough whole-proof samples. The paper attempts to preempt this by noting that some solved theorems are not found at pass@1024 by the base models, but that comparison is against single models, not the ensemble, and it is not matched in compute. The sample-budget issue compounds the problem: Table 1 lists Bourbaki's budget as 512, but the Section 4 setup says each MCTS iteration may try up to N=10 tactic candidates, so '512 iterations' is not equivalent to 512 whole-proof samples, nor to DeepSeek-Prover-V2's 1024 samples. Thus the 'more proofs with fewer samples' statement is not established by the reported numbers. The reader's weakest assumption already flags the two-model ensemble and the small single-run margin as possible artifacts, so our concern is closely related but more specific: it isolates the missing control that would settle whether the method itself does anything. Because the correct response is to require that control plus code release and error bars before accepting the SOTA claim, the reader's CONDITIONAL verdict remains appropriate; hence UNCHANGED.","tokens_in":9582,"tokens_out":6080,"duration_ms":71837,"concrete_test":"Run a no-search ensemble control on the identical 658-problem version: use the same two base models (DeepSeek-Prover-v2-7B and Kimina-7B) in the same Lean/PyPantograph environment, generate whole-proof samples with the same total number of policy-model calls actually consumed by Bourbaki's 512 iterations (or at least 512 samples per model), and take the union of type-checked proofs. If this ensemble baseline reaches 26/658 or more, the sG-MDP/MCTS wrapper is not the cause of the reported gain and the SOTA/sample-efficiency claims collapse. If the ensemble baseline is clearly below 26, additionally rerun Bourbaki at least 5 times to estimate run-to-run variance and compare against DeepSeek-Prover-V2 pass@1024 on exactly the same problem set.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim has two parts: (i) the sG-MDP formulation plus MCTS yields more proofs per sample than the base models, and (ii) 26/658 is a 7B state of the art. The first part is not supported because no control removes the search wrapper while keeping the exact same two-model ensemble. Bourbaki (7B) ensembles DeepSeek-Prover-v2-7B and Kimina-7B (Section 1), but Table 1 compares against these models individually. If the 26 solved theorems are simply the union of each base model's best whole-proof generations, the entire contribution reduces to ensembling plus extra sampling. The paper's claim that 'some new theorems at pass@512 are not found at pass@1024 using the base models' is not a substitute for this control, since the base models were not run as an ensemble and not at matched compute. Second, the 'sample budget' column is not a matched budget. Section 4 sets K=512 iterations and N=10 tactic candidates per node; an MCTS iteration can consume many model calls, and heuristic tactics (e.g., apply?) are finished by a base-model completion. Comparing this to pass@1024 whole-proof generations in Table 1 overstates sample efficiency; Table 2's '128 vs 128' comparison has the same unit problem. The benchmark version footnote (644 vs 658) and the absence of repeated runs/error bars further weaken the SOTA margin (26 vs 23), but the missing ensemble control is the load-bearing issue: without it, no empirical claim about goal-conditioned subgoal search is established.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces self-generated goal-conditioned MDPs (sG-MDPs), a formalism for theorem proving in which an LLM proposes subgoals during proof search, and applies MCTS-like search with rewards derived from Lean verification and solved conjectures. The system, Bourbaki (7B), ensembles DeepSeek-Prover-v2-7B and Kimina-7B and is evaluated on PutnamBench. The authors report 26/658 solved problems at an MCTS budget of 512, claiming a new 7B state of the art and improved sample efficiency over whole-proof baselines, plus additional improvements when wrapping STP and DeepSeek-Prover-v2.","tokens_in":9916,"tokens_out":7199,"duration_ms":71504,"significance":"If the empirical claims were properly controlled, the sG-MDP formalism and the verifier-based subgoal reward could be a useful framework for dense reward in neural theorem proving. The use of Lean verification instead of a learned critic is an attractive simplification, and the modular ensembling design is a strength. However, the current evidence does not support the causal claim that goal-conditioned search, rather than ensembling or additional model calls, produces the improvement. The single-run, small-margin headline result and the mixed benchmark denominators further limit confidence. The contribution is therefore potentially significant but not yet substantiated.","major_comments":[{"comment":"The headline comparison lacks an ensemble/no-search control. Bourbaki (7B) is built by ensembling DeepSeek-Prover-v2-7B and Kimina-7B (Section 1), but Table 1 compares Bourbaki against these models individually. Without a control that runs the same two-model ensemble under whole-proof generation, the 26/658 result cannot be attributed to sG-MDP goal-conditioned search; it may simply be the union of the base models' best whole-proof generations plus extra sampling. The observation that 'some new theorems at pass@512 are not found at pass@1024 using the base models' does not replace this control, because the base models were not run as an ensemble and not at a matched budget.","section":"Section 4, Table 1"},{"comment":"The 'sample budget' is not a matched comparison. Each of K=512 MCTS iterations consumes multiple LLM calls: tactic sampling with N=10 candidates, subgoal proposal, and, for heuristic tactics such as apply?, a full base-model completion (as stated in the Implementation Details). Comparing this to pass@1024 whole-proof generations in Table 1, or to pass@64/128 in Table 2, therefore does not establish sample efficiency. The paper should report a common unit such as total LLM calls or model-compute-equivalent samples.","section":"Section 4, Tables 1 and 2"},{"comment":"The headline margin is a single run with no error bars. Bourbaki solves 26/658 versus DeepSeek-Prover-v2's 23/658; with no repeated seeds or variance estimates, a 3-problem difference cannot be distinguished from run-to-run noise. The table also mixes benchmark versions: the footnote states that some prior results used the 644-problem version, but the table's denominators are 644 and 658 (e.g., Kimina 10/644 vs Bourbaki 26/658). The comparison should be made on a single frozen version with confidence estimates.","section":"Section 4, Table 1"},{"comment":"The handling of heuristic tactics through a fallback base-model completion is a potential confound. The paper states that tactics such as apply? are finished by 'the plain base model to complete the remainder of the proof.' If many of the 26 solved proofs are completed by this fallback, the improvement may come from the base model rather than from sG-MDP search. The authors should report how many solved proofs required the fallback and verify that the claimed gains survive when the fallback is omitted or separately ablated.","section":"Section 4, Implementation Details"},{"comment":"The objective used in the experiments is underspecified. Equation (1) defines the reward as R(st, ¯g0) + λ R(st, ¯gt), but Section 3.2 states that the initial value of a node is R(st, ¯gt) and backpropagation uses R(st, ¯gt), and the Implementation Details say the value is 'a combination of depth-based metrics and the number of solved conjectures' without giving the formula. The paper should specify the exact reward and value-update equations used to produce Tables 1 and 2.","section":"Section 3.2 and Eq. (1)"}],"minor_comments":[{"comment":"The statement that Kimina-7B is the previous 7B state of the art with 10/644 should be reconciled with the 658-problem version of the benchmark; the caption should state the version for every row.","section":"Section 1 and Table 1"},{"comment":"The definitions of IsGoal, ToGoal, and Solves overlap with the reward function; it is also unclear what happens to the transition when RemoveLast is applied to an empty goal stack.","section":"Section 3.1"},{"comment":"The term pass@k is used for the MCTS system, but k is not defined in that context; the authors should state explicitly whether k counts MCTS iterations, expanded nodes, or LLM calls.","section":"Section 4"},{"comment":"The notation is inconsistent: the text refers to both 'DeepSeek-V2-7B' and 'DeepSeek-Prover-v2-7B' for the same model.","section":"Section 4"},{"comment":"The related-work paragraph on MCTS contains citation and punctuation errors, for example 'AlphaProof (2024); Xin et al. (2024). (Han et al., 2022)', which should be corrected.","section":"Related Work"}],"recommendation":"major_revision","confidential_remarks":"The empirical attribution is the main risk: the missing ensemble/no-search control and the unmatched sample budgets are load-bearing for the paper's central claims. If the authors add the requested controls and the margin persists, the contribution would be of value to the theorem-proving community. The theoretical sG-MDP part is light, so the paper should be evaluated primarily as an empirical systems contribution."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The thing to know: Bourbaki is a real, buildable idea — generate subgoals as Lean 'have' statements, verify them during MCTS, and use that as dense reward. That is worth reading. But the headline comparison is shakier than it looks: the 26/658 vs 23/658 margin is a single run, the sample-budget column mixes units, and there is no control that isolates the search wrapper from the two-model ensemble.\n\nWhat's genuinely new is the sG-MDP framing and the reward from verified conjectures rather than a learned critic. The implementation is described cleanly: Pantograph, Lean 4, vLLM, N=10, K=512, and an honest footnote about the 644 vs 658 benchmark versions. Table 2 is the most useful evidence: applying the wrapper to STP and to DeepSeek-Prover-v2 as single base models gives 7 vs 6, 8 vs 7, and 23 vs 15 at 128. That suggests the subgoal mechanism itself does something, not just ensembling.\n\nThe soft spots are real. The load-bearing one is that 'sample budget' isn't a matched budget. An MCTS iteration can call the model many times: up to N tactic candidates plus a completion step for heuristic tactics like apply?. Comparing K=512 iterations to pass@1024 whole-proof generations overstates sample efficiency, and Table 2's '128 vs 128' has the same unit problem. So the paper's claim that the method 'completes more proofs with fewer samples' is not established. Second, there is no ensemble-only control; part of the 26 could be the union of each base model's best whole-proof generations. Table 2 mitigates this for single models, but not with matched units. Third, single run, no error bars; 26 vs 23 is three problems, within plausible noise. Fourth, no code release.\n\nNone of this kills the idea. The sG-MDP formulation is a reasonable way to think about subgoal-conditioned search, and the verified-conjecture reward is a nice alternative to learned critics. But the empirical claims need version-matched, budget-matched controls, repeated runs, and code before I'd call it SOTA.\n\nWho is this for? Researchers working on LLM-based theorem proving and anyone interested in search wrappers over small open models. It deserves a serious referee — the idea is worth building on and the authors are transparent about known limitations — but the review should demand the missing controls.\n\nRecommendation: send to peer review, but expect revision.","headline":"A promising wrapper over 7B provers with a genuine subgoal-search idea, but the headline SOTA claim rests on unmatched budgets and a missing ensemble control.","tokens_in":10499,"tokens_out":3616,"would_cite":false,"duration_ms":37627,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"By generating and verifying its own intermediate lemmas during search, a 7B-parameter system solves 26 PutnamBench problems, a new best at that scale.","keywords":["self-generated goal-conditioned MDP","automated theorem proving","Lean 4","Monte Carlo Tree Search","PutnamBench","subgoal decomposition","sample efficiency","large language models"],"falsifier":"Repeat Bourbaki's PutnamBench evaluation on the fixed 658-problem version with several random seeds, and also run the same two base models under the same MCTS but with the conjecture-reward term disabled; if a fresh Bourbaki run scores 23 or below, or if removing the subgoal reward leaves the solved count unchanged, the central claim fails.","tokens_in":9373,"feed_emoji":"🧩","tokens_out":7390,"duration_ms":75880,"temperature":0.7,"pith_summary":"The paper sets out to show that the sparse-reward problem in formal theorem proving can be attacked by letting the proof agent generate its own subgoals during search, and that this yields a new state of the art at the 7-billion-parameter scale. It formalizes this as a self-generated goal-conditioned MDP (sG-MDP), where the agent may create a Lean conjecture at any point and is rewarded when such conjectures are independently verified. Its instantiation, Bourbaki (7B), combines two 7B LLMs with an MCTS-style search over a stack of goals, and reports solving 26 of 658 PutnamBench problems at pass@512, beating previous 7B/8B results that used larger sample budgets. If the result holds, smaller models become a practical route to competition-level formal proofs.","feed_headline":"Self-made subgoals push 7B prover to 26 Putnam proofs","feed_subtitle":"A new search framework with self-generated lemmas sets a 7B-scale best on PutnamBench.","key_machinery":"The central object is the self-generated goal-conditioned MDP (sG-MDP), a goal-conditioned MDP augmented with a goal stack: an action can either be a primitive Lean tactic or a newly proposed conjecture, where primitive actions only transition the proof state when they solve the top goal, and proposing a conjecture pushes that conjecture onto the stack. The search machinery is an MCTS variant whose node value is initialized by a reward combining progress on the original goal with progress on generated subgoals, and whose selection uses UCB over the empirical mean; PyPantograph validates tactics and verifies goals and subgoals inside Lean 4. The key work is that the reward becomes denser while remaining grounded in verifier feedback, so the search does not need a learned critic.","core_discovery":"On its own terms, the paper's discovery is that a theorem-prover can profitably treat intermediate lemmas as actions: instead of a preset goal distribution, the transition function lets the agent push a newly proposed conjecture onto a goal stack and then use every primitive tactic as an attempt to solve the top goal. MCTS then explores this state-goal graph, and the value of a node is computed entirely from verified outcomes—how many locally introduced conjectures were confirmed and how far the proof advanced—rather than from a learned critic. The authors report that this enabled their ensemble Bourbaki (7B) to solve 26/658 PutnamBench problems at pass@512, compared with 23/658 for DeepSeek-Prover-V2 at a larger sample budget and 10/644 for Kimina-7B, and that applying the wrapper to STP and DeepSeek-Prover-V2 produced additional solved theorems at matched budgets. They interpret this as evidence that self-generated subgoals make proof search more sample-efficient and more diverse.","pith_inferences":["In my reading, the reported gain over the previous best is a 3-problem margin from a single run with no reported variance, so the state-of-the-art claim should be treated as provisional until reproduced across seeds on a fixed benchmark version.","The mechanism predicts a testable scaling pattern: the advantage over whole-proof sampling should be largest on problems that admit a useful intermediate 'have' step, and should shrink on problems with a flat proof structure.","The same formulation could be lifted to other tactic-based proof assistants, such as Isabelle or Coq, wherever a verifier interface analogous to PyPantograph can expose goal states and conjecture validation.","Because the value signal comes from verifier feedback, training an RL policy directly on the sG-MDP rewards, as the paper notes is possible, could convert the search-time gains into one-shot model capabilities without new proof corpora."],"forward_implications":["At the 7B-8B scale, search with self-generated subgoals completes more PutnamBench proofs than prior whole-proof and tree-search baselines, including models that used larger sample budgets.","Wrapping an existing prover in the sG-MDP framework yields extra completed proofs at the same sample budget: STP goes from 6 to 7 at pass@64 and 7 to 8 at pass@128, while DeepSeek-Prover-V2 goes from 15 to 23 at pass@128.","Subgoal generation supplies a denser, verifier-based reward signal that can replace or complement learned critics in MCTS-based theorem proving.","The framework is modular: as long as a policy can emit valid Lean conjectures and tactics, other base models can be ensembled or swapped in.","Because the rewards are computed from Lean verification alone, the proof fragments counted by the search are machine-checked rather than merely plausible."],"supporting_citations":[{"why":"Supplies PyPantograph, the Lean 4 interface used to validate tactics and verify goals and subgoals at every search step.","marker":"Aniva et al., 2025"},{"why":"Provides the PutnamBench dataset and leaderboard that define the evaluation task and the previous 7B result the paper seeks to beat.","marker":"Tsoukalas et al., 2024"},{"why":"DeepSeek-Prover-V2 is both an ensemble member of Bourbaki and the strongest reported 7B baseline at 23/658.","marker":"Ren et al., 2025"},{"why":"Kimina-7B is the other ensemble member and the prior 7B leaderboard state of the art at 10/644.","marker":"Wang et al., 2025"},{"why":"STP serves as the base prover for the matched-budget sample-efficiency experiments.","marker":"Dong & Ma, 2025"},{"why":"Provides the goal-conditioned reinforcement-learning formulation that the sG-MDP extends.","marker":"Schaul et al., 2015"}],"fun_headline_variants":["Self-generated goals let 7B LLM prove 26 PutnamBench challenges","7B prover learns to generate its own subgoals, cracks 26 Putnam problems","Bourbaki: self-made lemmas help 7B solver hit 26 Putnam problems","Goal-conditioned MDPs lift 7B prover to 26 Putnam solves"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The comparison that makes the claim a new state of the art assumes that one run scoring 26/658 genuinely beats 23/658 on the same fixed problem set, rather than reflecting the benchmark's version change, the two-model ensemble, or run-to-run variance.","fun_headline_variants_meta":{"raw":{"variants":["Self-generated goals let 7B LLM prove 26 PutnamBench challenges","7B prover learns to generate its own subgoals, cracks 26 Putnam problems","Bourbaki: self-made lemmas help 7B solver hit 26 Putnam problems","Goal-conditioned MDPs lift 7B prover to 26 Putnam solves"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001126,"raw_usage":{"total_tokens":4678,"prompt_tokens":934,"completion_tokens":3744,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":550,"completion_tokens_details":{"reasoning_tokens":3652}},"tokens_in":550,"tokens_out":3744,"duration_ms":25232,"temperature":1.0,"reasoning_tokens":3652,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T20:22:18.987794+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Repeat Bourbaki's PutnamBench evaluation on the fixed 658-problem version with several random seeds, and also run the same two base models under the same MCTS but with the conjecture-reward term disabled; if a fresh Bourbaki run scores 23 or below, or if removing the subgoal reward leaves the solved count unchanged, the central claim fails.","supporting_citations":[{"cited_title":"Pantograph: A machine-to-machine interaction interface for advanced theorem proving, high level reasoning, and data extraction in lean 4","cited_arxiv_id":null,"evidence_quote":"Supplies PyPantograph, the Lean 4 interface used to validate tactics and verify goals and subgoals at every search step."},{"cited_title":"Putnambench: A multilingual competition-mathematics benchmark for formal theorem-proving","cited_arxiv_id":null,"evidence_quote":"Provides the PutnamBench dataset and leaderboard that define the evaluation task and the previous 7B result the paper seeks to beat."},{"cited_title":"Stp: Self-play llm theorem provers with iterative conjecturing and proving","cited_arxiv_id":null,"evidence_quote":"STP serves as the base prover for the matched-budget sample-efficiency experiments."},{"cited_title":"Universal value function approximators","cited_arxiv_id":null,"evidence_quote":"Provides the goal-conditioned reinforcement-learning formulation that the sG-MDP extends."}],"review_version":1}