Pith. sign in

REVIEW 3 major objections 3 minor 98 references

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

T0 review · 3 major / 3 minor · reviewed 2026-08-11 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read 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.

desk verdict 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. read the letter →

arxiv 2412.14063 v3 pith:37GEVRQX submitted 2024-12-18 cs.SE cs.AI

Kyle Thompson , Nuno Saavedra , Pedro Carrott , Kevin Fisher , Alex Sanchez-Stern , Yuriy Brun , João F. Ferreira , Sorin Lerner
show 1 more author
Emily First
This is my paper · ORCID
classification cs.SEcs.AI
keywords Rangoretrieval-augmentedprovingCoqproofsynthesislargelanguagemodelsretrievallemmaStoq
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 3 minor

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%.

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 (3)
  1. [V-H (Table III) and V-C (Table IV)] 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.
  2. [V-C (Table IV)] 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).
  3. [V-B (Table II and contributions list)] 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.
minor comments (3)
  1. [V-E (Table VII)] 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.
  2. [References and front matter] 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.
  3. [V-A (Experimental Setup)] 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.

Circularity Check

0 steps flagged · score 0.0 of 10

No circular derivation: Rango's claims are supported by held-out benchmark evaluation and Coq-verified proofs, with no fitted quantity re-labeled as a prediction.

full rationale

Rango's central claim is that in-project proof and lemma retrieval improves tactic prediction. The proof retriever (BM-25 over proof states) and lemma retriever (TF-IDF) are fixed retrieval algorithms with no parameters fitted to the benchmark; the LLM is fine-tuned on a disjoint training split, and the benchmark and post-cutoff projects are held out. The 47% proof-retriever effect comes from an ablation in which a variant is trained without proof retrieval and evaluated on the same held-out subset (Table IV), so the improvement is empirical rather than forced by construction. All synthesized proofs are checked by Coq, so success is not self-certified. The paper's own Section V-H acknowledges that CoqStoq's benchmark may overlap with DeepSeek-Coder's pretraining data and mitigates with two post-cutoff projects; this is an external-validity risk (and the post-cutoff comparison is limited), but it is not a circularity, because the benchmark numbers are not defined in terms of the model's outputs. The only self-citations (CoqPyt for data extraction and Baldur for next-token loss masking) are tooling/methodological references, not load-bearing arguments that assume the paper's conclusion. No equation or definition reduces a claimed result to its input.

Assumptions & free parameters 5 free parameters · 4 assumptions · 0 invented entities

The paper introduces no mathematical entities. Its free parameters are standard ML hyperparameters and retrieval token limits. The main domain assumptions are about benchmark representativeness, the validity of BM-25 for proof relevance, and pretraining contamination.

free parameters (5)
  • number of retrieved proofs (k) = not reported
    The proof context is token-limited to 1024 tokens, so k varies per step; the exact value is not fixed or reported.
  • number of retrieved lemmas (j) = not reported
    Lemma context is token-limited to 512 tokens; j is not specified explicitly.
  • temperature = 1.0
    Sampling temperature for rollout search; chosen without reported sensitivity analysis.
  • timeout = 10 minutes
    Proof search timeout used for all tools, affecting the comparison.
  • token allocation = 1024/512/512/1024/128
    Token limits for proofs, lemmas, theorem+script, proof state, and output are set by hand and could affect retrieval quality.
assumptions (4)
  • domain assumption Coq's kernel soundly checks generated proofs, so any proof accepted by Coq 8.18 is correct.
    The evaluation treats Coq's proof checking as ground truth; this is standard for proof-assistant research.
  • domain assumption BM-25 similarity over identifiers in proof states is a valid proxy for the usefulness of a proof as context for the next tactic.
    The proof retriever assumes that proof states sharing identifiers indicate relevant proofs; the paper only tests this via end-to-end performance and ablations.
  • domain assumption The benchmark projects did not appear in DeepSeek-Coder's pretraining in a way that inflates Rango's results.
    Acknowledged threat in Section V-H; mitigated only by two post-cutoff projects (Coq-BB5 and PnVRocqLib).
  • domain assumption The 500-theorem ablation set is representative of the full benchmark.
    Ablation conclusions (47% increase from proof retrieval) are drawn from a randomly selected subset; no confidence intervals are reported.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification." pith.science (2026). https://pith.science/paper/37GEVRQX

@misc{pith2026241214063,
  author       = {Pith},
  title        = {Pith review of: Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/37GEVRQX}},
  note         = {Machine review of arXiv:2412.14063}
}
read the original abstract

Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has explored automating proof synthesis using machine learning and large language models (LLMs). This work has shown that identifying relevant premises, such as lemmas and definitions, can aid synthesis. We present Rango, a fully automated proof synthesis tool for Coq that automatically identifies relevant premises and also similar proofs from the current project and uses them during synthesis. Rango uses retrieval augmentation at every step of the proof to automatically determine which proofs and premises to include in the context of its fine-tuned LLM. In this way, Rango adapts to the project and to the evolving state of the proof. We create a new dataset, CoqStoq, of 2,226 open-source Coq projects and 196,929 theorems from GitHub, which includes both training data and a curated evaluation benchmark of well-maintained projects. On this benchmark, Rango synthesizes proofs for 32.0% of the theorems, which is 29% more theorems than the prior state-of-the-art tool Tactician. Our evaluation also shows that Rango adding relevant proofs to its context leads to a 47% increase in the number of theorems proven.

Figures

Figures reproduced from arXiv: 2412.14063 by the authors.

Figure 1
Figure 1. Overview of Rango’s architecture. Rango’s tactic generator uses retrieved relevant proofs and lemmas from the current project as input to an LLM [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
Figure 2
Figure 2. Violin chart over the size of proofs in the training set, benchmark, and [PITH_FULL_IMAGE:figures/full_fig_p005_2.png] view at source ↗
Figure 3
Figure 3. Violin chart over the size of projects contained in the training set, [PITH_FULL_IMAGE:figures/full_fig_p005_3.png] view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Number of Theorems proven by Rango variants over time in seconds. [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 6
Figure 6. Figure 6: Percentage of theorems proven by Rango, Tactician and Proverbot by [PITH_FULL_IMAGE:figures/full_fig_p009_6.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

98 extracted references · 31 canonical work pages

  1. [1]

    https://github.com/ccz181078/Coq-BB5, 2024

    Coq-BB5. https://github.com/ccz181078/Coq-BB5, 2024

    2024

  2. [2]

    https://github.com/PnVDiscord/PnVRocqLib, 2024

    PnVRocqLib. https://github.com/PnVDiscord/PnVRocqLib, 2024

    2024

  3. [3]

    Afzal, M

    A. Afzal, M. Motwani, K. T. Stolee, Y . Brun, and C. Le Goues. SOSRepair: Expressive semantic search for real-world program repair. IEEE Transactions on Software Engineering (TSE) , 47(10), 2021. doi: 10.1109/TSE.2019.2944914

    work page arXiv 2021

  4. [4]

    Albarghouthi, L

    A. Albarghouthi, L. D’Antoni, S. Drews, and A. Nori. FairSquare: Probabilistic verification for program fairness. In ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA), 2017

    2017

  5. [5]

    Ammann and J

    P. Ammann and J. Offutt. Introduction to Software Testing . Cambridge University Press, 1 ed., 2008

    2008

  6. [6]

    C. An, Z. Chen, Q. Ye, E. First, L. Peng, J. Zhang, Z. Wang, S. Lerner, and J. Shang. Learn from failure: Fine-tuning LLMs with trial-and-error data for intuitionistic propositional logic proving. CoRR, abs/2404.07382, 2024

    arXiv 2024

  7. [7]

    Azerbayev, B

    Z. Azerbayev, B. Piotrowski, and J. Avigad. ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems. In Toward Human-Level Mathematical Reasoning , 2022

    2022

  8. [8]

    Azerbayev, H

    Z. Azerbayev, H. Schoelkopf, K. Paster, M. D. Santos, S. McAleer, A. Q. Jiang, J. Deng, S. Biderman, and S. Welleck. Llemma: An open language model for mathematics. CoRR, abs/2310.10631, 2023

    arXiv 2023

Show all 98 references
  1. [9]

    Bansal, C

    K. Bansal, C. Szegedy, M. Rabe, S. Loos, and V . Toman. Learning to reason in large theories without imitation. CoRR, abs/1905.10501, 2019

    1905 arXiv

  2. [10]

    Blaauwbroek, M

    L. Blaauwbroek, M. Ol ˇs´ak, J. Rute, F. I. S. Massolo, J. Piepenbrock, and V . Pestun. Graph2Tac: Online representation learning of formal math concepts. In International Conference on Machine Learning , 2024. 11

    2024

  3. [11]

    Y . Brun, R. Holmes, M. D. Ernst, and D. Notkin. Speculative analysis: Exploring future states of software. In Future of Software Engineering Research (FoSER), pp. 59–63, 2010. doi: 10.1145/1882362.1882375

    2010

  4. [12]

    Brun and A

    Y . Brun and A. Meliou. Software fairness. In ESEC/FSE NIER Track, pp. 754–759, 2018. doi: 10.1145/3236024.3264838

    2018

  5. [13]

    Carrott, N

    P. Carrott, N. Saavedra, K. Thompson, S. Lerner, J. F. Ferreira, and E. First. CoqPyt: Proof navigation in Python in the era of LLMs. In Foundations of Software Engineering (FSE) Demo Track , 2024

    2024

  6. [14]

    Chakraborty, G

    S. Chakraborty, G. Ebner, S. Bhat, S. Fakhoury, S. Fatima, S. Lahiri, and N. Swamy. Towards neural synthesis for SMT-assisted proof-oriented programming. CoRR, abs/2405.01787, 2024

    2024 arXiv

  7. [15]

    J. Chen, H. Lin, X. Han, and L. Sun. Benchmarking large language models in retrieval-augmented generation. In AAAI Conference on Artificial Intelligence, vol. 38, pp. 17754–17762, 2024

    2024

  8. [16]

    Chowdhery et al

    A. Chowdhery et al. PaLM: Scaling language modeling with pathways. CoRR, abs/2204.02311, 2022

    2022 arXiv

  9. [17]

    https://github.com/coq-community, 2024

    Coq-Community. https://github.com/coq-community, 2024

    2024

  10. [18]

    Czajka and C

    Ł . Czajka and C. Kaliszyk. Hammer for Coq: Automation for dependent type theory. Journal of Automated Reasoning , 61(1-4):423–453, 2018. doi: 10.1007/s10817-018-9458-4

    2018 doi

  11. [19]

    de Moura and N

    L. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems . 2008. doi: 10. 1007/978-3-540-78800-3 24

    2008

  12. [20]

    de Moura and S

    L. de Moura and S. Ullrich. The Lean 4 theorem prover and programming language. In International Conference on Automated Deduction , 2021

    2021

  13. [21]

    Eladawy, C

    H. Eladawy, C. Le Goues, and Y . Brun. Automated program repair, what is it good for? Not absolutely nothing! In ICSE, pp. 1017–1029, 2024. doi: 10.1145/3597503.3639095

    2024

  14. [22]

    Endres, S

    M. Endres, S. Fakhoury, S. Chakraborty, and S. K. Lahiri. Can large language models transform natural language intent into formal method postconditions? Proceedings of the ACM Software Engineering (PACMSE), 1(FSE):84:1–84:24, July 2024. doi: 10.1145/3660791

    2024 doi

  15. [23]

    Z. Feng, D. Guo, D. Tang, N. Duan, X. Feng, M. Gong, L. Shou, B. Qin, T. Liu, D. Jiang, et al. Codebert: A pre-trained model for programming and natural languages. CoRR, abs/2002.08155, 2020

    2002 arXiv

  16. [24]

    First and Y

    E. First and Y . Brun. Diversity-driven automated formal verification. In ICSE, 2022. doi: 10.1145/3510003.3510138

    2022

  17. [25]

    First, Y

    E. First, Y . Brun, and A. Guha. TacTok: Semantics-aware proof synthesis. Proceedings of the ACM on Programming Languages (PACMPL), 4, 2020. doi: 10.1145/3428299

    2020 doi

  18. [26]

    First, M

    E. First, M. Rabe, T. Ringer, and Y . Brun. Baldur: Whole-proof generation and repair with large language models. In ESEC/FSE, pp. 1229–1241, 2023. doi: 10.1145/3611643.3616243

    2023

  19. [27]

    Galhotra, Y

    S. Galhotra, Y . Brun, and A. Meliou. Fairness testing: Testing software for discrimination. In ESEC/FSE, pp. 498–510, 2017. doi: 10.1145/3106237 .3106277

    2017 doi

  20. [28]

    Gauthier, C

    T. Gauthier, C. Kaliszyk, and J. Urban. TacticToe: Learning to reason with HOL4 tactics. In International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) , vol. 46, pp. 125–143, 2017

    2017

  21. [29]

    Giguere, B

    S. Giguere, B. Metevier, Y . Brun, B. C. da Silva, P. S. Thomas, and S. Niekum. Fairness guarantees under demographic shift. In International Conference on Learning Representations (ICLR) , April 2022

    2022

  22. [30]

    Goffi, A

    A. Goffi, A. Gorla, M. D. Ernst, and M. Pezz `e. Automatic generation of oracles for exceptional behaviors. In International Symposium on Software Testing and Analysis (ISSTA) , pp. 213–224, July 2016. doi: 10. 1145/2931037.2931061

    2016

  23. [31]

    D. Guo, Q. Zhu, D. Yang, Z. Xie, K. Dong, W. Zhang, G. Chen, X. Bi, Y . Wu, Y . Li, et al. DeepSeek-Coder: When the large language model meets programming–the rise of code intelligence. CoRR, abs/2401.14196, 2024

    2024 arXiv

  24. [32]

    J. M. Han, J. Rute, Y . Wu, E. W. Ayers, and S. Polu. Proof artifact co-training for theorem proving with language models. CoRR, 2021

    2021

  25. [33]

    A. Hoag, J. Kostas, B. C. da Silva, P. Thomas, and Y . Brun. Seldonian toolkit: Building software with safe and fair machine learning. In ICSE Demo, 2023. doi: 10.1109/ICSE-Companion58688.2023.00035

    2023

  26. [34]

    E. J. Hu, Y . Shen, P. Wallis, Z. Allen-Zhu, Y . Li, S. Wang, L. Wang, and W. Chen. Lora: Low-rank adaptation of large language models. CoRR, abs/2106.09685, 2021

    2021 arXiv

  27. [35]

    Huang, P

    D. Huang, P. Dhariwal, D. Song, and I. Sutskever. GamePad: A learning environment for theorem proving. CoRR, abs/1806.00608, 2018

    2018 arXiv

  28. [36]

    Jiang, K

    A. Jiang, K. Czechowski, M. Jamnik, P. Milos, S. Tworkowski, W. Li, and Y . T. Wu. Thor: Wielding hammers to integrate language models and automated theorem provers. In Neural Information Processing Systems (NeurIPS). New Orleans, LA, USA, 2022

    2022

  29. [37]

    A. Q. Jiang, W. Li, J. M. Han, and Y . Wu. LISA: Language models of ISAbelle proofs. In Conference on Artificial Intelligence and Theorem Proving (AITP), pp. 17.1–17.3, September 2021

    2021

  30. [38]

    A. Q. Jiang, S. Welleck, J. P. Zhou, T. Lacroix, J. Liu, W. Li, M. Jamnik, G. Lample, and Y . Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference on Learning Representations , 2023

    2023

  31. [39]

    Jiang, Y

    J. Jiang, Y . Xiong, H. Zhang, Q. Gao, and X. Chen. Shaping program repair space with existing patches and similar code. In ACM/SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) , pp. 298–309, July 2018. doi: 10.1145/3213846.3213871

    2018

  32. [40]

    Johnson, Y

    B. Johnson, Y . Brun, and A. Meliou. Causal testing: Understanding defects’ root causes. In ICSE, 2020. doi: 10.1145/3377811.3380377

    2020

  33. [41]

    Karpukhin, B

    V . Karpukhin, B. O˘guz, S. Min, P. Lewis, L. Wu, S. Edunov, D. Chen, and W.-t. Yih. Dense passage retrieval for open-domain question answering. CoRR, abs/2004.04906, 2020

    2004 arXiv

  34. [42]

    D. P. Kingma and J. Ba. Adam: A method for stochastic optimization. CoRR, abs/1412.6980, 2014

    2014 arXiv

  35. [43]

    H. Krasner. The cost of poor software quality in the us: A 2020 report. Proc. Consortium Inf. Softw. QualityTM (CISQTM) , 2, 2021

    2020

  36. [44]

    Lample, T

    G. Lample, T. Lacroix, M.-A. Lachaux, A. Rodriguez, A. Hayat, T. Lavril, G. Ebner, and X. Martinet. Hypertree proof search for neural theorem proving. Advances in Neural Information Processing Systems , 35:26337– 26349, 2022

    2022

  37. [45]

    Lasse, J

    B. Lasse, J. Urban, and H. Geuvers. The Tactician: A seamless, interactive tactic learner and prover for Coq. In International Conference on Intelligent Computer Mathematics (CICM) , pp. 271–277, 2020. doi: 10.1007/978-3-030-53518-6 17

    2020 doi

  38. [46]

    Le Goues, M

    C. Le Goues, M. Pradel, and A. Roychoudhury. Automated program repair. Communications of the ACM , 62(12):56–65, Nov. 2019. doi: 10. 1145/3318162

    2019

  39. [47]

    X. Leroy. Formal certification of a compiler back-end or: Programming a compiler with a proof assistant. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) , pp. 42–54, 2006. doi: 10.1145/1111037.1111042

    2006

  40. [48]

    X. Leroy. Formal verification of a realistic compiler. Communications of the ACM (CACM), 52(7):107–115, 2009. doi: 10.1145/1538788.1538814

    2009

  41. [49]

    Lewis, E

    P. Lewis, E. Perez, A. Piktus, F. Petroni, V . Karpukhin, N. Goyal, H. K ¨uttler, M. Lewis, W.-t. Yih, T. Rockt ¨aschel, et al. Retrieval- augmented generation for knowledge-intensive nlp tasks. Advances in Neural Information Processing Systems , 33:9459–9474, 2020

    2020

  42. [50]

    J. A. Li, Y . Li, G. Li, X. Hu, X. Xia, and Z. Jin. Editsum: A retrieve-and- edit framework for source code summarization. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE) , pp. 155–166. IEEE, 2021

    2021

  43. [51]

    K. Liu, A. Koyuncu, D. Kim, and T. F. Bissyand ´e. TBar: Revisiting template-based automated program repair. In ACM SIGSOFT Interna- tional Symposium on Software Testing and Analysis (ISSTA) , pp. 31–42,

  44. [52]

    Megill and D

    N. Megill and D. A. Wheeler. Metamath: a computer language for mathematical proofs. Lulu. com, 2019

    2019

  45. [53]

    Metevier, S

    B. Metevier, S. Giguere, S. Brockman, A. Kobren, Y . Brun, E. Brunskill, and P. S. Thomas. Offline contextual bandits with high probability fairness guarantees. In Annual Conference on Neural Information Processing Systems (NeurIPS), Advances in Neural Information Processing S...

    2019

  46. [54]

    Mikuła, S

    M. Mikuła, S. Antoniak, S. Tworkowski, A. Q. Jiang, J. P. Zhou, C. Szegedy, Łukasz Kuci ´nski, P. Miło ´s, and Y . Wu. Magnushammer: A Transformer-based Approach to Premise Selection, 2023

    2023

  47. [55]

    Mirchev, A

    M. Mirchev, A. Costea, A. K. Singh, and A. Roychoudhury. Assured au- tomatic programming via large language models. CoRR, abs/2410.18494, 2024

    2024 arXiv

  48. [56]

    Motwani and Y

    M. Motwani and Y . Brun. Automatically generating precise oracles from structured natural language specifications. In ICSE, pp. 188–199, May

  49. [57]

    Motwani and Y

    M. Motwani and Y . Brun. Better automatic program repair by using bug reports and tests together. In ICSE, pp. 1229–1241, May 2023. doi: 10. 1109/ICSE48619.2023.00109

    2023

  50. [58]

    doi: 10.1109/ICSE.2019.00035

    2019

  51. [59]

    Mu s ¸lu, Y

    K. Mu s ¸lu, Y . Brun, and A. Meliou. Data debugging with continuous testing. In ESEC/FSE NI Track , pp. 631–634, August 2013. doi: 10. 1145/2491411.2494580

    2013

  52. [60]

    Motwani, M

    M. Motwani, M. Soto, Y . Brun, R. Just, and C. Le Goues. Quality of automated program repair on real-world defects. IEEE Transactions on Software Engineering (TSE) , 48(2):637–661, February 2022. doi: 10. 1109/TSE.2020.2998785 12

    2022

  53. [61]

    Nashid, M

    N. Nashid, M. Sintaha, and A. Mesbah. Retrieval-based prompt selection for code-related few-shot learning. In ICSE, pp. 2450–2462, 2023

    2023

  54. [62]

    Mus ¸lu, Y

    K. Mus ¸lu, Y . Brun, and A. Meliou. Preventing data errors with continuous testing. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA) , pp. 373–384, July 2015. doi: 10.1145/2771783. 2771792

    2015 doi

  55. [63]

    D. H. O’Dell. The debugging mindset: Understanding the psychology of learning strategies leads to effective problem-solving skills. Queue, 15(1):71–90, Feb. 2017. doi: 10.1145/3055301.3068754

    2017

  56. [64]

    Nipkow, L

    T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL: A proof assistant for higher-order logic , vol. 2283. Springer Science & Business Media, 2002

    2002

  57. [65]

    Fully Sharded Data Parallel: faster AI training with fewer GPUs

    Ott, Myle and Shleifer, Sam and Xu, Min and Goyal, Priya and Duval, Quentin and Caggiano, Vittorio. Fully Sharded Data Parallel: faster AI training with fewer GPUs. https://engineering.fb.com/2021/07/15/ open-source/fsdp/, 2021

    2021

  58. [66]

    GPT-4 technical report

    OpenAI. GPT-4 technical report. CoRR, abs/2303.08774, 2023

    2023 arXiv

  59. [67]

    M. R. Parvez, W. Ahmad, S. Chakraborty, B. Ray, and K.-W. Chang. Retrieval augmented code generation and summarization. In Findings of the Association for Computational Linguistics: EMNLP 2021 , pp. 2719–2734, 2021

    2021

  60. [68]

    Paliwal, S

    A. Paliwal, S. M. Loos, M. N. Rabe, K. Bansal, and C. Szegedy. Graph representations for higher-order logic and theorem proving. In Conference on Artificial Intelligence (AAAI) , pp. 2967–2974. AAAI Press, 2020

    2020

  61. [69]

    S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. Formal mathematics statement curriculum learning. In International Conference on Learning Representations (ICLR) , 2023

    2023

  62. [70]

    Paulson and T

    L. Paulson and T. Nipkow. The Sledgehammer: Let automatic theorem provers write your Isabelle scripts! https://isabelle.in.tum.de/ website-Isabelle2009-1/sledgehammer.html, 2023

    2023

  63. [71]

    Ringer, A

    T. Ringer, A. Sanchez-Stern, D. Grossman, and S. Lerner. REPLica: REPL instrumentation for Coq analysis. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP) , pp. 99–113, 2020. doi: 10.1145/3372885.3373823

    2020

  64. [72]

    Polu and I

    S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. CoRR, 2020

    2020

  65. [73]

    Sanchez-Stern, Y

    A. Sanchez-Stern, Y . Alhessi, L. Saul, and S. Lerner. Generating correctness proofs with neural networks. In ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL) , pp. 1–10, 2020

    2020

  66. [74]

    Robertson, H

    S. Robertson, H. Zaragoza, et al. The probabilistic relevance framework: BM25 and beyond. Foundations and Trends® in Information Retrieval , 3(4):333–389, 2009

    2009

  67. [75]

    Sanchez-Stern, A

    A. Sanchez-Stern, A. Varghese, Z. Kaufman, D. Zhang, T. Ringer, and Y . Brun. QEDCartographer: Automating formal verification using reward- free reinforcement learning. In ICSE, April 2025

    2025

  68. [76]

    Sanchez-Stern, E

    A. Sanchez-Stern, E. First, T. Zhou, Z. Kaufman, Y . Brun, and T. Ringer. Passport: Improving automated formal verification using identifiers. ACM Transactions on Programming Languages and Systems (TOPLAS) , 45(2):12:1–12:30, June 2023. doi: 10.1145/3593374

    2023 doi

  69. [77]

    Sparck Jones

    K. Sparck Jones. A statistical interpretation of term specificity and its application in retrieval. Journal of documentation , 28(1):11–21, 1972

    1972

  70. [78]

    E. K. Smith, E. Barr, C. Le Goues, and Y . Brun. Is the cure worse than the disease? Overfitting in automated program repair. In ESEC/FSE, pp. 532–543, September 2015. doi: 10.1145/2786805.2786825

    2015

  71. [79]

    Thakur, Y

    A. Thakur, Y . Wen, and S. Chaudhuri. A Language-Agent Approach to Formal Theorem-Proving, 2023

    2023

  72. [80]

    G. Team, R. Anil, S. Borgeaud, Y . Wu, J.-B. Alayrac, J. Yu, R. Soricut, J. Schalkwyk, A. M. Dai, A. Hauth, et al. Gemini: A family of highly capable multimodal models. CoRR, abs/2312.11805, 2023

    2023 arXiv

  73. [81]

    P. S. Thomas, B. C. da Silva, A. G. Barto, S. Giguere, Y . Brun, and E. Brunskill. Preventing undesirable behavior of intelligent machines. Science, 366(6468):999–1004, 22 November 2019. doi: 10.1126/science. aag3311

    2019 doi

  74. [82]

    Coq, v.8.7

    The Coq Development Team. Coq, v.8.7. https://coq.inria.fr, 2017

    2017

  75. [83]

    Grimm, J

    V´eronique Cortier, N. Grimm, J. Lallemand, and M. Maffei. A type system for privacy properties. In ACM SIGSAC Conference on Computer and Communications Security (CCS) , pp. 409–423. Association for Computing Machinery, 2017. doi: 10.1145/3133956.3133998

    2017

  76. [84]

    Touvron et al

    H. Touvron et al. Llama 2: Open foundation and fine-tuned chat models. CoRR, abs/2307.09288, 2023

    2023 arXiv

  77. [85]

    W. Wang, Y . Wang, S. Joty, and S. C. Hoi. Rap-gen: Retrieval-augmented patch generation with codet5 for automatic program repair. In ESEC/FSE, pp. 146–158, 2023

    2023

  78. [86]

    H. Wang, H. Xin, C. Zheng, Z. Liu, Q. Cao, Y . Huang, J. Xiong, H. Shi, E. Xie, J. Yin, et al. Lego-prover: Neural theorem proving with growing libraries. In The Twelfth International Conference on Learning Representations, 2024

    2024

  79. [87]

    M. Wu, M. Norrish, C. Walder, and A. Dezfouli. TacticZero: Learning to prove theorems from scratch with deep reinforcement learning. CoRR, abs/2102.09756, 2021

    2021 arXiv

  80. [88]

    Weiss, A

    A. Weiss, A. Guha, and Y . Brun. Tortoise: Interactive system config- uration repair. In IEEE/ACM International Conference on Automated Software Engineering (ASE) , pp. 625–636, October/November 2017. doi: 10.1109/ASE.2017.8115673

    2017

  81. [89]

    H. Xin, D. Guo, Z. Shao, Z. Ren, Q. Zhu, B. Liu, C. Ruan, W. Li, and X. Liang. DeepSeek-Prover: Advancing theorem proving in llms through large-scale synthetic data. CoRR, abs/2405.14333, 2024

    2024 arXiv

  82. [90]

    Y . Wu, A. Q. Jiang, W. Li, M. Rabe, C. Staats, M. Jamnik, and C. Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems , 35:32353–32368, 2022

    2022

  83. [91]

    K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models, 2023

    2023

  84. [92]

    Yang and J

    K. Yang and J. Deng. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning (ICML), 2019

    2019

  85. [93]

    Zeller and R

    A. Zeller and R. Hildebrandt. Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering , 28(2):183–200, February 2002. doi: 10.1109/32.988498

    2002 doi

  86. [94]

    X. Yang, Y . Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) , pp. 283–294, 2011. doi: 10.1145/1993498.1993532

    2011

  87. [95]

    Zheng, H

    C. Zheng, H. Wang, E. Xie, Z. Liu, J. Sun, H. Xin, J. Shen, Z. Li, and Y . Li. Lyra: Orchestrating dual correction in automated theorem proving. CoRR, abs/2309.15806, 2023

    2023 arXiv

  88. [96]

    J. Zhai, Y . Shi, M. Pan, G. Zhou, Y . Liu, C. Fang, S. Ma, L. Tan, and X. Zhang. C2S: Translating natural language comments to formal program specifications. In ESEC/FSE, pp. 25–37, 2020. doi: 10.1145/3368089. 3409716

    2020 doi

  89. [98]

    Q. Zhu, Z. Sun, Y . an Xiao, W. Zhang, K. Yuan, Y . Xiong, and L. Zhang. A syntax-guided edit decoder for neural program repair. In ESEC/FSE, pp. 341–353, 2021. doi: 10.1145/3468264.3468544 13

    2021

  90. [2019]

    doi: 10.1145/3293882.3330577

Pith tools

Reviewed August 11, 2026 · model on record in the stance chip above.