一句话：提出 Rango，用检索增强的微调 LLM 在 Coq 中自动识别相关前提与相似证明，实现全自动证明合成。
使用 Coq 等证明助手进行形式验证可以产出高质量软件，但编写证明需要大量专业知识与手工劳动。近期工作尝试用机器学习和 LLM 自动合成证明，并发现识别相关前提（引理、定义）有助于合成。本文提出 Rango，一个面向 Coq 的全自动证明合成工具：它在证明的每一步都使用检索增强，自动从当前项目中找出相关前提与相似证明，并将其放入微调 LLM 的上下文中，从而同时适应当前项目与不断演化的证明状态。作者构建了新数据集 CoqStoq，涵盖 GitHub 上 2,226 个开源 Coq 项目、196,929 条定理，既包含训练数据，也包含由维护良好的项目构成的评测基准。在该基准上，Rango 为 32.0% 的定理合成出证明，比此前最先进的工具 Tactician 多证明 29% 的定理；评估还表明，把相关证明加入上下文可使被证明的定理数量提升 47%。
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.
DOI 原文 ·
@inproceedings{paperbot8712,
title = {Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification},
author = {Kyle 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},
booktitle = {ICSE},
year = {2025},
doi = {10.1109/icse55347.2025.00161}
}