{"id":"ae5d06a7-6859-4611-ab5f-ddc538f5bc41","arxiv_id":"2505.12031","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":15,"one_line_summary":"A tree-search theorem prover trained on synthetic proof-state exploration data reaches 60.74% Pass@1 on MiniF2F and 21.18% on ProofNet using an adaptive beam size.","lead":"This paper teaches a 7B LLM to prove math theorems in Lean 4 by first exploring many intermediate proof states to create training data, then fine-tuning on that data. Adding an adaptive beam size during search lifts its pass rate to 60.74% on MiniF2F and 21.18% on ProofNet, ahead of the tree-search baselines they compare against.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Table 1's Pass@1 comparison mixes unequal total tactic-generation budgets, so the adaptive gains may be a compute artifact rather than a method effect.","rationale":"The reader's stated weakest assumption (sufficiency of the 60-tactic set T) is real but not the most load-bearing issue: the final model is additionally trained on Mathlib human-authored proofs, so it is not strictly confined to T at inference, and the exploration data is only one component of the training corpus. The more decisive weakness is that the central numerical claim, the Pass@1 comparison in Table 1, is not controlled for total compute. The paper fixes E=600 but varies beam size between methods and over the course of the adaptive search, so 'same computational budget' is not satisfied under the paper's own K×B×E accounting. Moreover, the adaptive hyperparameters are tuned per benchmark without a validation split, making the reported adaptive gains vulnerable to selection on the test set. These concerns do not require doubting the released code or the reported numbers; they require additional controlled experiments. The paper has genuine strengths: the method is concrete, the implementation and model are released, and the fixed-beam results at least show plausibility. But as it stands, the evidence does not uniquely support the causal claim that scalable synthetic data generation drives the improvement. The reader's CONDITIONAL verdict is therefore the right disposition, and my read does not call for a different verdict.","tokens_in":17273,"tokens_out":10066,"duration_ms":117139,"concrete_test":"Re-run BFS-Prover, InternLM2.5-StepProver, and the proposed method under a fixed total number of tactic generations: for each method, set E so that the integrated beam count (sum of beam sizes over expansions) equals the same constant, for example 6,000 tactic generations per theorem, and choose all beam and decay hyperparameters on the MiniF2F validation split and a ProofNet training split rather than on the test sets. If the proposed adaptive method no longer surpasses the baselines under this equal-generation budget, the headline Pass@1 comparison in Table 1 is a budget artifact and the central claim would need to be weakened.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The headline empirical claim is not established because the comparison in Table 1 is not budget-equivalent under the paper's own K×B×E accounting. The baselines are run at their original beam sizes: BFS-Prover uses B=2 and InternLM2.5-StepProver uses B=32, both with E=600, giving 1,200 and 19,200 tactic generations per theorem, respectively. The adaptive schedules in Appendix A.4 use different per-benchmark beam sizes: MiniF2F (Bmax=16, Bmin=4, λ=15) spends roughly 2,600 tactic generations, about 2.2 times BFS-Prover's budget, while ProofNet (Bmax=48, Bmin=24, λ=2) spends roughly 18,000 tactic generations. Thus the reported deltas (60.74% vs 55.49% on MiniF2F, and 21.18% vs 19.89% on ProofNet) are confounded by total search effort. The problem is compounded by the fact that the adaptive beam hyperparameters were selected separately for each benchmark without a held-out validation split, which amounts to test-set tuning of the most performance-sensitive hyperparameter identified in Section 4.3. A reader cannot tell whether the improvement comes from proof-state exploration, from the adaptive strategy, or from simply spending a different amount of search compute.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a data synthesis pipeline called proof-state exploration for LLM-based automated theorem proving in Lean 4. Starting from seed problems in the STP dataset, the method uses constrained decoding over a curated set of 60 tactics, followed by premise completion and Lean verification, to generate a large corpus of intermediate proof-state transitions. The resulting data is used to fine-tune Qwen2.5-Math-7B, and at inference the paper proposes an adaptive beam size strategy that starts with a large beam and decays it as search progresses. The authors report Pass@1 averages of 60.74% on MiniF2F and 21.18% on ProofNet under K=1, E=600, claiming these results outperform the tree-search baselines InternLM2.5-StepProver and BFS-Prover. The paper also introduces the DoBeVi REPL and visualization tool and reports confidence intervals for the main results.","tokens_in":17622,"tokens_out":6156,"duration_ms":60921,"significance":"If the empirical claims are substantiated, the paper makes a useful contribution: it describes a concrete, reproducible data synthesis method that goes beyond Expert Iteration by collecting diverse intermediate proof states rather than only successful full proofs, and it releases code and a model checkpoint. The fixed-beam result of 59.51% on MiniF2F at B=8 is itself competitive with strong baselines, and the paper provides confidence intervals, which is good practice. The main scientific value is the demonstration that large-scale synthetic proof-state data can improve the policy model in a one-shot training pass. However, the paper's central attribution claim is currently under-supported because the headline comparison in Table 1 does not isolate the data synthesis contribution from differences in search effort, and the adaptive beam hyperparameters are selected on the test benchmarks.","major_comments":[{"comment":"The statement in Section 4.2 that baselines are evaluated under the same computational budget is not supported by the paper's own budget definition K×B×E. In Table 1, BFS-Prover at B=2 and E=600 spends 1,200 tactic generations per theorem; InternLM2.5-StepProver at B=32 and E=600 spends 19,200; Ours fixed at B=8 spends 4,800; the adaptive schedule for MiniF2F (Bmax=16, Bmin=4, λ=15) spends approximately 2,900; and the adaptive schedule for ProofNet (Bmax=48, Bmin=24, λ=2) spends approximately 18,000. Thus the reported deltas of +5.25 points over BFS-Prover on MiniF2F and +1.29 points over InternLM2.5-StepProver on ProofNet are confounded with total search effort. The paper should report matched-budget comparisons, for example by giving a pass-rate-vs-total-tactic-generations curve for all methods, or by fixing a single total budget and letting each method choose its beam configuration within that budget.","section":"Section 4.1/Table 1"},{"comment":"The adaptive beam hyperparameters Bmax, Bmin, and λ are set separately for MiniF2F and ProofNet, and the fixed beam sweep B∈{4,8,16,32} is also reported on the test sets, with no validation split defined. Because the adaptive schedule is tuned per benchmark after seeing test performance, the reported adaptive gains (60.74% vs 59.51% on MiniF2F, 21.18% vs 20.75% on ProofNet) may reflect test-set selection rather than a generally effective search strategy. The paper should specify a validation procedure, or report a single schedule chosen on a held-out set and then evaluated on both benchmarks, to make the adaptive strategy comparison meaningful.","section":"Section 4.2 and Appendix A.4"},{"comment":"The decontamination step is described only as using BLEU similarity to remove examples with high overlap with the evaluation benchmarks, but neither the BLEU threshold nor the number of removed examples is reported. Since the final training set comprises approximately 20 million proof transitions drawn from STP and Mathlib, and MiniF2F and ProofNet are small public benchmarks, this omission leaves open the possibility that the reported pass rates are inflated by near-duplicate training examples. The authors should report the decontamination threshold and the quantity of data removed, and ideally verify that no benchmark theorem or close paraphrase appears in the training set.","section":"Section 3.1 (post-processing)"},{"comment":"No ablation isolates the contribution of the proof-state exploration data synthesis. The comparison against InternLM2.5-StepProver and BFS-Prover changes the base model, the training data, and the search procedure simultaneously, so the superiority of 'Ours (fixed beam size)' does not establish that the synthetic exploration data is the cause of the improvement. A control experiment training the same base model on existing data (for example, STP-only data, or data obtained by rejection sampling on successful proofs) under the same search budget is needed to support the paper's central claim that scalable synthetic data generation is the decisive factor.","section":"Section 4.2 (experimental design)"},{"comment":"The 60-tactic set T is derived by frequency filtering on the STP dataset, but no coverage analysis is reported for MiniF2F or ProofNet. Because data synthesis uses constrained decoding over T, any tactic outside T will never appear in the synthetic training data, and the fine-tuned policy will have low probability of emitting it at inference. The paper asserts that such a curated set is sufficient for the vast majority of problems, but it does not provide evidence. The authors should report what fraction of human-written or baseline-generated proof steps on the two benchmarks use tactics from T, and discuss the resulting completeness limitation.","section":"Section 3.1 and Appendix A.6"}],"minor_comments":[{"comment":"There is a typo in Algorithm 1: 'lean_prvoer' should be 'lean_prover'.","section":"Algorithm 1"},{"comment":"The phrase 'same search budget' in Section 4.2 is ambiguous because the paper's own metric K×B×E includes the beam size B, which differs across rows; please replace it with an explicit statement of which quantities are fixed (K and E) and which are allowed to vary.","section":"Section 4.1"},{"comment":"In the example theorem statement 'amc12a_2009_p6', the type annotation '(m n p q : R) R' appears malformed; it should likely be a single type annotation for the variables.","section":"Appendix A.2"},{"comment":"The node terminology is inconsistent between the text ('Open Node', 'Error Node', 'ProofFinished Node') and the figure caption ('Internal', 'Proof', 'LeanError'); please unify the labels.","section":"Appendix A.3/Figure 3"},{"comment":"The sentence 'An fundamental cause is that LLMs are typically trained for general-purpose language understanding' contains a grammatical error ('An' should be 'A').","section":"Section 1"},{"comment":"Figure 5 includes a curve for B=2, but Table 1 does not report a fixed-beam result for B=2 for the proposed model; please clarify whether this configuration was evaluated and, if so, why it is omitted from the main table.","section":"Appendix A.7"}],"recommendation":"major_revision","confidential_remarks":"The paper has a sound and clearly described core method, and the fixed-beam MiniF2F result is strong enough that the central hypothesis remains plausible. The main blocker is not the method itself but the evidence: the headline comparison in Table 1 mixes unequal total search budgets, the adaptive hyperparameters are tuned on the test benchmarks, and the decontamination details are missing. If the authors can provide matched-budget curves and a validation-based selection procedure, I would be willing to support acceptance. I would also encourage the editors to ask for an ablation that isolates the data synthesis contribution, since without it the title's causal claim is not directly established."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"You should read this paper if you care about scalable synthetic data for LLM-based theorem proving. The authors present a clean engineering pipeline: they use tree search to explore intermediate proof states, constrain the policy to a curated set of 60 tactics, complete premises separately, and fine-tune Qwen2.5-Math-7B on ~20M proof transitions. They also add an adaptive beam-size schedule that decays from Bmax to Bmin during search. On MiniF2F and ProofNet they report Pass@1 of 60.74% and 21.18%, and the code and model are public.\n\nWhat is genuinely new is the proof-state exploration for data synthesis: forcing the model to sample low-probability tactics across a wide range of states, with tactic and premise generation decoupled. That is a plausible and practical way to generate training data without expert iteration. The adaptive beam decay is less surprising, it is a simple heuristic, but it works in their experiments. The paper is well-written, the limitations section is honest, and the implementation details (DoBeVi REPL, decontamination, rejection sampling) are concrete enough to reproduce.\n\nThe soft spots are real, and you should be skeptical of the headline deltas. Table 1 compares against baselines at their original beam sizes without matching total tactic-generation budget. Under the paper's own K×B×E accounting, the adaptive schedule on MiniF2F spends roughly 2.6k tactic generations versus 1.2k for BFS-Prover (B=2), so the 5-point gain over BFS-Prover is confounded by search compute. On ProofNet, their adaptive budget (~18k) is close to InternLM2.5-StepProver's B=32 budget (~19.2k), but the comparison to BFS-Prover at B=2 is again unfair. More seriously, the adaptive hyperparameters (Bmax, Bmin, λ) are tuned separately for each benchmark with no held-out validation split: that is test-set tuning of the most performance-sensitive parameter. There is also no ablation isolating the contribution of the proof-state exploration data; the fixed-beam results (e.g., 59.51% at B=8 on MiniF2F) are strong, but they still reflect more compute than BFS-Prover's budget.\n\nThat said, the underlying claim is probably sound. The fixed-beam results are competitive with strong baselines, and the adaptive schedule beats their own fixed beams while using fewer tactic generations on MiniF2F. The paper does not overclaim; it explicitly lists dependence on seed dataset and suboptimal scoring as limitations. It just needs budget-matched baselines and an ablation to be fully convincing.\n\nThis is a solid contribution for the ATP community. I would send it to peer review, but the authors should be asked to add budget-matched comparisons and ablate the data synthesis component. If they do, this could become a reliable reference point for tree-search ATP.","headline":"Solid engineering contribution to tree-search ATP with a clean data-synthesis pipeline, but the headline gains over baselines are confounded by unmatched search budgets and benchmark-tuned hyperparameters.","tokens_in":18145,"tokens_out":4133,"would_cite":true,"duration_ms":37213,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Proof-state exploration drives a 7B Lean prover to 60.74% on MiniF2F","keywords":["automated theorem proving","Lean 4","synthetic data generation","proof state exploration","adaptive beam search","tree search","Pass@1","large language models"],"falsifier":"Take a theorem whose only Lean 4 proof uses a tactic operator outside the 60-tactic set or below the frequency threshold of 0.999, run the full exploration, fine-tuning, and adaptive-beam pipeline on it, and check whether any search succeeds; a failure on such a theorem would show that the curated tactic set is a real ceiling. A separate check is to fix the beam size at its best constant value and compare against the adaptive schedule under the identical budget of one search and 600 expansions, which isolates how much of the reported gain comes from the schedule rather than from the synthetic data.","tokens_in":1787,"feed_emoji":"🧮","tokens_out":11839,"duration_ms":182649,"temperature":0.7,"pith_summary":"This paper argues that the bottleneck in LLM-based formal theorem proving is not the search strategy alone, but the shortage of training data that covers the intermediate proof states a policy actually meets during search. It proposes a one-pass data-synthesis method, proof-state exploration, which starts from a corpus of formalized theorems and forces a policy model to generate diverse tactic applications at many intermediate states, then records the resulting proof steps for fine-tuning. A companion adaptive beam-size strategy widens the search early and narrows it as depth grows, so the policy first explores a broad space of tactics and then concentrates on the most promising branches. On MiniF2F and ProofNet, the paper reports average Pass@1 rates of 60.74% and 21.18% under a budget of one search and 600 expansions, which it presents as evidence that scalable synthetic data, rather than expert iteration or a larger model, is the decisive ingredient.","feed_headline":"Proof-state exploration drives a 7B Lean prover to 60.74% on MiniF2F","feed_subtitle":"One synthetic-data pass over explored proof states plus a shrinking beam beats fixed-beam tree search on Pass@1.","key_machinery":"The load-bearing object is the proof-state exploration loop with constrained decoding over the curated tactic set $T$. $T$ contains the 60 tactic operators that survive a nucleus filter with $P=0.999$ applied to usage frequencies in a large Lean corpus, and every synthetic transition uses an operator from $T$ while premise completion is delegated to the policy model, so the data generator can produce diverse proof steps without needing complete proofs as ground truth. The adaptive beam schedule, which starts wide and linearly decays to a narrow beam as the expansion budget is consumed, converts the broad exploration data into focused proof completion during search.","core_discovery":"The central claim is that a Lean 4 policy model fine-tuned on synthetic proof transitions collected by exploring intermediate proof states can solve formal theorems with one-shot best-first search. Exploration decouples the tactic operator from its premises: at each state, constrained decoding forces the model to sample a batch of operators from a curated set of 60 high-frequency tactics, the same model fills in premises for each operator, and the Lean 4 prover advances the states; the batch deliberately includes low-probability operators that the policy would otherwise never emit. The resulting dataset of roughly 20 million transitions is combined with human-authored Lean library data and used for a single supervised fine-tuning pass, without expert iteration. At search time, an adaptive beam schedule shrinks the beam from a large initial value to a small final value as the number of expansions grows, and each child state is scored by the log-probability of the tactic that produced it plus the parent's score. Under Pass@1 with $K=1$ and $E=600$, the paper reports average success rates of 60.74% on MiniF2F and 21.18% on ProofNet.","pith_inferences":["The 60-tactic set acts as an upper bound on expressiveness: if a benchmark theorem needs an operator outside that set, neither exploration nor the trained policy can ever produce it, so part of the reported success may reflect how well the seed corpus's tactic distribution covers the evaluation benchmarks.","If the diversity mechanism is the active ingredient, then increasing the exploration budget or the number of seed problems should improve performance most on out-of-distribution benchmarks such as ProofNet; this scaling prediction is testable but not reported.","The scoring function rates the tactic, not the resulting proof state, so the adaptive beam is a heuristic patch over a weaker signal; a learned value estimator on states might dominate both the fixed and the adaptive schedules.","The same synthetic-transition data could plausibly be reused as a warm start for reinforcement learning or whole-proof generation, since it exposes the policy to precisely the states where search currently loses budget."],"forward_implications":["If the central claim is right, one exhaustive exploration pass over existing formalized statements can generate enough proof-step data to train a capable policy, removing the need for repeated expert-iteration loops.","The adaptive beam schedule implies that fixed beam sizes waste a fixed budget: wide early beams find candidate branches, and narrow late beams stop the search from being trapped in one subtree.","Because the method records all valid transitions, not just successful proofs, even unsolved or partially solved seeds contribute training data, so data volume scales with search expansion rather than with the number of completed proofs.","The method depends only on a proof assistant that can check single proof steps, so the same recipe should transfer to other interactive provers once an equivalent high-frequency tactic set is built.","The reported Pass@1 numbers under a one-search, 600-expansion budget provide a concrete target for later work: any competing tree-search method should be compared at the same expansion count and with the same pass definition."],"supporting_citations":[{"why":"Supplies the seed problem corpus for exploration and the usage statistics from which the 60-tactic set is derived.","marker":"[Dong and Ma, 2025]"},{"why":"Provides the BFS-Prover tree-search method used as a policy for exploration and as a comparison baseline.","marker":"[Xin et al., 2025]"},{"why":"Provides the InternLM2.5-StepProver baseline that is compared under the same search budget.","marker":"[Wu et al., 2024]"},{"why":"Supplies the 7B base model that is full fine-tuned into the policy model.","marker":"[Yang et al., 2024b]"},{"why":"Defines the MiniF2F evaluation benchmark.","marker":"[Zheng et al., 2021]"},{"why":"Defines the ProofNet evaluation benchmark.","marker":"[Azerbayev et al., 2023a]"},{"why":"Contributes the human-authored Lean 4 library data that is combined with the synthetic transitions before training.","marker":"[mathlib Community, 2020]"},{"why":"Supplies the constrained decoding technique that restricts tactic sampling to the curated set during exploration.","marker":"[Hokamp and Liu, 2017]"},{"why":"Establishes the tree-search and expert-iteration paradigm that this paper extends and contrasts with.","marker":"[Polu and Sutskever, 2020]"}],"fun_headline_variants":["Synthetic proof states push Lean 4 to 60.7% on MiniF2F","Exploring proof states yields 60.74% MiniF2F pass rate","Adaptive beam plus synthetic data lifts theorem proving","One-shot fine-tuning on 20M synthetic transitions hits 60.74%","Proof-state exploration beats fixed-beam search in Lean"],"cache_read_input_tokens":20224,"weakest_assumption_plain":"The entire pipeline assumes that the 60 high-frequency tactic operators found in the seed corpus are enough to prove the evaluation problems, because any proof requiring an operator outside that set is never generated during exploration and therefore can never be emitted by the trained model.","fun_headline_variants_meta":{"raw":{"variants":["Synthetic proof states push Lean 4 to 60.7% on MiniF2F","Exploring proof states yields 60.74% MiniF2F pass rate","Adaptive beam plus synthetic data lifts theorem proving","One-shot fine-tuning on 20M synthetic transitions hits 60.74%","Proof-state exploration beats fixed-beam search in Lean"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000418,"raw_usage":{"total_tokens":2154,"prompt_tokens":947,"completion_tokens":1207,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":563,"completion_tokens_details":{"reasoning_tokens":1113}},"tokens_in":563,"tokens_out":1207,"duration_ms":9394,"temperature":1.0,"reasoning_tokens":1113,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T20:41:56.945099+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a theorem whose only Lean 4 proof uses a tactic operator outside the 60-tactic set or below the frequency threshold of 0.999, run the full exploration, fine-tuning, and adaptive-beam pipeline on it, and check whether any search succeeds; a failure on such a theorem would show that the curated tactic set is a real ceiling. A separate check is to fix the beam size at its best constant value and compare against the adaptive schedule under the identical budget of one search and 600 expansions, which isolates how much of the reported gain comes from the schedule rather than from the synthetic data.","supporting_citations":[],"review_version":1}