dafny-annotator: AI-Assisted Verification of Dafny Programs

📄 arXiv: 2411.15143v1 📥 PDF

作者: Gabriel Poesia, Chloe Loughridge, Nada Amin

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

发布日期: 2024-11-05

💡 一句话要点

提出dafny-annotator，利用AI辅助Dafny程序的形式化验证，提升验证效率。

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

关键词: 形式化验证 Dafny 大型语言模型 AI辅助编程 程序合成

📋 核心要点

  1. 形式化验证成本高昂，阻碍大规模应用，Dafny需要人工逻辑注解辅助验证，存在效率瓶颈。
  2. 利用大型语言模型和搜索算法，自动为Dafny程序添加逻辑注解，直至验证通过，降低人工干预。
  3. 通过合成数据DafnySynth扩充训练集，显著提升LLaMa 8B的注解成功率，达到50.6%。

📝 摘要（中文）

形式化验证有潜力大幅减少软件错误，但其高昂的成本阻碍了大规模应用。Dafny有望显著降低编写已验证程序的难度，但用户通常需要提供逻辑注解来辅助验证器。本文探索使用大型语言模型和搜索相结合的方法，构建dafny-annotator：一个向Dafny方法添加逻辑注解的工具，直到验证器能够证明其正确性。在DafnyBench程序集合的测试集上，由LLaMa 3.1 8B引导的贪婪搜索仅成功注释了15.7%的方法。由于这种数据驱动的方法受到缺乏大规模训练数据的限制，我们提出了一种开放式合成新Dafny程序的方法，该方法在一个灵活的pipeline中，由LLM制定高层想法，实现它们，并逐步提出对现有程序的更改，Dafny验证这些更改。这为我们提供了一个合成数据集DafnySynth，我们使用它来扩充DafnyBench进行训练。在两个数据集上进行微调，使LLaMa 8B的成功率提高到50.6%，明显优于基础模型或仅在任一数据集上进行训练。我们的结果表明，对于尚无大规模人工生成示例的语言，可以使用功能强大的AI助手。反过来，这样的助手可能会减少用户的摩擦，并最终推动采用。

🔬 方法详解

问题定义：论文旨在解决Dafny程序形式化验证过程中，人工添加逻辑注解耗时耗力的问题。现有方法依赖人工经验，效率低下，且容易出错。缺乏大规模的Dafny程序训练数据，限制了数据驱动方法的效果。

核心思路：论文的核心思路是利用大型语言模型（LLM）的强大代码生成能力，结合搜索算法，自动生成Dafny程序的逻辑注解。通过合成Dafny程序数据，扩充训练集，提升LLM的注解能力。

技术框架：整体框架包含以下几个主要模块：1) LLM驱动的注解生成器：使用LLM生成候选的逻辑注解。2) Dafny验证器：验证生成的注解是否能够使程序通过形式化验证。3) 搜索算法：根据验证结果，迭代优化注解，直至程序验证通过。4) 数据合成模块：利用LLM生成新的Dafny程序，用于扩充训练集。

关键创新：论文的关键创新在于：1) 提出了一种基于LLM和搜索算法的自动注解方法，降低了人工干预。2) 提出了一种开放式合成Dafny程序数据的方法，解决了缺乏大规模训练数据的问题。3) 将数据合成与模型训练相结合，形成一个闭环的优化流程。

关键设计：论文的关键设计包括：1) 使用LLaMa 3.1 8B作为LLM，进行微调。2) 使用贪婪搜索算法，迭代优化注解。3) 设计DafnySynth数据合成流程，包括高层想法制定、代码实现和增量修改等步骤。4) 结合DafnyBench和DafnySynth数据集进行训练。

📊 实验亮点

实验结果表明，在DafnyBench数据集上，由LLaMa 3.1 8B引导的贪婪搜索仅成功注释了15.7%的方法。通过使用DafnySynth合成数据进行微调，LLaMa 8B的成功率提高到50.6%，显著优于基础模型或仅在任一数据集上进行训练。这表明合成数据可以有效提升AI辅助验证的性能。

🎯 应用场景

该研究成果可应用于软件形式化验证领域，降低验证成本，提高验证效率。通过AI辅助，可以减少人工编写逻辑注解的工作量，加速形式化验证技术的普及和应用，提升软件的可靠性和安全性。未来可扩展到其他形式化验证语言和工具。

📄 摘要（原文）

Formal verification has the potential to drastically reduce software bugs, but its high additional cost has hindered large-scale adoption. While Dafny presents a promise to significantly reduce the effort to write verified programs, users are often required to provide logical annotations to aid the verifier. Here, we explore using a combination of Large Language Models and search to build dafny-annotator: a tool that adds logical annotations to a Dafny method until the verifier can prove it correct. On a test set from the DafnyBench collection of programs, greedy search guided by LLaMa 3.1 8B successfully annotates only 15.7% of the methods. Since this data-driven approach is hindered by the lack of large-scale training data, we propose a method for open-ended synthesis of new Dafny programs in a flexible pipeline where LLMs formulate high-level ideas, implement them, and incrementally propose changes to existing programs, which Dafny validates. This gives us a synthetic dataset, DafnySynth, which we use to augment DafnyBench for training. Fine-tuning on both datasets boosts LLaMa 8B's success rate to 50.6% -- significantly better than the base model, or training on either dataset alone. Our results suggest a path towards capable AI assistants for languages that don't yet have large-scale human-generated examples. In turn, such assistants might reduce friction for users and ultimately drive adoption.