Dafny is a popular verification language, which automates proofs by outsourcing them to an SMT solver. This automation is not perfect, however, and the solver often requires guidance in the form of helper assertions creating a burden for the proof engineer. In this paper, we propose Laurel, a tool that uses large language models (LLMs) to automatically generate helper assertions for Dafny programs. 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 lemma similarity metric. We evaluate our techniques on a dataset of helper assertions we extracted from three real-world Dafny codebases. Our evaluation shows that Laurel is able to generate over 50% of the required helper assertions given only a few attempts, making LLMs a usable and affordable tool to further automate practical program verification.

翻译：Dafny是一种流行的验证语言，通过将证明任务委托给SMT求解器来自动化证明过程。然而，这种自动化并不完美，求解器通常需要以辅助断言的形式进行指导，这给验证工程师带来了负担。本文提出Laurel工具，该工具利用大型语言模型（LLMs）为Dafny程序自动生成辅助断言。为提升LLMs在此任务中的成功率，我们设计了两种领域特定的提示技术。首先，通过分析验证器的错误信息并在相应位置插入断言占位符，帮助LLM定位缺失断言的位置。其次，基于我们提出的新引理相似度度量方法，从同一代码库中筛选示例断言提供给LLM。我们在从三个真实世界Dafny代码库中提取的辅助断言数据集上评估了所提技术。实验表明，仅需少量尝试，Laurel即能生成超过50%的必要辅助断言，这使LLMs成为进一步自动化实际程序验证的可用且高效的工具。