Inferring multiple helper Dafny assertions with LLMs

📄 arXiv: 2511.00125v1 📥 PDF

作者: Álvaro Silva, Alexandra Mendes, Ruben Martins

分类: cs.SE, cs.AI, cs.LO, cs.PL

发布日期: 2025-10-31

💡 一句话要点

提出DAISY，利用LLM自动推断Dafny程序中缺失的多个辅助断言，提升形式化验证效率。

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

关键词: 形式化验证 Dafny 大型语言模型 自动断言推断 程序验证

📋 核心要点

  1. Dafny形式化验证依赖大量手动断言，耗时且阻碍应用，亟需自动化辅助断言生成。
  2. DAISY系统结合LLM预测与错误信息启发式，实现对Dafny程序中缺失断言的自动推断。
  3. 实验表明DAISY能有效推断单个及多个缺失断言，显著减少人工干预，提升验证效率。

📝 摘要（中文）

Dafny验证器提供强大的正确性保证，但通常需要大量手动辅助断言，这成为其应用的主要障碍。本文研究了使用大型语言模型（LLM）自动推断Dafny程序中缺失的辅助断言，主要关注涉及多个缺失断言的情况。为了支持这项研究，我们扩展了DafnyBench基准，创建了删除一个、两个或所有断言的精选数据集，并引入了断言类型分类法来分析推断难度。我们的方法通过结合LLM预测和错误消息启发式的混合方法来改进故障定位。我们在名为DAISY（Dafny Assertion Inference SYstem）的新工具中实现了这种方法。虽然我们的重点是多个缺失断言，但我们也评估了DAISY在单个断言情况下的表现。DAISY验证了63.4%的具有一个缺失断言的程序和31.7%的具有多个缺失断言的程序。值得注意的是，许多程序可以用比最初存在的更少的断言来验证，这突出了证明通常允许多种有效的修复策略，并且不需要恢复每个原始断言。这些结果表明，自动断言推断可以大大减少证明工程工作，并代表着朝着更具可扩展性和可访问性的形式化验证迈出的一步。

🔬 方法详解

问题定义：Dafny程序的形式化验证依赖于大量的辅助断言，这些断言需要人工编写，耗时且容易出错。现有方法缺乏自动推断缺失断言的能力，尤其是在多个断言缺失的情况下，验证过程变得更加困难。因此，如何自动推断Dafny程序中缺失的辅助断言，特别是当存在多个缺失断言时，是一个亟待解决的问题。

核心思路：本文的核心思路是利用大型语言模型（LLM）的强大代码理解和生成能力，结合Dafny验证器的错误信息，来自动推断缺失的断言。通过分析错误信息，可以定位可能存在问题的代码区域，然后利用LLM生成候选断言，并使用Dafny验证器进行验证。如果候选断言能够使程序通过验证，则认为该断言是有效的。这种方法结合了LLM的生成能力和验证器的验证能力，能够有效地推断缺失的断言。

技术框架：DAISY系统的整体架构包含以下几个主要模块：1) 错误定位模块：该模块分析Dafny验证器产生的错误信息，定位可能存在问题的代码区域。2) LLM预测模块：该模块利用LLM生成候选断言，LLM的输入包括代码上下文和错误信息。3) 验证模块：该模块使用Dafny验证器验证候选断言的有效性。4) 断言选择模块：该模块选择能够使程序通过验证的断言。整个流程是一个迭代的过程，直到程序通过验证或者达到最大迭代次数。

关键创新：本文最重要的技术创新点在于提出了一种混合方法，将LLM的预测能力与Dafny验证器的验证能力相结合。与传统的基于规则或模板的方法相比，LLM能够更好地理解代码的语义，生成更准确的候选断言。此外，通过分析错误信息，可以更精确地定位问题区域，减少LLM的搜索空间。这种混合方法能够有效地推断缺失的断言，尤其是在多个断言缺失的情况下。

关键设计：DAISY的关键设计包括：1) LLM的选择：选择了具有强大代码理解和生成能力的LLM，例如Codex。2) 错误信息分析：设计了有效的错误信息分析方法，提取关键信息，例如错误类型、代码位置等。3) 候选断言生成：设计了合适的prompt，引导LLM生成高质量的候选断言。4) 验证策略：采用了高效的验证策略，快速验证候选断言的有效性。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

DAISY在DafnyBench扩展数据集上进行了评估，结果表明，对于单个缺失断言的情况，DAISY能够验证63.4%的程序；对于多个缺失断言的情况，DAISY能够验证31.7%的程序。此外，实验还发现，许多程序可以用比原始程序更少的断言来验证，表明自动断言推断能够找到更简洁的证明策略。

🎯 应用场景

该研究成果可应用于形式化验证领域，降低Dafny等验证工具的使用门槛，加速软件开发的验证过程。通过自动推断缺失断言，减少人工编写断言的工作量，提高验证效率，从而提升软件的可靠性和安全性。未来，该技术有望推广到其他形式化验证工具和编程语言中，实现更广泛的应用。

📄 摘要（原文）

The Dafny verifier provides strong correctness guarantees but often requires numerous manual helper assertions, creating a significant barrier to adoption. We investigate the use of Large Language Models (LLMs) to automatically infer missing helper assertions in Dafny programs, with a primary focus on cases involving multiple missing assertions. To support this study, we extend the DafnyBench benchmark with curated datasets where one, two, or all assertions are removed, and we introduce a taxonomy of assertion types to analyze inference difficulty. Our approach refines fault localization through a hybrid method that combines LLM predictions with error-message heuristics. We implement this approach in a new tool called DAISY (Dafny Assertion Inference SYstem). While our focus is on multiple missing assertions, we also evaluate DAISY on single-assertion cases. DAISY verifies 63.4% of programs with one missing assertion and 31.7% with multiple missing assertions. Notably, many programs can be verified with fewer assertions than originally present, highlighting that proofs often admit multiple valid repair strategies and that recovering every original assertion is unnecessary. These results demonstrate that automated assertion inference can substantially reduce proof engineering effort and represent a step toward more scalable and accessible formal verification.