Towards Formal Verification of LLM-Generated Code from Natural Language Prompts
This addresses the issue for users of AI code assistants, particularly those with little programming knowledge, by providing formal guarantees, though it is incremental as it builds on existing formal methods for a specific language.
The paper tackles the problem of LLMs generating incorrect code from natural language prompts by proposing a formal verification method to guarantee correctness, achieving verification of correct code in 83% of cases and identification of incorrect code in 92% on a benchmark.
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%.