Abstract
In the past few years LLMs have emerged as a tool that can aid programmers by taking natural language descriptions and generating code based on it. However, LLMs often generate incorrect code that users need to fix and the literature suggests users often struggle to detect these errors. In this work we seek to offer formal guarantees of correctness to LLM generated code; such guarantees could improve the experience of using AI Code Assistants and potentially enable natural language programming for users with little or no programming knowledge. To address this challenge we propose to incorporate a formal query language that can represent a user's intent in a formally defined but natural language-like manner that a user can confirm matches their intent. Then, using such a query we propose to verify LLM generated code to ensure it matches the user's intent. We implement these ideas in our system, Astrogator, for the Ansible programming language which includes such a formal query language, a calculus for representing the behavior of Ansible programs, and a symbolic interpreter which is used for the verification. On a benchmark suite of 21 code-generation tasks, our verifier is able to verify correct code in 83% of cases and identify incorrect code in 92%.
Abstract (translated)
在过去的几年里，大型语言模型（LLMs）作为一种工具出现，能够通过接受自然语言描述并根据这些描述生成代码来帮助程序员。然而，LLMs经常会生成错误的代码，用户需要对其进行修正，并且文献表明用户常常难以发现这些错误。在这项工作中，我们寻求为LLM生成的代码提供正式的正确性保证；这样的保证可以改善使用AI编码助手的体验，并有可能使具有很少或没有编程知识的用户实现自然语言编程。 为了应对这一挑战，我们提议纳入一种形式化的查询语言，该语言能够以类似于自然语言的方式表示用户的意图，同时在形式上被定义清楚，使得用户可以确认它与他们的意图相匹配。然后，通过使用这种查询，我们建议验证LLM生成的代码，确保其符合用户的意图。 我们在名为Astrogator的系统中实现了这些想法，该系统针对Ansible编程语言设计，并包含这样的形式化查询语言、表示Ansible程序行为的微积分以及用于验证的符号解释器。在一套包含了21个代码生成任务的基准测试套件上，我们的验证器能够在83%的情况下验证正确的代码，并在92%的情况下识别出错误的代码。
URL
https://arxiv.org/abs/2507.13290
