用Dafny语言生成可验证的中间代码，提升LLM编程的准确性。
Dafny as Verification-Aware Intermediate Language for Code Generation
- 让LLM先生成带形式化验证的Dafny中间代码
- 在HumanEval上通过率提升至82.3%
- 适合需要高可靠代码的开发者或安全敏感场景
利用大语言模型（LLMs）从自然语言提示生成源代码是一项热门且前景广阔的技术，但生成的代码有时存在微妙错误，尽管看似正确。本文探索如何通过形式化方法提高LLM生成代码的质量。我们提出：用户引导LLM首先生成一种不透明的中间表示——验证感知语言Dafny中的代码，该代码可自动验证是否符合既定规范。正确无误的Dafny程序随后被编译为目标语言并返回给用户。整个过程中的用户-系统交互均通过自然语言完成，用户无需接触Dafny代码。我们介绍了当前原型，并报告其在HumanEval Python代码生成基准上的表现。
原文摘要 · Abstract (English)
Using large language models (LLMs) to generate source code from natural language prompts is a popular and promising idea with a wide range of applications. One of its limitations is that the generated code can be faulty at times, often in a subtle way, despite being presented to the user as correct. In this paper, we explore ways in which formal methods can assist with increasing the quality of code generated by an LLM. Instead of emitting code in a target language directly, we propose that the user guides the LLM to first generate an opaque intermediate representation, in the verification-aware language Dafny, that can be automatically validated for correctness against agreed on specifications. The correct Dafny program is then compiled to the target language and returned to the user. All user-system interactions throughout the procedure occur via natural language; Dafny code is never exposed. We describe our current prototype and report on its performance on the HumanEval Python code generation benchmarks.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。