{"id":"ff89292f-e6ee-43ce-88a3-00ea55d1c0ed","arxiv_id":"2412.14063","paper_version":3,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":5,"one_line_summary":"Rango proves 32.0% of Coq theorems in a large benchmark by retrieving relevant in-project proofs and lemmas at each step, outperforming prior proof synthesis tools.","lead":"Rango is a new tool that automatically proves theorems in the Coq proof assistant by retrieving relevant lemmas and previously written proofs from the project at every proof step and feeding them to a fine-tuned language model. On a benchmark of 10,396 theorems from real Coq projects, it proves 32.0%, about 29% more than the previous best automated tool.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Pretraining contamination may inflate the headline gains over Tactician and could even inflate the 47% proof-retriever effect; the two post-cutoff projects do not test that key ablation.","rationale":"I read the paper in good faith. The central claim, as the reader states, is that per-step retrieval of in-project proofs is the main driver of improvement. The paper provides Coq-validated results, a large new dataset, released code, and multiple ablations, which are real strengths. The most load-bearing threat is not internal inconsistency but test-set contamination. The authors acknowledge it and add a post-cutoff evaluation, but that evaluation has two weaknesses: (1) it covers only two projects, so the 6% margin over Tactician is fragile; (2) it does not evaluate the proof-retriever ablation, which is the direct evidence for the mechanistic claim. If the benchmark is memorized, the 47% effect might be inflated because retrieved proofs can serve as memory prompts for the model rather than providing project-specific knowledge. This is testable: running the Table IV ablation on the post-cutoff projects, and checking the base model's zero-shot proof rate on the benchmark, would settle it. I therefore partly agree with the reader's weakest assumption: contamination is central, but the reader emphasized the absolute 32.0% success rate, whereas the more precise danger is that the key ablation itself is unvalidated without contamination. The verdict remains CONDITIONAL, pending these checks. I recommend no change to the reader's verdict.","tokens_in":21185,"tokens_out":9180,"duration_ms":76287,"concrete_test":"Run the four variants from Table IV (Rango, Rango w/o Lemmas, Rango w/o Proofs, Rango w/o Retrieval) on the two post-cutoff projects Coq-BB5 and PnV (1,171 theorems) using the same 10-minute timeout, and compute the percentage gain from the proof retriever. Additionally, prompt the unfine-tuned DeepSeek-Coder 1.3B with the 10,396 CoqStoq benchmark theorem statements and check the generated proofs with Coq 8.18 to quantify how many theorems the base model can prove from memory. If the proof-retriever gain on post-cutoff theorems is far below 47% (or absent), the central claim about per-step proof retrieval must be qualified; if it is comparable, the contamination threat to the mechanism is resolved.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central quantitative support for Rango's contribution is the 47% increase in theorems proven when the proof retriever is added (Table IV: 150/500 vs 102/500). This ablation is run only on CoqStoq's benchmark, which was mined from public GitHub repositories and may overlap with DeepSeek-Coder 1.3B's pretraining data (Section V-H). The paper's own post-cutoff evaluation (Section V-H, Table III) shows that the headline 29% improvement over Tactician collapses to only 6% (352 vs 331 on 1,171 theorems). If the model has memorized benchmark proofs, the proof retriever may act partly as a cue that helps the LLM access memorized proofs, rather than as a source of genuinely new project-specific proof structure. In that case, the 150-vs-102 gap could shrink on uncontaminated theorems. The two post-cutoff projects are too few to establish statistical significance, and the paper does not run the proof-retriever ablation on them, so the core mechanistic claim is not yet tested without contamination.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents Rango, an automated Coq proof-synthesis tool that, at each proof step, retrieves similar in-project proofs and lemmas and feeds them, together with the current theorem, proof script, and proof state, to a fine-tuned DeepSeek-Coder 1.3B language model; a rollout-search procedure then attempts to complete the proof. The authors introduce CoqStoq, a dataset of 196,929 theorems and 2,225,515 proof steps from 2,226 GitHub repositories, and evaluate Rango on a 12-project benchmark. They report that Rango proves 32.0% of benchmark theorems versus 24.8% for Tactician and 19.3% for Proverbot9001, that it proves 4% more theorems than Graph2Tac on a three-project subset, and that removing the proof retriever degrades performance from 150 to 102 proven theorems on a 500-theorem ablation set (a 47% relative increase from adding the proof retriever). The paper also reports a post-training-cutoff evaluation on two newer projects, where Rango proves 30.1% versus Tactician's 28.3%.","tokens_in":21388,"tokens_out":5916,"duration_ms":54954,"significance":"If the results hold, Rango makes a solid contribution to retrieval-augmented proving by showing that per-step retrieval of full in-project proofs, not only lemmas, can substantially improve LLM-based tactic synthesis. The paper has several strengths: every synthesized proof is checked by Coq, so the reported theorems are sound; the main comparison against Tactician and Proverbot is run on the same benchmark and the same Coq version; the ablation isolates the proof retriever's contribution; and the authors release the code, models, and dataset. The post-cutoff evaluation is an honest acknowledgment of the contamination threat. However, the post-cutoff evidence is limited and does not control the central proof-retriever ablation, so the headline quantitative claims remain vulnerable to pretraining contamination.","major_comments":[{"comment":"The paper's own post-cutoff evaluation is the right kind of control for pretraining contamination, but it does not include the proof-retriever ablation. On the two post-cutoff projects, Rango's advantage over Tactician shrinks to 6% (352 vs 331 of 1,171 theorems), whereas on the main benchmark it is 29%. Since Table IV's central 47% proof-retriever effect (150 vs 102 of 500) is measured only on the pre-cutoff CoqStoq benchmark, it remains possible that part of that effect is the retriever cueing proofs memorized during pretraining rather than contributing new project-specific proof structure. The authors should run the same ablation (Rango vs Rango without proof retriever vs Rango without any retrieval) on the two post-cutoff projects, or otherwise provide contamination-controlled evidence for the proof-retriever mechanism.","section":"V-H (Table III) and V-C (Table IV)"},{"comment":"The central 47% claim rests on a single random subset of 500 theorems, with no repeated runs, confidence intervals, or significance testing. Because the searcher uses temperature sampling at temperature 1.0 and the subset is only about 5% of the 10,396-theorem benchmark, the 150-vs-102 difference carries nontrivial stochastic uncertainty. The paper should report variance over multiple seeds, bootstrap confidence intervals, or a significance test, and ideally run the ablation on the full benchmark (as was done for the retrieval-algorithm comparison in Table VI).","section":"V-C (Table IV)"},{"comment":"The claim that Rango proves 4% more theorems than Graph2Tac is based on a much weaker comparison than the rest of the evaluation: only three projects, different Coq versions (8.11 vs 8.18), and theorem statements matched across project versions that may differ in definitions and dependencies. The paper discloses these limitations, but the contribution list states that Rango does better than Graph2Tac. This claim should be either removed or substantially softened, or supported by a controlled comparison on identical project versions and a fixed Coq version.","section":"V-B (Table II and contributions list)"}],"minor_comments":[{"comment":"Please clarify whether Rango-PRE and Rango-Hybrid use separately fine-tuned models in which the training examples were also created with prefix-only or hybrid retrieval, or whether the same Rango model is reused with altered retrieval at inference time. This distinction matters for interpreting the comparison in Table VII.","section":"V-E (Table VII)"},{"comment":"The conference location in the ICSE reference is spelled 'Ottowa' but should be 'Ottawa'; also, the text says 'We call this retrieval technique prefix retrieval' in Section V-E but the abbreviation Rango-PRE is used in the table before the technique is fully defined, which may confuse readers.","section":"References and front matter"},{"comment":"Please state the number of rollouts or generated tactics per theorem that the 10-minute timeout allows in practice, and how the timeout interacts with the token-generation limit, since both affect the comparison with best-first search in Section V-F.","section":"V-A (Experimental Setup)"}],"recommendation":"major_revision","confidential_remarks":"The contamination concern is the central issue. The post-cutoff results already show that the benchmark advantage over Tactician shrinks from 29% to 6%, which makes the missing post-cutoff ablation a genuine gap rather than a hypothetical one. I am not recommending rejection because the approach is plausible and the Coq-checked evaluation is a solid basis, but the authors should be asked to run the proof-retriever ablation on the post-cutoff projects or otherwise address the contamination threat before the central claim can be accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Quick read of Rango. The genuinely new thing here is per-step retrieval of full in-project proofs, not just lemmas, and the paper makes a credible case that this is what moves the needle: the ablation shows the proof retriever adds 47% more theorems (150 vs 102 on 500), and the file-wise split shows the same pattern (160 vs 111). The CoqStoq dataset, with 2,226 projects and 196k theorems, plus the released code and models, is a real contribution for the community.\n\nSoundness is taken care of by Coq checking every generated proof. The comparison against Tactician and Proverbot is on the same benchmark and Coq version, which is fair. I also appreciate how forthright the threats section is about pretraining contamination.\n\nThe soft spots are real but not fatal. First, the post-cutoff comparison (Table III) shows the headline advantage over Tactician drops from 29% to 6% (352 vs 331 on 1,171 theorems). That's a large shrink, and the paper does not run the proof-retriever ablation on those two projects. So the central claim—that the proof retriever, not just the LM, drives the gain—is not yet tested in a contamination-free setting. I don't think this sinks the paper, but it deserves a clear follow-up. Second, the Graph2Tac comparison is on a different Coq version and only three projects, so treat that 4% as suggestive, not solid. Third, there are no confidence intervals or repeated-seed runs; the ablation set is 500 theorems and the main numbers are point estimates. Minor, but worth tightening.\n\nOne nuance on the stress-test note: the proof-retriever ablation compares two LLM variants on the same benchmark, so memorization would have to interact differently with the retriever to fully explain the 47% gap. That seems possible—the retriever could cue memorized proofs—but it would still be a useful mechanism. The post-cutoff ablation would settle it.\n\nBottom line: this is a serious, honest piece of work. It belongs in a reading group on proof automation, I would cite it, and it deserves serious peer review. Expect the reviewers to ask for the post-cutoff ablation and variance estimates before the numbers are taken as final.","headline":"Solid incremental contribution; the proof-retriever claim is plausible but the post-cutoff ablation gap should be closed before accepting the headline numbers at face value.","tokens_in":21959,"tokens_out":3007,"would_cite":true,"duration_ms":27279,"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":"Retrieving similar proofs from the same project at every step lets a Coq proof assistant's language model prove more theorems than prior automated tools.","keywords":["Rango","retrieval-augmented proving","Coq","proof synthesis","large language models","proof retrieval","lemma retrieval","CoqStoq"],"falsifier":"Run Rango and its no-proof-retriever ablation on thousands of Coq theorems written after the model's training cutoff and withheld from training; if the no-proof-retriever variant recovers most of the 47% advantage, the reported effect comes from memorized training data rather than from retrieving similar proofs.","tokens_in":20982,"feed_emoji":"✅","tokens_out":11227,"duration_ms":85906,"temperature":0.7,"pith_summary":"The paper tries to show that automated proof synthesis in Coq gets substantially better when the model is handed, at every proof step, similar proofs from the same project, not just lemmas and definitions. It builds Rango, which retrieves relevant proofs and lemmas, feeds them to a fine-tuned language model, and searches for complete proofs. On a benchmark of 10,396 theorems drawn from open-source Coq projects, Rango completes 32.0% of theorems, beating prior proof-synthesis tools; removing the proof retriever cuts the number of theorems proven by 47%. If the claim holds, a proof assistant can learn project-specific proof style from its own past proofs, reducing the manual effort of formal software verification.","feed_headline":"Per-step proof retrieval proves 29% more theorems","feed_subtitle":"Rango adapts to each project by pulling relevant proofs and lemmas into the model's context at every proof step.","key_machinery":"The load-bearing mechanism is Rango's tactic generator, which re-retrieves context at every step. The proof bank holds completed proofs from earlier in the file and from the file's dependencies; the proof retriever uses BM-25, a sparse scorer based on identifier-word overlap between proof states, to pick the most similar proofs to the current proof state. The lemma retriever uses TF-IDF to pick relevant lemmas. A fine-tuned decoder-only language model takes the retrieved proofs, retrieved lemmas, the proof script so far, and the current proof state, and generates the next tactic; a rollout searcher samples tactics until Coq accepts a complete proof or a timeout is reached. Token budgets partition the context among proofs, lemmas, script, and state, and the retrievers are run on the same pipeline during training and inference.","core_discovery":"The paper's central claim is that adding similar proofs from the current project to the language model's context, at every proof step, is what makes retrieval-augmented proving work well in Coq, not just adding lemmas. Rango combines a proof retriever that scores earlier in-project proofs by BM-25 similarity of proof states, a lemma retriever that scores lemmas by TF-IDF, and a fine-tuned decoder-only language model that predicts the next tactic from these retrieved items plus the current proof state. On the 10,396-theorem CoqStoq benchmark, Rango proves 32.0% of theorems, 29% more than the prior best tool Tactician; on the ablation set, removing the proof retriever lowers the number of theorems proven by 47%, while removing only the lemma retriever costs 3%. The paper interprets this as evidence that full proofs, not just premises, supply the project-specific proof strategies the model needs.","pith_inferences":["If per-step proof retrieval is the cause, the same design should transfer to other proof assistants such as Lean or Isabelle wherever a project's completed proofs can be indexed by proof state; the paper does not test this.","The result hints at a capacity-versus-retrieval trade-off: a smaller model with good proof retrieval may match a larger model without it, which would make proof automation cheaper to run.","Because plain BM-25 already beats generic code embeddings for proof-state similarity, a retriever trained specifically to rank proofs by how useful they are for the next tactic could push success rates above 32.0%.","A benchmark assembled entirely from theorems written after the model's training cutoff would settle the memorization question more fully than the paper's two post-cutoff projects."],"forward_implications":["On the CoqStoq benchmark, Rango proves 32.0% of theorems, which is 29% more than Tactician and 66% more than Proverbot9001.","Ablations attribute most of the gain to the proof retriever: removing it cuts proven theorems by 47%, while removing only the lemma retriever costs 3%.","Combining Rango with a prefix-retrieval variant that uses the lines immediately before the theorem as context proves 4% more theorems than Rango alone, so the two retrieval strategies cover different situations.","Sparse BM-25 proof retrieval beats dense CodeBERT embedding retrieval by 46% on the full benchmark, suggesting that identifier overlap captures proof-state similarity better than generic code embeddings.","Rango's success rate drops with human-proof length and with file dependency count, just as earlier tools' rates do, but from a higher baseline."],"supporting_citations":[{"why":"Defines Proverbot9001, one of the neural proof-search systems Rango is compared against on the benchmark.","marker":"[73]"},{"why":"Defines Tactician, the prior state-of-the-art proof-state k-NN prover whose benchmark score Rango exceeds by 29%.","marker":"[45]"},{"why":"Defines Graph2Tac, the online-representation-learning prover that retrieves definitions and lemmas, which is the closest comparison point.","marker":"[10]"},{"why":"Supplies CoqGym, whose projects form the core of the CoqStoq evaluation benchmark.","marker":"[90]"},{"why":"Supplies LeanDojo, the retrieval-augmented premise-selection approach that motivates retrieving lemmas during proof synthesis.","marker":"[91]"},{"why":"Introduces retrieval-augmented generation, the general mechanism that Rango adapts to per-step proof prediction.","marker":"[49]"},{"why":"Defines BM-25, the sparse retrieval algorithm that Rango uses to score proof-state similarity for proof retrieval.","marker":"[72]"},{"why":"Defines TF-IDF, the sparse retrieval algorithm that Rango uses to select relevant lemmas.","marker":"[77]"},{"why":"Defines Baldur, the whole-proof generation approach whose in-project context is the basis of Rango's prefix-retrieval variant.","marker":"[26]"},{"why":"Defines DeepSeek-Coder, the pretrained 1.3B language model that Rango fine-tunes for tactic generation.","marker":"[31]"}],"fun_headline_variants":["Rango adapts per-step to prove 29% more theorems","Proof context at every step: 47% more proved theorems","Adaptive retrieval-augmented proving for Coq","Similar proofs in context: 29% more theorems","Every step: pull similar proofs to prove 47% more"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The evaluation assumes that the CoqStoq benchmark theorems were not memorized during the language model's pretraining, so the reported 32.0% success rate and the 47% proof-retriever effect measure retrieval rather than recall.","fun_headline_variants_meta":{"raw":{"variants":["Rango adapts per-step to prove 29% more theorems","Proof context at every step: 47% more proved theorems","Adaptive retrieval-augmented proving for Coq","Similar proofs in context: 29% more theorems","Every step: pull similar proofs to prove 47% more"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000859,"raw_usage":{"total_tokens":3745,"prompt_tokens":980,"completion_tokens":2765,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":596,"completion_tokens_details":{"reasoning_tokens":2682}},"tokens_in":596,"tokens_out":2765,"duration_ms":19267,"temperature":1.0,"reasoning_tokens":2682,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-11T12:30:36.007075+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run Rango and its no-proof-retriever ablation on thousands of Coq theorems written after the model's training cutoff and withheld from training; if the no-proof-retriever variant recovers most of the 47% advantage, the reported effect comes from memorized training data rather than from retrieving similar proofs.","supporting_citations":[{"cited_title":"Sanchez-Stern, Y","cited_arxiv_id":null,"evidence_quote":"Defines Proverbot9001, one of the neural proof-search systems Rango is compared against on the benchmark."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies CoqGym, whose projects form the core of the CoqStoq evaluation benchmark."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies LeanDojo, the retrieval-augmented premise-selection approach that motivates retrieving lemmas during proof synthesis."},{"cited_title":"Polu and I","cited_arxiv_id":null,"evidence_quote":"Defines BM-25, the sparse retrieval algorithm that Rango uses to score proof-state similarity for proof retrieval."},{"cited_title":"Sparck Jones","cited_arxiv_id":null,"evidence_quote":"Defines TF-IDF, the sparse retrieval algorithm that Rango uses to select relevant lemmas."}],"review_version":1}