Dafny as Verification-Aware Intermediate Language for Code Generation
This addresses the issue of unreliable code generation for users relying on LLMs for programming tasks, representing an incremental improvement by integrating formal methods.
The paper tackles the problem of faulty code generated by large language models (LLMs) by proposing a method where LLMs first generate code in the verification-aware language Dafny, which is automatically validated for correctness before compilation to the target language, achieving performance on the HumanEval Python benchmarks.
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.