Dafny as Verification-Aware Intermediate Language for Code Generation
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910780632334336 |
|---|---|
| author | Li, Yue Chen Zetzsche, Stefan Somayyajula, Siva |
| author_facet | Li, Yue Chen Zetzsche, Stefan Somayyajula, Siva |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_06283 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Dafny as Verification-Aware Intermediate Language for Code Generation Li, Yue Chen Zetzsche, Stefan Somayyajula, Siva Software Engineering Artificial Intelligence Computation and Language Logic in Computer Science Programming Languages 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. |
| title | Dafny as Verification-Aware Intermediate Language for Code Generation |
| topic | Software Engineering Artificial Intelligence Computation and Language Logic in Computer Science Programming Languages |
| url | https://arxiv.org/abs/2501.06283 |