利用大型语言模型提升 Dafny 开发者的生产力
软件工程
2024-01-03 v1 计算机科学中的逻辑
编程语言
摘要
本研究构想论文提出利用大型语言模型（LLM）来提升 Dafny 开发者的生产力。尽管过去十年中 Dafny 等支持验证的语言使用量显著增加，但其尚未被广泛采用。使用此类语言的成本往往过高，原因在于对开发者专业水平要求较高，且他们在尝试证明程序正确性时常面临挑战。即使 Dafny 自动化了大部分验证过程，有时仍存在某些步骤过于复杂，导致 Dafny 无法独立完成。其中一种情况是缺失引理，即若无额外帮助（如辅助证明该步骤的定理），Dafny 便无法证明某一结果。本文介绍了一项关于新型 Dafny 插件的初步工作，该插件利用 LLM 通过生成相关引理建议来协助开发者，这些引理是 Dafny 自身无法发现和使用的。此外，对于无法自动证明的引理，该插件还尝试提供相应的计算性证明。我们还通过描述一项研究议程来探讨未来工作方向，旨在利用 LLM 提高开发者生产力并降低构建形式化规范及证明程序属性所需的专业门槛，从而总体上提升支持验证语言的采用率。
引用
@article{arxiv.2401.00963,
title = {Leveraging Large Language Models to Boost Dafny's Developers Productivity},
author = {Álvaro Silva and Alexandra Mendes and João F. Ferreira},
journal= {arXiv preprint arXiv:2401.00963},
year = {2024}
}