Towards AI-Assisted Synthesis of Verified Dafny Methods

大型随机语言模型在许多领域中都展现出了巨大的潜力，包括编程。承诺容易做出，但难以兑现，语言模型在应用于编程时经常无法兑现承诺，生成错误的代码。让模型生成支持形式验证的编程语言中的代码是保持模型诚实的一种有前途的途径：如果采用了这种方法，模型将提供代码证明，并且该证明将被自动验证。不幸的是，现有的大型语言模型在经过验证的编程语言方面的熟练程度严重不足。在本文中，我们演示了如何提高两个预训练模型在Dafny经过验证的编程语言方面的熟练程度。我们使用MBPP数据集中的178个编程问题，提示两个现代模型（GPT-4和PaLM-2）在Dafny中生成方法。我们使用了三种不同类型的提示：直接的无上下文提示，第二个提示包括方法签名和测试用例，第三个提示将问题分解成步骤，并包括动态选择的相似示例。我们的结果表明，GPT-4比PaLM-2更好，但在两个模型中，第三个提示极大地提高了直接提示的生成任务的成功率。使用第三个提示，GPT-4能够在58％的情况下生成经过验证的（并由人评估的）Dafny方法，而第一个提示仅在19％的情况下生成经过验证的（并由人评估的）方法。令人惊讶的是，第二个提示的表现最差，仅有10％。我们工作的一个实际贡献是收集了153个在Dafny中实现和正式验证的MBPP问题，其中50个是我们编写的，103个是由GPT-4自动合成的。此外，我们的结果表明，正式程序验证（正确性证明）的好处现在已经可以实现了...

提高大规模语言模型在验证编程语言中的能力

使用第三类提示，将大规模语言模型的Dafny验证编程语言生成任务的成功率提高到58%

使用178个编程问题的数据集，展示了GPT-4和PaLM-2模型在Dafny验证编程语言中的能力。通过使用不同类型的提示，发现第三类提示可以极大提高模型的成功率。作者还提供了一些在Dafny中实现和正式验证的编程问题。

最近的相关研究包括：1.《Formally Verified Semantic Equivalence of LLVM IR Optimizations》2.《DeepTest: Automated Testing of Deep-Neural-Network-driven Autonomous Cars》3.《A Systematic Survey of Program Synthesis》