TLDR: This research introduces Astrogator, a system designed to formally verify code generated by Large Language Models (LLMs) from natural language prompts. It proposes using a user-friendly formal query language to capture user intent, which then serves as a precise specification for verifying the LLM-generated code. Implemented for Ansible, Astrogator leverages a State Calculus and symbolic interpreter to compare program behavior against the formal query. Evaluation shows Astrogator effectively identifies correct and incorrect code, offering a path towards more reliable AI code assistants and natural language programming by providing formal correctness guarantees.
Large Language Models (LLMs) have become incredibly powerful tools, capable of generating code from natural language descriptions. Imagine telling a computer what you want it to do in plain English, and it writes the program for you. This dream, often called natural language programming, has been a long-standing goal in the programming world. However, there’s a significant challenge: LLMs frequently produce code that isn’t quite right, and users, especially those without deep programming knowledge, often struggle to spot these errors.
A new research paper, “Towards Formal Verification of LLM-Generated Code from Natural Language Prompts,” addresses this critical issue. Authored by Aaron Councilman, David Fu, Aryan Gupta, Chengxiao Wang, Yu-Xiong Wang, and Vikram Adve from the University of Illinois at Urbana-Champaign, along with David Grove from IBM Research, the paper proposes a novel approach to provide formal guarantees that LLM-generated code is correct. This could dramatically improve the reliability of AI Code Assistants and truly open up programming to a wider audience.
The core idea is to introduce a ‘formal query language.’ Think of this as a bridge between a user’s natural language request and a precise, machine-understandable specification. This language is designed to be natural language-like, so users can easily understand and confirm that it accurately reflects their intentions. Once this formal query is established, the system can then verify the LLM-generated code against it, ensuring the code actually does what the user intended.
The researchers implemented these concepts in a system they call Astrogator, specifically for the Ansible programming language. Ansible is widely used for automating IT tasks like managing servers and deploying applications. Astrogator includes its own formal query language, a way to represent Ansible program behavior (called the State Calculus), and a symbolic interpreter for verification.
How Astrogator Works
Astrogator operates with two main components: the Formal Query Language and the Program Verifier. The Formal Query Language is designed to be high-level and user-friendly, avoiding technical jargon like specific package names. Instead, it uses descriptive terms such as “install numpy” or “create bashrc file for user ‘foo’.” This is supported by a ‘knowledge base’ that translates these high-level concepts into the precise details needed for code generation, like the correct package name for ‘numpy’ on different operating systems.
The Program Verifier is where the magic of correctness checking happens. It takes the generated Ansible code and the formal query, both translated into the State Calculus, and compares their behaviors. The State Calculus models how programs change a system’s state (e.g., creating a file, installing software). A ‘symbolic interpreter’ analyzes the program’s behavior under various conditions, and a ‘unifier’ then checks if the program’s actions align with the formal query’s intent. Importantly, the verifier can also identify when a generated program makes additional assumptions or performs actions not explicitly stated in the query, which can then be flagged for user review.
Evaluation and Results
To test Astrogator, the team created a benchmark suite of 21 common Ansible tasks, each with a natural language description, a formal query, and a reference solution. They then used six different LLMs (Deepseek Coder, GPT-4.o, Granite Code, Llama 3.1, Qwen2.5 Coder, and Starcoder 2) to generate 10 programs for each task, totaling 1,260 programs. These generated programs were run on virtual machines running different Linux distributions (Debian, Ubuntu, RHEL) to determine their actual correctness.
The results showed that only about 26.5% of the LLM-generated programs were actually correct. GPT-4.o performed significantly better than the open-source models, generating 51.4% correct code compared to about 21.5% from the others. When Astrogator was put to the test, it successfully identified 82.9% of the truly correct programs as correct. Even more impressively, it rejected 92.4% of the incorrect programs.
The paper acknowledges that Astrogator isn’t perfect. Some correct programs were rejected due to unsupported features or limitations in the knowledge base, such as expecting a specific file path when multiple valid ones exist. Conversely, some incorrect programs were accepted because they would be correct under certain additional assumptions (e.g., a user already existing) that were not met in the testing environment. The researchers emphasize that these assumptions are highlighted by the verifier, requiring user intervention to confirm if they align with their intent.
Also Read:
- ARPaCCino: An AI-Powered Approach to Policy as Code Compliance
- CodeAssistBench: A New Standard for Evaluating Programming AI
Looking Ahead
This research marks a significant step towards reliable natural language programming. While Astrogator is currently focused on Ansible, the underlying principles, especially the State Calculus and the verification approach, are designed to be adaptable to other domain-specific languages. The authors believe that DSLs are particularly well-suited for this approach due to their defined concepts and often non-Turing complete nature, which simplifies verification. This work lays a strong foundation for future systems that can generate code with formal guarantees, moving us closer to a world where anyone can program a computer using natural language. You can read the full paper here.
