AutoVerus: Automated Proof Generation for Rust Code

📄 arXiv: 2409.13082v3 📥 PDF

作者: Chenyuan Yang, Xuheng Li, Md Rakib Hossain Misu, Jianan Yao, Weidong Cui, Yeyun Gong, Chris Hawblitzel, Shuvendu Lahiri, Jacob R. Lorch, Shuai Lu, Fan Yang, Ziqiao Zhou, Shan Lu

分类: cs.SE, cs.AI, cs.FL

发布日期: 2024-09-19 (更新: 2025-08-22)

备注: OOPSLA 2025

DOI: 10.1145/3763174

💡 一句话要点

AutoVerus：利用LLM自动生成Rust代码正确性证明

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

关键词: Rust代码验证 自动证明生成 大型语言模型 LLM代理 形式化验证

📋 核心要点

  1. 基于LLM的代码生成取得了显著进展，但基于LLM的证明生成仍处于起步阶段，面临诸多挑战。
  2. AutoVerus通过构建LLM代理网络，模拟人类专家构建证明的三个阶段，实现Rust代码正确性证明的自动生成。
  3. 实验结果表明，AutoVerus在150个证明任务的基准测试中，成功生成超过90%任务的正确证明。

📝 摘要（中文）

本文提出AutoVerus，一个利用大型语言模型（LLM）自动生成Rust代码正确性证明的系统。AutoVerus的设计与Verus的特性相匹配，Verus是一个验证工具，它使用Rust编写的证明和规范来证明Rust代码的正确性。AutoVerus由LLM代理网络组成，这些代理经过精心设计和编排，以模仿人类专家构建证明的三个阶段：初步证明生成、通用提示指导下的证明细化以及验证错误指导下的证明调试。为了全面评估AutoVerus并促进未来在该方向的研究，我们基于现有的代码生成和验证基准，构建了一个包含150个重要的证明任务的基准测试套件。评估结果表明，AutoVerus可以自动生成超过90%任务的正确证明，其中一半以上的任务在不到30秒或3次LLM调用内完成。

🔬 方法详解

问题定义：论文旨在解决Rust代码正确性证明的自动化生成问题。现有方法依赖人工编写证明，耗时且容易出错。大型语言模型在代码生成方面表现出色，但在自动生成代码正确性证明方面仍存在差距，缺乏针对验证工具的有效利用。

核心思路：论文的核心思路是模仿人类专家构建证明的过程，将证明生成分解为初步生成、细化和调试三个阶段，并利用大型语言模型构建相应的代理来执行这些阶段。通过迭代优化，逐步逼近正确的证明。

技术框架：AutoVerus的技术框架包含一个LLM代理网络，该网络模拟人类专家构建证明的三个阶段： 1. 初步证明生成：利用LLM生成初始的证明草案。 2. 证明细化：根据通用提示（例如，添加循环不变式）指导LLM细化证明。 3. 证明调试：根据验证工具（Verus）返回的错误信息，指导LLM调试和修复证明。 这三个阶段循环迭代，直到生成正确的证明或达到最大迭代次数。

关键创新：AutoVerus的关键创新在于将证明生成过程分解为多个阶段，并针对每个阶段设计了专门的LLM代理。这种模块化的设计使得系统能够更好地利用LLM的能力，并有效地解决证明生成中的各种挑战。此外，AutoVerus还针对Verus验证工具的特点进行了优化，使其能够更好地与Verus协同工作。

关键设计：AutoVerus的关键设计包括： 1. LLM选择：选择合适的LLM作为各个代理的基础模型。 2. 提示工程：设计有效的提示，指导LLM生成、细化和调试证明。 3. 迭代策略：设计合理的迭代策略，控制证明生成的流程。 4. 错误分析：设计有效的错误分析机制，从Verus的错误信息中提取有用的信息，指导LLM进行调试。

🖼️ 关键图片

img_0
img_1
img_2

📊 实验亮点

AutoVerus在包含150个证明任务的基准测试中表现出色，能够自动生成超过90%任务的正确证明。更令人印象深刻的是，超过一半的任务在不到30秒或3次LLM调用内完成。这表明AutoVerus具有很高的效率和准确性，能够显著提高Rust代码验证的效率。

🎯 应用场景

AutoVerus可应用于软件开发过程中的代码验证环节，提高代码质量和可靠性。它可以帮助开发者自动生成Rust代码的正确性证明，减少人工验证的工作量，并降低代码错误的风险。该研究成果对于构建更安全、更可靠的软件系统具有重要意义，尤其是在安全攸关的应用领域，如操作系统、区块链和嵌入式系统。

📄 摘要（原文）

Generative AI has shown its values for many software engineering tasks. Still in its infancy, large language model (LLM)-based proof generation lags behind LLM-based code generation. In this paper, we present AutoVerus. AutoVerus uses LLMs to automatically generate correctness proof for Rust code. AutoVerus is designed to match the unique features of Verus, a verification tool that can prove the correctness of Rust code using proofs and specifications also written in Rust. AutoVerus consists of a network of LLM agents that are crafted and orchestrated to mimic human experts' three phases of proof construction: preliminary proof generation, proof refinement guided by generic tips, and proof debugging guided by verification errors. To thoroughly evaluate AutoVerus and help foster future research in this direction, we have built a benchmark suite of 150 non-trivial proof tasks, based on existing code-generation benchmarks and verification benchmarks. Our evaluation shows that AutoVerus can automatically generate correct proof for more than 90% of them, with more than half of them tackled in less than 30 seconds or 3 LLM calls.