Laurel: Unblocking Automated Verification with Large Language Models

📄 arXiv: 2405.16792v2 📥 PDF

作者: Eric Mugnier, Emmanuel Anaya Gonzalez, Ranjit Jhala, Nadia Polikarpova, Yuanyuan Zhou

分类: cs.LO, cs.AI

发布日期: 2024-05-27 (更新: 2025-03-03)

备注: 34 pages, accepted at OOPSLA 25

💡 一句话要点

Laurel：利用大语言模型自动生成断言，解决程序验证中的阻塞问题

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

关键词: 程序验证 大语言模型 断言生成 SMT求解器 形式化方法

📋 核心要点

  1. 程序验证依赖SMT求解器，但求解器常需人工提示（断言），增加了工程师负担。
  2. Laurel利用LLM自动生成断言，通过错误信息定位和代码相似性选择示例断言。
  3. 在DafnyGym基准测试中，Laurel仅需几次尝试即可生成超过56.6%的所需断言。

📝 摘要（中文）

程序验证器（如Dafny）通过将证明外包给SMT求解器来实现自动化验证。然而，这种自动化并非完美，求解器通常需要断言形式的提示，这给证明工程师带来了负担。本文提出了Laurel，一种通过使用大型语言模型（LLM）自动生成断言来减轻这种负担的工具。为了提高LLM在此任务中的成功率，我们设计了两种特定领域的提示技术。首先，我们通过分析验证器的错误消息并在该位置插入断言占位符来帮助LLM确定缺失断言的位置。其次，我们向LLM提供来自同一代码库的示例断言，这些断言是基于一种新的证明相似性度量选择的。我们在新的基准DafnyGym（一个从三个真实Dafny代码库中提取的复杂引理数据集）上评估了我们的技术。评估表明，Laurel仅需几次尝试即可生成超过56.6%的所需断言，这使得LLM成为一种经济实用的工具，可以在无需人工干预的情况下解除程序验证器的阻塞。

🔬 方法详解

问题定义：程序验证器依赖SMT求解器进行自动化证明，但SMT求解器常常需要人工编写的断言作为提示才能完成证明。人工编写断言耗时费力，成为程序验证自动化的瓶颈。现有方法难以有效自动生成这些断言，导致验证过程受阻。

核心思路：利用大型语言模型（LLM）的强大代码生成能力，自动生成程序验证所需的断言。通过特定领域的提示技术，引导LLM生成更准确、有效的断言，从而提高程序验证的自动化程度。

技术框架：Laurel工具包含以下主要阶段：1) 错误信息分析：分析程序验证器（如Dafny）的错误信息，确定缺失断言的位置。2) 断言占位符插入：在错误信息指示的位置插入断言占位符，作为LLM的输入。3) 示例断言选择：基于新的证明相似性度量，从同一代码库中选择与当前证明相关的示例断言。4) LLM提示：将包含断言占位符和示例断言的代码片段作为提示输入LLM。5) 断言生成：LLM根据提示生成断言，填充断言占位符。

关键创新：1) 领域特定提示技术：针对程序验证任务，设计了两种提示技术，包括基于错误信息定位和基于证明相似性选择示例断言。2) 证明相似性度量：提出了一种新的证明相似性度量，用于选择与当前证明相关的示例断言，提高LLM生成断言的准确性。

关键设计：1) 错误信息分析：解析Dafny的错误信息，提取关键信息（如变量名、类型、位置等），用于确定断言占位符的位置。2) 证明相似性度量：基于代码的抽象语法树（AST）结构和变量使用情况，计算证明之间的相似度。3) LLM选择：使用预训练的code-davinci-002模型，并进行微调以适应Dafny代码的风格。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

Laurel在DafnyGym基准测试中表现出色，仅需几次尝试即可生成超过56.6%的所需断言。与没有提示的LLM相比，Laurel的两种提示技术显著提高了断言生成的成功率。实验结果表明，Laurel能够有效减轻程序验证工程师的负担，提高程序验证的自动化程度。

🎯 应用场景

该研究成果可应用于各种需要形式化验证的软件开发场景，例如操作系统内核、编译器、智能合约等。通过自动生成断言，Laurel可以显著降低程序验证的成本，提高软件的可靠性和安全性，并加速软件开发流程。未来，该技术有望集成到IDE中，为开发者提供实时的断言生成建议。

📄 摘要（原文）

Program verifiers such as Dafny automate proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires hints in the form of assertions, creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that alleviates this burden by automatically generating assertions using large language models (LLMs). To improve the success rate of LLMs in this task, we design two domain-specific prompting techniques. First, we help the LLM determine the location of the missing assertion by analyzing the verifier's error message and inserting an assertion placeholder at that location. Second, we provide the LLM with example assertions from the same codebase, which we select based on a new proof similarity metric. We evaluate our techniques on our new benchmark DafnyGym, a dataset of complex lemmas we extracted from three real-world Dafny codebases. Our evaluation shows that Laurel is able to generate over 56.6\% of the required assertions given only a few attempts, making LLMs an affordable tool for unblocking program verifiers without human intervention.