{"id":"25568d3c-b1b3-4a4f-9d5e-1dbe2da804bf","arxiv_id":"2506.11487","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":6,"one_line_summary":"An inference-only neuro-symbolic pipeline, DSP+, solves 80.7% of miniF2F and the previously unsolved imo_2019_p1, matching heavily RL-trained theorem provers without fine-tuning.","lead":"DSP+ coordinates off-the-shelf AI reasoning models with a symbolic theorem prover to prove competition math problems in Lean, without any extra training. It matches the accuracy of heavily trained systems on benchmarks like miniF2F while using fewer tokens, suggesting a cheaper path for automated math proof.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The 80.7% miniF2F parity is computed on a dataset with eight corrected statements and a different Lean version than the comparison systems, so the headline claim is not yet anchored to a fixed benchmark.","rationale":"I read the paper's central claim as an empirical parity claim: with no additional training, DSP+ matches or approaches RL-trained systems on standard benchmarks. For that claim to hold, the benchmark must be identical across systems. The paper's own appendices show two ways in which it is not: eight statements were corrected after DSP+ failed on them, and the Lean/Mathlib version differs from the v4.9.0-rc1 dataset used by DeepSeek-Prover-V1.5/V2 lineage, with version-dependent tactic behavior documented in Appendix E.4. The reader's weakest-assumption analysis already identifies the corrected statements as the main risk; I agree, and I fold in the version mismatch as part of the same fixed-benchmark concern. This is not an accusation of bad faith: discovering formalization errors is a legitimate contribution, and the corrections may make the benchmark more faithful to the intended mathematics. But the comparison with published scores of other systems is only fair if the same statements are used; otherwise the reported parity could be driven by benchmark curation rather than by the DSP+ pipeline itself. I considered other candidate concerns (accumulative ensemble results, pass@k methodology, lack of commit-anchored code, token accounting). Those are real limitations but secondary: the ensemble is clearly labeled as accumulative, and token accounting is detailed. The benchmark-fixity concern is the most load-bearing because it directly affects the single number used for the headline parity claim. A clean empirical test is available: recompute on original statements or exclude corrected ones, and see whether the parity survives. Until that is reported, the appropriate verdict is CONDITIONAL, which is exactly what the reader assigned; no change is needed.","tokens_in":32224,"tokens_out":7517,"duration_ms":70193,"concrete_test":"Publish a commit-anchored statement manifest for the 244 miniF2F-test problems, with a per-statement diff against the original v4.9.0-rc1 miniF2F. For each of the eight corrected statements, determine whether the original statement is provable in Lean v4.17.0-rc1 and whether DSP+ (R1-V3-BFS, pass@1024) proves the original. Recompute the headline accuracy on the original statements only. If any corrected-only successes disappear and 80.7% drops materially, restate the parity claim as conditional on the corrected benchmark.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is that an inference-only pipeline is comparable to RL-trained provers. That comparison is only meaningful if all systems face the same formal statements in the same environment. This condition is not met. Appendix F reports eight miniF2F-test statements that DSP+ could not prove as formalized and that the authors then corrected, and the paper states 'We use their corrected versions in our experiments' (footnote to Appendix F). Section 5.2, however, describes the benchmark as simply 'the Lean 4 version', so the headline 80.7% silently includes solutions to these post-hoc corrected statements. Since Kimina-Prover-Preview and DeepSeek-Prover-V2 results are cited from their own papers on their own statement and version sets, the parity may be an artifact of benchmark modification rather than of the neuro-symbolic pipeline. The concern is reinforced by the paper's own Appendix E.4, which shows that the same proof can fail or succeed depending on Lean version (v4.9.0-rc1 vs v4.17.0-rc1), and by footnote 4, which notes Lean version issues affect DeepSeek-Prover-V2. Even if the corrections are mathematically justified, they must be applied uniformly to all compared systems or removed from the headline comparison before 'comparable performance' is claimed.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper proposes DSP+, an inference-only, three-phase theorem-proving pipeline for Lean 4. In the draft phase, a reasoning LLM generates a concise natural-language proof outline; in the sketch phase, a second LLM autoformalizes the outline into a hierarchy of subgoals with explicit hypothesis hints, and a rule-based \"error line masking\" repair removes syntactically invalid lines; in the proving phase, the subgoals are discharged by an integration of Aesop tree search with a step prover (BFS-Prover-7B). The default configuration (QwQ-32B, DeepSeek-V3-0324, BFS-Prover) reports 79.5% on miniF2F-test, 32.8% on ProofNet-test, and 24/644 on PutnamBench; replacing QwQ with DeepSeek-R1 gives 80.7% on miniF2F-test, and an ensemble of six configurations reaches 83.6%. The paper further claims that DSP+ proves imo_2019_p1 for the first time and that it discovered eight wrong formalizations in miniF2F. The evaluation uses Lean 4 v4.17.0-rc1, and the headline comparison is made against RL-trained provers such as DeepSeek-Prover-V2-671B and Kimina-Prover-Preview-72B.","tokens_in":32512,"tokens_out":7479,"duration_ms":70791,"significance":"If the headline claims held on a fixed, version-controlled benchmark, this would be a notable result: it would show that an inference-only neuro-symbolic pipeline, using off-the-shelf models, can reach parity with RL-trained provers on miniF2F while spending fewer inference tokens, and it would provide a useful tool for proof-data generation and formalization auditing. The paper's strengths include extensive ablations over draft/sketch/proving components, open prompts, a full trace for imo_2019_p1, discussion of failure modes, and the formalization-error discovery workflow. The main caveat is that several comparison mechanisms—dataset corrections, Lean-version differences, accumulative ensembling, and token accounting—are not yet aligned between DSP+ and the cited systems, so the significance is conditional on resolving these measurement issues.","major_comments":[{"comment":"The central parity claim is computed on a modified benchmark. Appendix F identifies eight miniF2F-test statements that were corrected after DSP+ failures, and footnote 5 states \"We use their corrected versions in our experiments,\" while §5.2 describes the benchmark only as \"the Lean 4 version.\" The 80.7%/83.6% numbers in Table 1 therefore do not measure the same problem set as the cited Kimina-Prover-Preview or DeepSeek-Prover-V2 results. Please report results on both the original and corrected statement sets, and either apply the corrections uniformly to all compared systems or remove the corrected-benchmark results from the headline comparison.","section":"§5.2, Appendix F, Table 1"},{"comment":"The comparison is also not version-matched. DSP+ runs on Lean 4 v4.17.0-rc1, while the cited baselines report results on their own Lean/Mathlib versions; §E.4 demonstrates that a proof can succeed under v4.9.0-rc1 and fail under v4.17.0-rc1, and footnote 4 notes version-related issues for DeepSeek-Prover-V2. These environment differences can change pass rates independently of the proving method. The paper should either re-run the compared systems on identical statements and Lean versions or explicitly qualify every cross-system number as version-sensitive.","section":"§5.1, §E.4, footnote 4"},{"comment":"The \"DSP+ ensemble\" result is reported as an accumulative union over six configurations with heterogeneous budgets (three at pass@1024, three at pass@128), not as a single algorithm with a defined total budget. Placing this union in Table 1 next to single-method pass@k numbers makes the comparison unclear, especially since §5.3 claims parity \"under the same sample budget.\" Please specify the total number of workflow attempts, tokens, and search budget for the ensemble, and compare it against an equivalently defined budget for each baseline.","section":"§5.3, Table 2"},{"comment":"The token-efficiency claim relies on average token counts reported in other papers for DeepSeek-Prover-V2 and Kimina-Prover-Preview, while DSP+ token counts are measured under the authors' own sampling configuration; the pass counts also differ (1024 vs. 8192). Please state exactly how each table entry is computed, including whether decoding settings and tokenizer conventions are matched, and provide sensitivity estimates for the total-token comparison.","section":"§6.4, Table 3"},{"comment":"PutnamBench results are not directly comparable across rows: DSP+ rows use a 644-problem Lean subset, whereas DeepSeek-Prover-V2 rows use 658 problems, and §5.2 notes the benchmark \"is extended to 658 problems later.\" Reporting 24/644 next to 49/658 without a common denominator can misstate the relative performance. Please use a fixed version of PutnamBench for all systems or report both counts with explicit version labels.","section":"Table 1, §5.2"}],"minor_comments":[{"comment":"The conciseness motivation in §3.1 is weakened by the paper's own ablation: Figure 4 shows that removing the conciseness prompt (\"No Format\") slightly outperforms the default concise format (75.4% vs. 74.2% at pass@128). Please reconcile this with the abstract's claim that concise draft generation benefits the pipeline, or reposition conciseness as an efficiency/robustness property rather than an accuracy improvement.","section":"§3.1, §6.2, Figure 4"},{"comment":"The imo_2019_p1 trace mixes sketch lines, proof lines, inline \"sorry\" placeholders, and editorial comments in a two-column layout; please provide a standalone, verified .lean file (or a pointer to the released artifact) so the claim that the final proof contains no unproved axioms can be checked directly.","section":"Appendix H"},{"comment":"Reference [52] duplicates reference [8] (InternLM2.5-StepProver), and the reference list/header contain minor formatting inconsistencies; please clean up citations and duplicate entries.","section":"References"},{"comment":"In the ProverBench table, DSP+ ensemble (55.69%) is compared to DeepSeek-Prover-V2-671B (59.1% at 512) without stating the ensemble's total sample budget; please add budget and token counts to this table so the comparison is interpretable.","section":"Table 6"},{"comment":"The phrase \"pass@k\" is used for executing the whole workflow k times, which differs from the standard next-tactic pass@k used in some baselines; please define the sampling unit (workflow attempt vs. tactic sample) explicitly when reporting pass@1024 and pass@8192.","section":"§4"}],"recommendation":"major_revision","confidential_remarks":"The paper is worth a revision rather than rejection: the DSP+ pipeline and the imo_2019_p1 result are potentially valuable, and the measurement problems are addressable by re-running comparisons on a fixed benchmark and version. I would ask the authors to supply the exact configuration files/artifacts and both original/corrected miniF2F numbers in the revision; if the corrected statements are kept, the comparison tables should be rerun or clearly separated."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"This paper deserves a serious referee, but the headline claim needs to be read with its caveats. The load-bearing assertion is that an inference-only pipeline matches Kimina-Prover-Preview-72B and approaches DeepSeek-Prover-V2 on miniF2F, plus proves imo_2019_p1 for the first time. That parity is computed on a benchmark where eight miniF2F statements were corrected after DSP+ failures, and where the Lean version (v4.17.0-rc1) differs from the versions used in the comparison papers. The paper is transparent about both facts, and some corrections actually make problems harder (the rfl example in Appendix E.4 shows the opposite direction), so the comparison is not obviously rigged in their favor. But it is not apples-to-apples, and the parity should not be stated so flatly until the comparison is rerun on a fixed statement set and version.\n\nWhat is genuinely new: the fine-grained enhancements to DSP—concise draft filtering, hypothesis-aware sketch with prove_with hints, error-line masking, and the built-in integration of Aesop with BFS-Prover. The ablation suite is broad and informative: removing hypothesis hints or error masking drops accuracy noticeably, and the component ablations show real synergy. The discovery of eight formalization errors in miniF2F is a concrete contribution in itself, as is the first proof of imo_2019_p1. Full traces and prompts are included, and the code is promised, which is more than many papers in this area ship.\n\nSoft spots, in proportion: the ensemble numbers are an accumulative union over six configurations, which is fine but should not be compared directly to a single pass@k of other systems. Token-efficiency comparisons rely on token counts reported in other papers, which is a weak basis. The conciseness claim is undercut by their own ablation: \"No Format\" slightly beats \"Concise Steps\" (75.4 vs 74.2). None of these are fatal; they are the usual gaps between a strong technical report and a careful benchmark study.\n\nWho should read this: anyone building neuro-symbolic provers, people studying whether RL training is truly necessary for competition-level formal math, and benchmark maintainers who should care about the eight corrected statements. For peer review: yes, send it out. Ask the reviewers to re-run the miniF2F comparison on a fixed statement set and version, and to separate the corrected-statement results from the headline. That is a fixable issue, not a fatal one.","headline":"Solid engineering and honest ablations, but the headline parity with RL-trained provers rests on a post-hoc corrected benchmark and a different Lean version—worth refereeing, not taking at face value.","tokens_in":33035,"tokens_out":1953,"would_cite":true,"duration_ms":20624,"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":"Without any training, a careful three-phase coordination of off-the-shelf reasoning models and tactic-step provers matches RL-trained state of the art on formal math benchmarks.","keywords":["automated theorem proving","Lean 4","Draft-Sketch-Prove","neuro-symbolic reasoning","reasoning models","reinforcement learning","tactic step provers","miniF2F"],"falsifier":"Re-run DSP+ and the cited baselines on the original, uncorrected miniF2F statements under a single Lean version, and check whether DSP+ still reaches 80.7% and whether the corrected statements are the only ones it solves; a significant drop would overturn the parity claim.","tokens_in":32033,"feed_emoji":"🧮","tokens_out":8931,"duration_ms":79214,"temperature":0.7,"pith_summary":"DSP+ is an inference-only revival of the Draft, Sketch, and Prove framework. It claims that, with no model training or fine-tuning, a careful three-phase coordination of off-the-shelf reasoning models and tactic-step provers can match reinforcement-learning-trained theorem provers on standard benchmarks. On miniF2F-test it solves 80.7%, on ProofNet-test 32.8%, and on PutnamBench 24 of 644 problems, while spending fewer inference tokens than a frontier RL-trained prover at equal accuracy. It also proves imo_2019_p1, an IMO problem no prior system solved, and exposes eight wrongly formalized miniF2F statements. If the parity holds, large-scale RL training is not the only route to advanced formal theorem proving.","feed_headline":"No-training theorem prover matches RL-trained rivals","feed_subtitle":"Coupling off-the-shelf reasoning models with Lean search solves 80.7% of miniF2F and a first IMO problem.","key_machinery":"The load-bearing mechanism is the three-phase DSP+ workflow, where each phase is engineered with the next phase in mind. In the sketch phase, LLM-generated subgoals are written with `prove_with[...]` hypothesis hints, which tell the prover which assumptions to keep and prevent cluttered proof states; lines that do not parse are masked, either commented out or replaced with `sorry`, so the rest of the sketch survives. In the proving phase, Aesop, a white-box best-first proof search for Lean, is modified so its tree nodes can be expanded either by built-in symbolic tactics or by tactic proposals from BFS-Prover, operating directly on Lean proof states rather than on reconstructed theorem statements. The draft phase feeds this machinery by prompting a reasoning model for one-equation-per-step drafts and removing thinking tokens, keeping the sketch short enough to avoid long-context degradation.","core_discovery":"The paper's central discovery is that the original DSP pipeline's poor results in Lean 4 came from coarse, phase-independent coordination, not from a fundamental limit of the inference-only paradigm. DSP+ improves each phase individually and in relation to the others: reasoning models produce concise natural-language drafts with thinking tokens stripped; the sketch model formalizes these as `have` subgoals carrying explicit hypothesis hints (`prove_with [h1, h2]`); and syntactically broken sketch lines are masked instead of restarting the sketch. The proving phase then merges Aesop's tree search with a BFS-Prover step prover, so every node can be expanded by either the symbolic engine or the neural prover. With a QwQ-32B draft, DeepSeek-V3-0324 sketch, and BFS-Prover proving, DSP+ reaches 79.5% on miniF2F-test at pass@1024, and swapping in DeepSeek-R1 as the draft model raises this to 80.7%. At that level it matches Kimina-Prover-Preview-72B at pass@8192 and approaches DeepSeek-Prover-V2-671B, while using less inference budget. It proves imo_2019_p1, an IMO problem not solved by any prior work, and uses its human-readable proof skeletons to find eight misformalized miniF2F statements, which the paper corrects in its experiments.","pith_inferences":["Editorial inference: the parity claim is only as fair as the benchmark comparison; the paper's eight corrected miniF2F statements mean a same-statement, same-Lean-version head-to-head is needed to make the match with prior published results airtight.","Editorial inference: error-line masking is a double-edged repair; it keeps workflows alive, but commented-out sketch lines could silently change what is being proved, so counting how often masked lines turn out to be genuinely unprovable would quantify this risk.","Editorial inference: the human-readable sketches produced by DSP+ could serve as a curriculum for RL training, not just cold-start data, by teaching a model to imitate the subgoal decompositions that make proofs tractable.","Editorial inference: because the original DSP ran on Isabelle, the same neuro-symbolic coordination should transfer to other proof assistants, with the assistant's native symbolic search in place of Aesop."],"forward_implications":["Large-scale RL training is not the only route to state-of-the-art formal proving; the paper's inference-only pipeline matches a frontier RL-trained prover at equal accuracy.","DSP+ extends the set of automatically provable IMO problems, proving imo_2019_p1 for the first time.","The readable subgoal structure turns the prover into a benchmark-auditing tool, leading to eight corrected miniF2F statements.","Ensembling different draft and sketch models raises miniF2F-test accuracy to 83.6%, showing model diversity is a resource even without training.","Because each phase is modular, the pipeline can be redeployed with newer reasoning models at low cost."],"supporting_citations":[{"why":"Supplies the miniF2F benchmark and its IMO subset on which DSP+ is evaluated.","marker":"[12]"},{"why":"The original Draft, Sketch and Prove framework that DSP+ revives with fine-grained neuro-symbolic enhancements.","marker":"[13]"},{"why":"BFS-Prover, the tactic step prover whose proposals expand nodes in the proving-phase tree search.","marker":"[4]"},{"why":"Aesop, the white-box best-first search engine that forms the symbolic backbone of the proving phase.","marker":"[43]"},{"why":"DeepSeek-Prover-V2, the RL-trained baseline whose accuracy DSP+ approaches and whose token budget is compared.","marker":"[2]"},{"why":"Kimina-Prover-Preview, the RL-trained baseline at pass@8192 that DSP+ matches at 80.7% on miniF2F-test.","marker":"[3]"},{"why":"QwQ-32B, the reasoning model used as the default draft model.","marker":"[17]"},{"why":"DeepSeek-V3-0324, the default sketch model that autoformalizes the draft into subgoals.","marker":"[18]"},{"why":"DeepSeek-R1, the draft model whose replacement lifts DSP+ to 80.7% on miniF2F-test.","marker":"[19]"},{"why":"Lean Copilot, used to integrate BFS-Prover directly into Aesop's internal search over Lean proof states.","marker":"[34]"}],"fun_headline_variants":["Untrained neuro-symbolic prover ties RL-trained models","DSP+ revives classic theorem proving to rival RL training","Zero-training prover solves previously unsolved IMO problem","Off-the-shelf models plus symbolic search match RL-trained provers"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The headline parity assumes that solving the eight corrected miniF2F statements is no easier than solving the original ones, and that comparing against baselines evaluated on their own Lean versions is a fair apples-to-apples comparison.","fun_headline_variants_meta":{"raw":{"variants":["Untrained neuro-symbolic prover ties RL-trained models","DSP+ revives classic theorem proving to rival RL training","Zero-training prover solves previously unsolved IMO problem","Off-the-shelf models plus symbolic search match RL-trained provers"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001045,"raw_usage":{"total_tokens":4520,"prompt_tokens":1199,"completion_tokens":3321,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":815,"completion_tokens_details":{"reasoning_tokens":3250}},"tokens_in":815,"tokens_out":3321,"duration_ms":24919,"temperature":1.0,"reasoning_tokens":3250,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T04:04:17.786628+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Re-run DSP+ and the cited baselines on the original, uncorrected miniF2F statements under a single Lean version, and check whether DSP+ still reaches 80.7% and whether the corrected statements are the only ones it solves; a significant drop would overturn the parity claim.","supporting_citations":[{"cited_title":"Aesop: White-box best-first proof search for lean","cited_arxiv_id":null,"evidence_quote":"Aesop, the white-box best-first search engine that forms the symbolic backbone of the proving phase."},{"cited_title":"Kimina-prover preview: Towards large formal reasoning models with reinforcement learning","cited_arxiv_id":null,"evidence_quote":"Kimina-Prover-Preview, the RL-trained baseline at pass@8192 that DSP+ matches at 80.7% on miniF2F-test."}],"review_version":1}