Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts

Aaron Councilman, David Jiahao Fu, Aryan Gupta, Chengxiao Wang, David Grove, Yu-Xiong Wang, Vikram Adve

TL;DR

This work tackles the challenge of providing formal correctness guarantees for code produced by LLMs from natural-language prompts, focusing on domain-specific automation language Ansible. It introduces a Formal Query Language (FQL) that is human-readable yet formally defined, a Knowledge Base to map high-level intents to concrete OS- and module-specific actions, and Astrogator to verify LLM-generated playbooks against a formal specification via a State Calculus-based verifier. The key contributions include: (1) a concrete design and implementation of FQL and a verifier for Ansible, (2) a State Calculus and symbolic interpreter that model Ansible state changes and enable rigorous behavioral verification, and (3) an empirical evaluation on 21 tasks showing substantial accuracy (83% verification of correct code) and strong error-detection (92% of incorrect code identified). The results demonstrate the feasibility of integrating NL-like formal specifications with programmable verification to support trusted AI code assistants in critical IT contexts, with clear pathways to generalize to other DSLs like Bash and Arduino and to automate knowledge-base construction.

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, the reliability of LLM code generation and current validation techniques for it are far from strong enough to be used for mission-critical or safety-critical applications. In this work we explore ways to offer formal guarantees of correctness to LLM generated code; such guarantees could improve the quality of general AI Code Assistants and support their use for critical applications. 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. We then have a formal specification of the user intent which we can use to verify that LLM-generated code matches the user's intent. We implement these ideas in our system, Astrogator, for the Ansible programming language, widely used for system administration, including for critical systems. The system includes an intuitive formal query language, a calculus for representing the behavior of Ansible programs, and a symbolic interpreter and a unification algorithm which together are used for the verification. A key innovation in Astrogator is the use of a Knowledge Base to capture system-specific implementation dependencies that greatly reduce the need for system knowledge in expressing formal queries. 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%.

Towards Formal Verification of LLM-Generated Code from Natural Language Prompts

TL;DR

This work tackles the challenge of providing formal correctness guarantees for code produced by LLMs from natural-language prompts, focusing on domain-specific automation language Ansible. It introduces a Formal Query Language (FQL) that is human-readable yet formally defined, a Knowledge Base to map high-level intents to concrete OS- and module-specific actions, and Astrogator to verify LLM-generated playbooks against a formal specification via a State Calculus-based verifier. The key contributions include: (1) a concrete design and implementation of FQL and a verifier for Ansible, (2) a State Calculus and symbolic interpreter that model Ansible state changes and enable rigorous behavioral verification, and (3) an empirical evaluation on 21 tasks showing substantial accuracy (83% verification of correct code) and strong error-detection (92% of incorrect code identified). The results demonstrate the feasibility of integrating NL-like formal specifications with programmable verification to support trusted AI code assistants in critical IT contexts, with clear pathways to generalize to other DSLs like Bash and Arduino and to automate knowledge-base construction.

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, the reliability of LLM code generation and current validation techniques for it are far from strong enough to be used for mission-critical or safety-critical applications. In this work we explore ways to offer formal guarantees of correctness to LLM generated code; such guarantees could improve the quality of general AI Code Assistants and support their use for critical applications. 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. We then have a formal specification of the user intent which we can use to verify that LLM-generated code matches the user's intent. We implement these ideas in our system, Astrogator, for the Ansible programming language, widely used for system administration, including for critical systems. The system includes an intuitive formal query language, a calculus for representing the behavior of Ansible programs, and a symbolic interpreter and a unification algorithm which together are used for the verification. A key innovation in Astrogator is the use of a Knowledge Base to capture system-specific implementation dependencies that greatly reduce the need for system knowledge in expressing formal queries. 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%.

Paper Structure

This paper contains 42 sections, 1 equation, 7 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Ansible
  4. Errors in LLM-Generated Ansible
  5. Problem Statement
  6. Approach
  7. Design Considerations for a Formal Query Language
  8. Program Verifier
  9. Formal Query Language and Verification of LLM-Generated Code for Ansible
  10. Ansible Formal Query Language Design
  11. State Calculus and Interpreter
  12. State Calculus
  13. States
  14. Syntax
  15. Symbolic Interpreter
  16. ...and 27 more sections

Figures (7)

  • Figure 1: An example Ansible playbook composed of a single play which configures a set servers by installing and starting Apache server.
  • Figure 2: Overview diagram of our code generation system. The dashed lines between the user and Query Check and Assumptions Check indicate the user needing to review and approve or disapprove.
  • Figure 3: Grammar of the Ansible Formal Query Language.
  • Figure 4: Description of the State Calculus
  • Figure 5: A simplified module description for ansible.builtin.copy
  • ...and 2 more figures