Dafny as Verification-Aware Intermediate Language for Code Generation

• URL: http://arxiv.org/abs/2501.06283v1
• Date: Fri, 10 Jan 2025 17:23:14 GMT
• Title: Dafny as Verification-Aware Intermediate Language for Code Generation
• Authors: Yue Chen Li, Stefan Zetzsche, Siva Somayyajula,
• Abstract summary: Large language models (LLMs) generate source code from natural language prompts. One of its limitations is that the generated code can be faulty at times, despite being presented to the user as correct. We propose that the user guides the LLM to first generate an opaque intermediate representation, in the verification-aware language Dafny. The correct Dafny program is then compiled to the target language and returned to the user.
• Score: 0.0
• License:
• Abstract: 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.

Related papers

• Effective LLM-Driven Code Generation with Pythoness [0.0]
  Pythoness is an embedded domain-specific language for code generation using large language models (LLMs) In Pythoness, developers operate at the level of behavioral specifications when writing functions, classes, or an entire program. We show that Pythoness can successfully leverage a combination of tests and code generation to yield higher quality code than specifications alone.
  arXiv  Detail & Related papers  (2025-01-03T23:14:46Z)
• Synthetic Programming Elicitation for Text-to-Code in Very Low-Resource Programming and Formal Languages [21.18996339478024]
  We introduce emphsynthetic programming elicitation and compilation (SPEAC) SPEAC produces syntactically correct programs more frequently and without sacrificing semantic correctness. We empirically evaluate the performance of SPEAC in a case study for the UCLID5 formal verification language.
  arXiv  Detail & Related papers  (2024-06-05T22:16:19Z)
• Decoding at the Speed of Thought: Harnessing Parallel Decoding of Lexical Units for LLMs [57.27982780697922]
  Large language models have demonstrated exceptional capability in natural language understanding and generation. However, their generation speed is limited by the inherently sequential nature of their decoding process. This paper introduces Lexical Unit Decoding, a novel decoding methodology implemented in a data-driven manner.
  arXiv  Detail & Related papers  (2024-05-24T04:35:13Z)
• CodeGRAG: Bridging the Gap between Natural Language and Programming Language via Graphical Retrieval Augmented Generation [58.84212778960507]
  We propose CodeGRAG, a Graphical Retrieval Augmented Code Generation framework to enhance the performance of LLMs. CodeGRAG builds the graphical view of code blocks based on the control flow and data flow of them to fill the gap between programming languages and natural language. Various experiments and ablations are done on four datasets including both the C++ and python languages to validate the hard meta-graph prompt, the soft prompting technique, and the effectiveness of the objectives for pretrained GNN expert.
  arXiv  Detail & Related papers  (2024-05-03T02:48:55Z)
• Bridging Code Semantic and LLMs: Semantic Chain-of-Thought Prompting for Code Generation [22.219645213202178]
  This paper proposes the "Semantic Chain-of-Thought" approach to intruduce semantic information of code, named SeCoT. We show that SeCoT can achieves state-of-the-art performance, greatly improving the potential for large models and code generation.
  arXiv  Detail & Related papers  (2023-10-16T05:09:58Z)
• CodeFuse-13B: A Pretrained Multi-lingual Code Large Language Model [58.127534002232096]
  This paper introduces CodeFuse-13B, an open-sourced pre-trained code LLM. It is specifically designed for code-related tasks with both English and Chinese prompts. CodeFuse achieves its effectiveness by utilizing a high quality pre-training dataset.
  arXiv  Detail & Related papers  (2023-10-10T02:38:44Z)
• Interactive Code Generation via Test-Driven User-Intent Formalization [60.90035204567797]
  Large language models (LLMs) produce code from informal natural language (NL) intent. It is hard to define a notion of correctness since natural language can be ambiguous and lacks a formal semantics. We describe a language-agnostic abstract algorithm and a concrete implementation TiCoder.
  arXiv  Detail & Related papers  (2022-08-11T17:41:08Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  We propose a retrieval-augmented code completion framework, leveraging both lexical copying and referring to code with similar semantics by retrieval. We evaluate our approach in the code completion task in Python and Java programming languages, achieving a state-of-the-art performance on CodeXGLUE benchmark.
  arXiv  Detail & Related papers  (2022-03-15T08:25:08Z)
• Incorporating External Knowledge through Pre-training for Natural Language to Code Generation [97.97049697457425]
  Open-domain code generation aims to generate code in a general-purpose programming language from natural language (NL) intents. We explore the effectiveness of incorporating two varieties of external knowledge into NL-to-code generation: automatically mined NL-code pairs from the online programming QA forum StackOverflow and programming language API documentation. Our evaluations show that combining the two sources with data augmentation and retrieval-based data re-sampling improves the current state-of-the-art by up to 2.2% absolute BLEU score on the code generation testbed CoNaLa.
  arXiv  Detail & Related papers  (2020-04-20T01:45:27Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.