Leveraging Large Language Models to Boost Dafny's Developers Productivity

本研究提出了一种利用大型语言模型（LLMs）提高Dafny开发人员生产力的研究想法。虽然验证感知语言（如Dafny）的使用在过去十年中已经大大增加，但这些语言仍未被广泛采用。通常使用这些语言的成本太高，因为需要开发人员具备高水平的专业知识，并且在试图证明程序正确性时常常面临挑战。尽管Dafny自动化了许多验证过程，但有时还存在一些步骤对于Dafny来说过于复杂而无法完成。其中一个例子是缺少引理，即Dafny无法在没有定理的帮助下证明结果。 在本文中，我们描述了一种新的Dafny插件的初步工作，利用LLMs为开发人员生成建议，以帮助Dafny发现和使用相关引理。此外，对于无法自动证明的引理，插件还尝试提供相应的计算证明。我们还讨论了未来工作的想法，通过描述一个使用LLMs来增加验证感知语言的采用的研究议程，通过提高开发人员的生产力和减少制定正式规范和证明程序属性所需的专业知识水平。

使用大型语言模型来提高Dafny开发人员的生产力和验证能力

使用LLMs生成建议引理并提供计算证明，以帮助Dafny开发人员解决无法自动证明的问题

论文提出了一种新的Dafny插件，使用LLMs来生成建议引理和计算证明，以帮助开发人员提高验证能力和生产力。未来的研究方向包括使用LLMs来提高验证感知语言的采用率，并减少制定正式规范和证明程序属性所需的专业知识水平。

近年来，还有其他研究使用机器学习来辅助程序验证，如DeepSpacer和Neurify。