一句话：Laurel 利用大语言模型自动生成 Dafny 断言，通过错误定位与代码库示例提示，减少验证器所需人工提示。
Dafny 等程序验证器将证明交给 SMT 求解器自动化，但求解器常需要断言作为提示，给证明工程师带来负担。本文提出 Laurel，用大语言模型自动生成缺失断言。为提升成功率，作者设计两种领域特定提示技术：分析验证器错误信息以确定缺失断言位置并插入占位符；基于新的证明相似度度量，从同一代码库中选取示例断言提供给模型。作者同时构建 DafnyGym 基准，从三个真实 Dafny 代码库抽取复杂引理。评估表明，在仅少量尝试下，Laurel 能生成超过 56.6% 的所需断言，使 LLM 成为无需人工干预即可解除验证器阻塞的实用工具。
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.
@article{paperbot3189,
title = {Laurel: Unblocking Automated Verification with Large Language Models},
author = {Eric Mugnier and Emmanuel Anaya Gonzalez and Nadia Polikarpova and Ranjit Jhala and Zhou Yuanyuan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720499}
}