Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

📄 arXiv: 2412.14063v3 📥 PDF

作者: Kyle Thompson, Nuno Saavedra, Pedro Carrott, Kevin Fisher, Alex Sanchez-Stern, Yuriy Brun, João F. Ferreira, Sorin Lerner, Emily First

分类: cs.SE, cs.AI

发布日期: 2024-12-18 (更新: 2025-01-28)

备注: In Proceedings of the 47th International Conference on Software Engineering (ICSE), Ottawa, ON, Canada, April 2025

💡 一句话要点

Rango：自适应检索增强证明，用于自动化软件验证。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化验证 自动化证明 检索增强 大型语言模型 Coq 软件验证 定理证明 CoqStoq数据集

📋 核心要点

  1. 形式化验证依赖专家知识和手动证明，自动化证明合成面临挑战。
  2. Rango通过检索相关前提和相似证明，增强LLM的证明能力，实现自适应证明。
  3. 实验表明，Rango在CoqStoq基准上显著优于现有技术，证明成功率提升29%。

📝 摘要（中文）

本文提出Rango，一个用于Coq的形式化验证的全自动证明合成工具。Rango在证明的每一步都使用检索增强，自动确定在微调的LLM上下文中包含哪些证明和前提。通过这种方式，Rango能够适应项目和证明的演进状态。作者构建了一个新的数据集CoqStoq，包含来自GitHub的2,226个开源Coq项目和196,929个定理，其中包括训练数据和一个精心策划的、维护良好的项目评估基准。在该基准上，Rango合成了32.0%的定理的证明，比之前的最先进工具Tactician多29%。评估还表明，Rango通过向其上下文中添加相关证明，使证明的定理数量增加了47%。

🔬 方法详解

问题定义：论文旨在解决使用Coq等证明辅助工具进行形式化验证时，需要大量人工干预和专业知识的问题。现有方法，如Tactician，在自动化证明合成方面存在局限性，尤其是在识别和利用相关前提（如引理和定义）方面表现不足，导致证明效率低下。

核心思路：Rango的核心思路是在证明过程中，利用检索增强技术，动态地从现有项目和证明中检索相关信息，并将其融入到LLM的上下文中。这样，LLM可以更好地理解当前证明状态，并生成更有效的证明策略。这种自适应检索机制使得Rango能够根据项目的具体情况和证明的演进状态进行调整。

技术框架：Rango的整体框架包含以下几个主要模块：1) CoqStoq数据集：用于训练和评估Rango的数据集，包含大量Coq项目和定理。2) 检索模块：负责从CoqStoq数据集中检索与当前证明状态相关的引理、定义和相似证明。3) LLM：一个经过微调的LLM，用于生成证明策略。4) 证明合成模块：利用LLM生成的策略，尝试完成证明。在证明的每一步，检索模块都会更新LLM的上下文，使其包含最相关的信息。

关键创新：Rango的关键创新在于其自适应检索增强机制。与以往方法不同，Rango不是静态地选择一组前提，而是在证明的每一步都动态地检索相关信息。这种动态检索使得Rango能够更好地适应证明的演进状态，并利用最相关的信息。此外，CoqStoq数据集的构建也为自动化证明合成的研究提供了宝贵资源。

关键设计：Rango的关键设计包括：1) 检索策略：如何有效地检索相关引理、定义和相似证明。2) LLM微调：如何微调LLM，使其能够更好地理解Coq代码和证明策略。3) 上下文构建：如何将检索到的信息有效地融入到LLM的上下文中。具体的技术细节，例如检索算法、LLM架构和损失函数等，论文中可能没有详细描述，属于未知信息。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

Rango在CoqStoq基准上取得了显著的性能提升，证明成功率达到32.0%，比之前的最先进工具Tactician高出29%。此外，实验结果表明，通过向LLM上下文中添加相关证明，Rango证明的定理数量增加了47%。这些结果表明，Rango的自适应检索增强机制能够有效地提高自动化证明合成的性能。

🎯 应用场景

Rango的应用场景包括自动化软件验证、形式化方法教育和Coq项目开发。它可以帮助开发者更轻松地验证软件的正确性，降低软件缺陷的风险。在教育领域，Rango可以作为辅助工具，帮助学生学习形式化方法和Coq证明。此外，Rango还可以加速Coq项目的开发过程，提高开发效率。

📄 摘要（原文）

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.