arXiv cs.AI· \'Alvaro Silva, Alexandra Mendes, Ruben Martins·· 1 天前AI 评分23
DAISY：面向 Dafny 的故障引导断言推断工具
DAISY: Fault-Guided Assertion Inference for Dafny
AI 导读
DAISY 是一款面向 Dafny 的故障引导断言推断工具，利用验证器诊断或 LLM 定位可能的断言位置，再由 LLM 生成候选断言并用 Dafny 验证器筛选。团队扩展 DafnyBench 构建了缺失断言变体基准，DAISY 在缺失单个断言的程序上验证通过率达 86%，缺失两个断言时为 36%。结果表明该方法能修复大量 Dafny 验证失败，且成功修复的断言常与原断言不同。
正文 · AI 翻译
摘要：使用 Dafny 进行形式化验证可提供强有力的正确性保证，但验证失败时，用户往往需要确定在哪里需要辅助断言，并手动编写验证成功所需的断言。这种证明工程负担困难、耗时，并且是采用验证感知语言的障碍。
我们提出 DAISY（Dafny Assertion Inference SYstem），一种用于 Dafny 中故障引导断言推断的工具。
给定一个 Dafny 程序和目标方法，DAISY 使用验证器诊断、基于 LLM 的定位或二者结合来定位可能的断言位置。然后，它用断言占位符标注程序，检索相关的上下文示例，使用 LLM 生成候选断言，并通过运行 Dafny 验证器来验证候选断言。
为了评估 DAISY，我们扩展了 DafnyBench，通过从已验证程序中移除辅助断言来创建验证失败的变体。由此产生的基准区分了缺少一个断言、缺少两个断言和移除所有断言的程序，使我们能够在日益困难的证明失败上评估 DAISY。在该基准上，DAISY 验证了 86\% 的缺少单个断言的程序和 36\% 的缺少两个断言的程序。这些结果表明，故障引导的 LLM 断言推断可以修复许多 Dafny 验证失败。它们还表明，成功的修复往往与原始断言不同，从而减少了证明工程工作量，而无需重建原始证明。
| 主题： | 软件工程（cs.SE）；人工智能（cs.AI）；计算机科学中的逻辑（cs.LO）；编程语言（cs.PL） |
| 引用为： | arXiv:2511.00125 [cs.SE] |
| （或此版本的 arXiv:2511.00125v2 [cs.SE]） | |
| https://doi.org/10.48550/arXiv.2511.00125 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Alvaro Festas Silva [查看电子邮件]
[v1]
2025 年 10 月 31 日星期五 09:45:39 UTC（168 KB）
[v2]
2026 年 11 月 11 日星期三 13:30:45 UTC（107 KB）
来源：arXiv cs.AI · arxiv.org