Formal verification using proof assistants, such as Coq, allows for high-quality software. However, the verification process is expensive, requiring significant expertise and manual effort to write proofs. Recent work has explored automating proof synthesis using machine learning, and even more recently, large language models (LLMs), showing that retrieving relevant premises (such as lemmas and definitions) is helpful for these models. We present Rango, a fully automated proof synthesis tool for Coq that uses, not only relevant premises but also similar proofs from the current project. 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,205 open-source Coq projects from GitHub, which includes both training data and a curated evaluation benchmark of well-maintained projects. On this benchmark, Rango synthesizes 27.7% of the proofs, which is 10% more proofs than prior state-of-the-art tool Tactician. Our evaluation also shows that adding relevant proofs to the context in Rango leads to a 45% increase in the number of theorems proven.
@inproceedings{Thompson25icse,
author = {Robert Thompson and Nuno Saavedra and Pedro Carrott and
Kevin Fisher and Alex Sanchez-Stern and Yuriy Brun and João F. Ferreira and
Sorin Lerner and Emily First},
title =
{\href{http://people.cs.umass.edu/brun/pubs/pubs/Thompson25icse.pdf}{Rango:
{Adaptive} Retrieval-Augmented Proving for Automated Software Verification}},
booktitle = {Proceedings of the 47th International Conference on Software Engineering (ICSE)},
venue = {ICSE},
address = {Ottowa, ON, Canada},
month = {April},
date = {28--30},
year = {2025},
accept = {$\frac{66}{662} \approx 10\%$ (2nd cycle direct accept, without revision)},
abstract = {<p>Formal verification using proof assistants, such as Coq, allows for
high-quality software. However, the verification process is expensive,
requiring significant expertise and manual effort to write proofs. Recent
work has explored automating proof synthesis using machine learning, and even
more recently, large language models (LLMs), showing that retrieving relevant
premises (such as lemmas and definitions) is helpful for these models. We
present Rango, a fully automated proof synthesis tool for Coq that uses, not
only relevant premises but also similar proofs from the current project.
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,205 open-source
Coq projects from GitHub, which includes both training data and a curated
evaluation benchmark of well-maintained projects. On this benchmark, Rango
synthesizes 27.7% of the proofs, which is 10% more proofs than prior
state-of-the-art tool Tactician. Our evaluation also shows that adding
relevant proofs to the context in Rango leads to a 45% increase in the number
of theorems proven.</p>},
}