{"id":"b4ef0f89-5cfe-4480-bd37-e7c41cf0c988","arxiv_id":"2507.20199","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":4,"one_line_summary":"A reinforcement learning pipeline with Lean verifier feedback trains a 32B model that scores 70.0% pass@1 on miniF2F-test, a new state of the art.","lead":"StepFun-Prover, a 32-billion-parameter AI model, solves 70% of the problems in a standard formal mathematics benchmark by writing Lean 4 proofs. It reaches this level with fewer proof attempts than previous systems, using real-time feedback from the Lean verifier during reasoning.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Benchmark comparability is the load-bearing risk: the 70.0% is measured on Numina's corrected miniF2F variant, while the baseline numbers are borrowed from papers, so the claimed SOTA margin may not be apples-to-apples.","rationale":"I read the paper as making a comparative empirical claim rather than a mathematical one. The proofs themselves are machine-checked by Lean, so the reported 70% is not a hallucinated accuracy in the usual sense; the unresolved risk is whether the number is measured on the same benchmark as the numbers it is being compared with. Section 3.1 evaluates on Numina's corrected miniF2F and takes baselines from their original papers. These two facts together leave open the possibility that the corrections changed the problem set in a way that favors StepFun. A 6-8 point margin on a 244-problem test is large but not overwhelming; a benchmark-level shift of a few problems could change the ranking. The paper also does not document the diff, does not provide error bars, and does not state train/test disjointness even though its training corpora overlap topically with competition-math sources. I do not see internal inconsistency in the training pipeline; the methodological details are plausible and the Lean REPL integration is concrete. The concern is about external comparability and benchmark validity, not internal soundness. Therefore the reader's conditional verdict stands, pending a benchmark-alignment check. My agreement is partial because the reader emphasized the train/test contamination angle, while I view the benchmark-variant comparability issue as the more directly load-bearing threat to the specific comparative SOTA claim; the two are related and both are addressed by the proposed check.","tokens_in":20751,"tokens_out":8907,"duration_ms":117306,"concrete_test":"Obtain the Numina corrected miniF2F corpus and the standard miniF2F-test; diff the two statement sets. Then run the open-weights DeepSeek-Prover-V2-671B and Kimina-Prover-72B with the paper's exact evaluation protocol (temperature 1.0, top-p 0.999, max 20480 tokens, Lean 4.20.0, 32 responses per problem, 60s REPL timeout) on the corrected miniF2F, and compute pass@1. If the baselines reproduce within sampling error (roughly ±3-4% on 244 problems with 32 samples), the claimed margin is real; if they shift by several points or the diff changes problems, the SOTA claim is not established on a shared benchmark. As a fallback, evaluate StepFun-Prover-Preview-32B on the original miniF2F-test under the same protocol.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central claim is a comparative state-of-the-art result, so the evaluation must compare like with like. Section 3.1 says the evaluation uses 'Numina's corrected miniF2F benchmark from their HuggingFace repository' while the baseline numbers are 'sourced from their respective original papers.' The paper neither specifies the corrections nor re-runs those systems on the same variant. If the corrected benchmark differs from the instance used for the 61.9% and 63.9% numbers—for example by fixing ill-posed statements, changing Lean or Mathlib versions, or altering the problem list—the reported 6-8 point margin could be an artifact of the benchmark instance rather than of model capability. The Lean-verified proofs show that the 70% is real under this evaluation, but the SOTA superiority claim requires a shared measurement. A separate but related gap is that training used Lean Workbook, STP, and autoformalized Numina problems, and no train/test disjointness statement is given for a Numina-distributed corrected miniF2F, leaving memorization as an unresolved alternative explanation.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This technical report presents StepFun-Prover, a family of Lean 4 theorem-proving LLMs (7B and 32B) trained through cold-start supervised fine-tuning, response-pattern fusion, and tool-integrated GRPO with real-time Lean4-REPL feedback. The main empirical claim is a pass@1 of 70.0% on the miniF2F-test benchmark with 32 responses per problem, which the authors state surpasses DeepSeek-Prover-V2-671B (61.9%) and Kimina-Prover-72B (63.9%). The paper also contributes a training pipeline, an iterative RL-SFT cycle, and a detailed example of tool-integrated reasoning.","tokens_in":20984,"tokens_out":7132,"duration_ms":74069,"significance":"If the empirical claim survives scrutiny, the result would be practically significant: a 32B model outperforming the much larger DeepSeek-Prover-V2-671B with relatively few samples suggests that tool-integrated RL is a promising direction for automated theorem proving. The paper is also commendable for announcing release of model weights and for including a concrete example of REPL-driven proof repair. However, the significance is currently bounded by three issues: (i) the use of an uncircumscribed corrected miniF2F variant while baselines are borrowed from original papers, (ii) the absence of a train/test disjointness statement, and (iii) the lack of uncertainty quantification. These issues are fixable but must be addressed before the SOTA claim can be accepted.","major_comments":[{"comment":"The central SOTA comparison is not apples-to-apples. The text states that evaluation is done on 'Numina's corrected miniF2F benchmark from their HuggingFace repository,' while all baseline numbers are 'sourced from their respective original papers.' The corrections are never specified, and no baseline is re-run on the same corrected instance. If the corrected benchmark changes problem statements, the Lean/Mathlib version (the paper states Lean 4.20.0 for its own runs but not for the baselines), or the problem list, the reported margin of 6.1–8.1 percentage points could be an artifact of the benchmark instance rather than of model capability. The authors should either supply a diff of the corrections, re-run the baselines on the identical corrected benchmark with an identical protocol, or downgrade the superiority claim accordingly.","section":"§3.1, Table 1"},{"comment":"The paper does not state that the training corpora (Lean Workbook, STP, and autoformalized Numina problems) are disjoint from the corrected miniF2F test set. Because miniF2F is a public benchmark with substantial overlap with datasets commonly used for formalization, and the paper does not report deduplication, the 70.0% figure remains open to a memorization-based explanation. Please report the exact deduplication procedure (or a hash-based overlap analysis) against the test problems, and/or validate on an entirely disjoint benchmark such as ProofNet.","section":"§2.1 and §3.1"},{"comment":"No uncertainty quantification is reported. Pass@1 is estimated from 32 responses per problem; with a test set of roughly 244 problems, the standard error of the difference between 70.0% and 63.9% is on the order of 4 percentage points, so the claimed 'over 4%' superiority margin is within roughly 1.5 standard errors. The paper should report per-problem pass rates, confidence intervals (e.g., bootstrap), or a paired comparison of the models on the same problem set.","section":"§3.1, Table 1"}],"minor_comments":[{"comment":"The phrase 'OpenAI o-seriers' should be 'OpenAI o-series'.","section":"Related Work"},{"comment":"The spelling 'Stepfun-Prover' conflicts with 'StepFun-Prover' in the text, and the caption should define pass@1, the number of responses per problem, and the sampling budget used for the baseline methods.","section":"Figure 1 caption"},{"comment":"The group-based advantage divides by the standard deviation of the reward group, which can be zero when all sampled rewards are equal; please specify the behavior in that case (e.g., set the advantage to 0).","section":"§2.4, Eq. (1)"},{"comment":"For reproducibility, please provide the exact commit or date of Numina's corrected miniF2F repository, the evaluation harness, and the generated proofs for all problems.","section":"§3.1"}],"recommendation":"major_revision","confidential_remarks":"The paper is a technical-report-style submission whose main contribution is an empirical benchmark result. The central concern is not the training method but the comparability and contamination controls around the 70.0% claim. I would encourage the editor to treat the benchmark comparability and train/test disjointness requirements as mandatory for acceptance. There is no indication of missing prior-work citation or deliberate obscurity; the limitations are presented straightforwardly."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The headline is a number: 70.0% pass@1 on miniF2F-test with a 32B model and 32 samples. If that number holds up under a shared evaluation, it is a real advance over DeepSeek-Prover-V2 and Kimina-Prover, and the training pipeline is worth reading on its own.\n\nWhat's actually new and good: the pipeline itself. Cold-start SFT from mixed sources, response pattern fusion to merge Claude and Kimina styles, tool-integrated GRPO with REPL feedback, dynamic in-training data filtering based on per-prompt success rates, and masking REPL tokens in the loss. The engineering around Lean4-REPL is solid: async streaming, a Redis broker, and a memory fix already acknowledged upstream. The appendix example shows genuine multi-turn debugging, not a one-shot proof dump. And they release weights, which makes the central number checkable.\n\nThe soft spot is benchmark comparability, and it is load-bearing. The evaluation uses Numina's corrected miniF2F variant, while baselines are borrowed from their original papers, which evaluated on a different variant. The paper does not specify the corrections, does not re-run baselines on the same instance, and does not state whether miniF2F problems were excluded from training corpora. Memorization is therefore an unresolved alternative explanation, and the claimed 6-8 point margin over prior SOTA could be partly a benchmark-instance artifact. Also minor: pass@1 with 32 samples has no error bars, and with roughly 134 problems a few problems move the number by ~0.7%, so the gap to Kimina's 63.9% is not a statistical blowout.\n\nNone of this sinks the paper. The example proofs are verifiable, the mechanism is plausible, and the missing pieces are addressable. What is needed: re-run baselines on the same corrected benchmark, publish the correction list, and state train/test disjointness explicitly. Without that, the SOTA claim is premature but the underlying result is still worth engaging with.\n\nWho this is for: anyone working on LLM-based theorem proving, especially RL-with-tools pipelines. The training details are concrete enough to reproduce or adapt. Yes, send it to peer review with a request for those evaluation details; the result is important enough that a serious referee should see it.","headline":"A new SOTA number on miniF2F with a believable training story, but the comparison is only as good as the benchmark variant, and that variant is underspecified.","tokens_in":21527,"tokens_out":1638,"would_cite":true,"duration_ms":21419,"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":"The paper reports a training pipeline that lets a language model decide when and how to query the Lean 4 verifier, and claims that the resulting 32B model reaches 70.0% pass@1 on miniF2F-test—above the previously published results from…","keywords":["formal theorem proving","Lean 4","reinforcement learning","tool-integrated reasoning","miniF2F","GRPO","pass@1","verifier feedback"],"falsifier":"Build a held-out set of formal statements of comparable difficulty that are provably absent from the training corpora, run the released 32B model with the same 32-sample protocol, and compare pass@1. If the score falls to the level of the previous baselines, the headline number is largely memorization rather than learned tool-integrated reasoning. A cheaper check is to diff the miniF2F-test statements against the three training corpora for exact or near-duplicate statements.","tokens_in":20565,"feed_emoji":"🧮","tokens_out":8200,"duration_ms":86859,"temperature":0.7,"pith_summary":"This paper reports a way to train a large language model that solves formal proofs by interacting with the Lean 4 proof assistant while it thinks. The model is free to emit partial Lean code, read back the verifier's error messages, revise, and try again before giving a final proof, with no fixed script for how many interactions to use. Trained with supervised warm-up followed by reinforcement learning whose only reward is whether the final proof verifies, the resulting 32B-parameter model reaches a pass@1 of 70.0% on the corrected miniF2F-test benchmark using 32 sampled attempts per problem. That figure is higher than the previously published results for a 72B-parameter prover (63.9%) and a 671B-parameter prover (61.9%) on the same benchmark. The paper's broader claim is that letting the model drive its own tool use, guided by verifier feedback, is a practical route to efficient automated theorem proving.","feed_headline":"A 32B prover hits 70% on miniF2F by reading verifier feedback","feed_subtitle":"Reasoning, code sketches, and live Lean 4 errors train one model to out-prove much larger provers in only 32 tries.","key_machinery":"The carrier of the argument is the tool-integrated rollout: a hybrid trajectory of the form natural-language reasoning, a Lean 4 sketch enclosed in <sketch> and </sketch>, the verifier's output enclosed in <REPL> and </REPL>, repeated until a final proof is emitted after a </think> delimiter. Each time the model closes a sketch, generation pauses, the snippet is sent to a wrapped Lean 4 REPL, and messages (errors, goals, sorries, or success) are returned as tokens the model can read. Training uses GRPO with a binary reward of 1 only when the final proof verifies and 0 otherwise, with the verifier-feedback tokens masked out of the loss so the model is trained only on its own reasoning. Around this mechanism sits a pipeline: a cold-start dataset built from formal corpora and autoformalized word problems, filtered for tautological, contradictory, or ill-posed statements; a fusion step that corrects wrong proofs from an existing 72B prover to harmonize response styles; an iterative RL-SFT cycle that re-trains on successful trajectories from problems of intermediate difficulty; and an asynchronous remote server that runs over a thousand REPL processes in parallel, making multi-turn reinforcement learning feasible.","core_discovery":"The central claim is that a proof-generating model can learn, end to end, to interleave natural-language reasoning with Lean 4 code sketches and live verifier feedback, and that this tool-integrated behavior transfers to a benchmark. The trained 32B model solves 70.0% of the problems on the corrected miniF2F-test at pass@1 with 32 generations per problem, while its 7B sibling reaches 66.0%. The paper argues these results come from the training pipeline rather than from larger scale: the same approach is presented as the reason the 32B model outperforms substantially larger prior provers, and longer generation limits (more room for reflection and interaction) push performance from 58.3% at 4096 tokens to 70.0% at 20480 tokens. The authors also observe emergent interaction habits, such as resolving warnings proactively, restructuring a proof when a tactic times out, and refining a solution after reading feedback.","pith_inferences":["Because the paper does not state that the corrected miniF2F-test problems are disjoint from the three training sources it lists (the workbook corpus, the self-play theorem-proving dataset, and autoformalized word problems), a portion of the 70.0% could reflect memorization; an independent contamination audit would settle this.","Pass@1 at 32 samples does not count the compute spent on REPL round-trips and re-generation inside each trajectory, so the efficiency gain relative to sampling-heavy baselines should be measured in total Lean calls or total tokens per solved problem, not just passes per sample.","The same training recipe could be tested on harder held-out problem sets, for example competition problems not present in any training corpus, to see whether the tool-integrated behavior generalizes rather than overfitting to benchmark idioms.","A natural extension, not explored here, is to give the model credit for intermediate milestones, such as clearing an error or closing a goal, through dense reward shaping, which could speed up learning beyond the binary final-proof reward."],"forward_implications":["Longer allowed generation length improves pass@1 monotonically on miniF2F-test, from 58.3% at 4096 tokens to 70.0% at 20480 tokens, so spending more generated tokens on check-and-revise behavior buys accuracy.","A 32B-parameter model trained this way can exceed the reported pass@1 of a 671B-parameter prover, so agentic use of verifier feedback can substitute for parameter count at this task.","The reward signal does not need to grade partial progress: binary outcome-based reward on final verification, combined with feedback tokens, is sufficient for the model to learn multi-step repair behavior.","The pipeline is presented as a general end-to-end framework for tool-integrated reasoning, applicable beyond formal mathematics to any setting where an environment returns reliable signals."],"supporting_citations":[{"why":"supplies the base models the training begins from and the precedent of outcome-only reward for reasoning models.","marker":"[2]"},{"why":"provides the autoformalizer used to generate formal problems from word problems and serves as a prior baseline.","marker":"[4]"},{"why":"serves as the main prior state-of-the-art baseline whose 61.9% pass@1 the paper compares against.","marker":"[5]"},{"why":"provides wrong proof responses and single-turn refinement data used in cold-start training, and is a baseline at 63.9%.","marker":"[8]"},{"why":"defines Lean 4, the formal verifier that executes sketches and supplies REPL feedback.","marker":"[9]"},{"why":"supplies one of the two open-source formal problem corpora used to build the cold-start training set.","marker":"[10]"},{"why":"supplies the other formal corpus and the prompts used during reinforcement learning.","marker":"[11]"},{"why":"provides the large model used to filter low-quality, tautological, or ill-posed training problems.","marker":"[12]"},{"why":"generates the roughly 8,000 multi-turn interaction trajectories used as cold-start data.","marker":"[13]"},{"why":"is the Lean read-eval-print-loop wrapped for multi-turn verifier interaction.","marker":"[15]"}],"fun_headline_variants":["Lean 4 prover learns from verifier feedback, hits 70% on miniF2F","32B model solves 70% of Lean proofs by checking its own work","Tool-integrated RL trains a prover to think and verify step by step","Verifier feedback powers a 32B prover to 70% on miniF2F","AI theorem prover uses live feedback to reach 70% on math benchmark"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the corrected miniF2F-test set is a fair, uncontaminated measure of proving ability, and specifically that its problems were not present in the training data; the paper does not document train/test disjointness or the corrections applied.","fun_headline_variants_meta":{"raw":{"variants":["Lean 4 prover learns from verifier feedback, hits 70% on miniF2F","32B model solves 70% of Lean proofs by checking its own work","Tool-integrated RL trains a prover to think and verify step by step","Verifier feedback powers a 32B prover to 70% on miniF2F","AI theorem prover uses live feedback to reach 70% on math benchmark"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000562,"raw_usage":{"total_tokens":2628,"prompt_tokens":862,"completion_tokens":1766,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":478,"completion_tokens_details":{"reasoning_tokens":1656}},"tokens_in":478,"tokens_out":1766,"duration_ms":14413,"temperature":1.0,"reasoning_tokens":1656,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T13:41:20.808427+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build a held-out set of formal statements of comparable difficulty that are provably absent from the training corpora, run the released 32B model with the same 32-sample protocol, and compare pass@1. If the score falls to the level of the previous baselines, the headline number is largely memorization rather than learned tool-integrated reasoning. A cheaper check is to diff the miniF2F-test statements against the three training corpora for exact or near-duplicate statements.","supporting_citations":[{"cited_title":"Kimina-Prover: Applying test-time rl search on large formal reasoning models, 2025","cited_arxiv_id":null,"evidence_quote":"provides wrong proof responses and single-turn refinement data used in cold-start training, and is a baseline at 63.9%."},{"cited_title":"The lean 4 theorem prover and programming language","cited_arxiv_id":null,"evidence_quote":"defines Lean 4, the formal verifier that executes sketches and supplies REPL feedback."},{"cited_title":"System card: Claude Opus 4 & Claude Sonnet 4","cited_arxiv_id":null,"evidence_quote":"generates the roughly 8,000 multi-turn interaction trajectories used as cold-start data."},{"cited_title":"A read-eval-print-loop for lean 4","cited_arxiv_id":null,"evidence_quote":"is the Lean read-eval-print-loop wrapped for multi-turn verifier interaction."}],"review_version":1}