Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

TL;DR

Rango tackles the high cost of formal verification by introducing adaptive retrieval-augmented proving for Coq, which continually retrieves in-project proofs and lemmas to guide a fine-tuned decoder-only LM at every proof step. The approach, tested on the CoqStoq dataset, outperforms prior proof synthesis tools and yields a substantial increase in proven theorems when incorporating retrieved proofs. Key contributions include the dual retriever architecture (proof and lemma retrievers), a rollout-based search strategy, and the CoqStoq dataset of 2,226 repositories, 196,929 theorems, and 2,225,515 proof steps. This work has practical impact for reducing the effort required for formal verification by leveraging local project knowledge through retrieval-augmented reasoning and may generalize to other proof systems.

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 (6)

• 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 (along with the theorem, current proof state, and proof script so far) to predict the next tactic. Rango's searcher uses the tactic predictions to attempt to synthesize a complete proof. A proof attempt is correct if Coq determines that it has no errors and there are no more goals left to solve.
• Figure 2: Violin chart over the size of proofs in the training set, benchmark, and validation set. Proof size is the number of steps in the proof. The quartiles are indicated near the corresponding dashed lines.
• Figure 3: Violin chart over the size of projects contained in the training set, benchmark, and validation set. Project size is the number of proofs in the project. The quartiles are indicated near the corresponding dashed lines.
• Figure 4: Number of Theorems proven by Rango variants over time in seconds.
• Figure 5: Percentage of theorems proven by Rango, Tactician, and Proverbot by the length of the human-written proof.