mlsanityData to 14 Oct 2026

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

arXiv 2507.13290 ↗First posted 17 Jul 2025cs.PL cs.AIcited by 8

Not on the map. Why?

Abstract (arXiv)

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%.

Key facts. Cited by 8 papers in the map (data through 14 Oct 2026). Builds on 29 of its 63 references that are in the map. First posted on arXiv 17 Jul 2025.

Builds on

29 of 63 references.

References · 29

  1. 2024The Llama 3 Herd of Modelscited by 14,715
  2. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  3. 2023SWE-bench: Can Language Models Resolve Real-World GitHub Issues?cited by 3,373
  4. 2023Code Llama: Open Foundation Models for Codecited by 2,139
  5. 2023Is Your Code Generated by ChatGPT Really Correct? Rigorous Evaluation of Large Language Models for Code Generationcited by 1,391
  6. 2024DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligencecited by 1,181
  7. 2024BigCodeBench: Benchmarking Code Generation with Diverse Function Calls and Complex Instructionscited by 546
  8. 2024StarCoder 2 and The Stack v2: The Next Generationcited by 502
  9. 2022CodeT: Code Generation with Generated Testscited by 384
  10. 2022Grounded Copilot: How Programmers Interact with Code-Generating Modelscited by 218
  11. 2022Do Users Write More Insecure Code with AI Assistants?cited by 192
  12. 2024Granite Code Models: A Family of Open Foundation Models for Code Intelligencecited by 117
17 more
  1. 2023CodeBERTScore: Evaluating Code Generation with Pretrained Models of Codecited by 102
  2. 2024LLM Hallucinations in Practical Code Generation: Phenomena, Mechanism, and Mitigationcited by 93
  3. 2023Studying the effect of AI Code Generators on Supporting Novice Learners in Introductory Programmingcited by 89
  4. 2024SynCode: LLM Generation with Grammar Augmentationcited by 69
  5. 2024A Survey on LLM-based Code Generation for Low-Resource and Domain-Specific Programming Languagescited by 66
  6. 2024SelfCodeAlign: Self-Alignment for Code Generationcited by 62
  7. 2023Can Large Language Models Transform Natural Language Intent into Formal Method Postconditions?cited by 57
  8. 2024What's Wrong with Your Code Generated by Large Language Models? An Extensive Studycited by 53
  9. 2023"What It Wants Me To Say": Bridging the Abstraction Gap Between End-User Programmers and Code-Generating Large Language Modelscited by 48
  10. 2023On the Effectiveness of Large Language Models in Domain-Specific Code Generationcited by 44
  11. 2025Type-Constrained Code Generation with Language Modelscited by 35
  12. 2024Policy Filtration for RLHF to Mitigate Noise in Reward Modelscited by 22
  13. 2015A Survey and Classification of Controlled Natural Languagescited by 18
  14. 2024CodeMMLU: A Multi-Task Benchmark for Assessing Code Understanding & Reasoning Capabilities of CodeLLMscited by 18
  15. 2024RLSF: Fine-tuning LLMs via Symbolic Feedbackcited by 14
  16. 2024InverseCoder: Self-improving Instruction-Tuned Code LLMs with Inverse-Instructcited by 8
  17. 2024PhotoScout: Synthesis-Powered Multi-Modal Image Searchcited by 2

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2025: 2; 2026: 6.

8 papers.

  1. 2026PatchWorld: Gradient-Free Optimization of Executable World Models for Agent Environmentscited by 7
  2. 2025SLMFix: Leveraging Small Language Models for Domain Specific Language Error Fixing with Reinforcement Learningcited by 2
  3. 2026EvoUndo: Recoverability-Constrained Self-Evolution for LLM Agent Harnessescited by 2
  4. 2026Feedback-based Automated Verification in Vibe Coding of CAS Adaptation Built on Constraint Logiccited by 1
  5. 2025Uplifted Attackers, Human Defenders: The Cyber Offense-Defense Balance for Trailing-Edge Organizationscited by 0
  6. 2026LLMs + Security = Troublecited by 0
  7. 2026Vibe-Coding: Feedback-Based Automated Verification with no Human Code Inspection, a Feasibility Studycited by 0
  8. 2026Model-Driven Requirements Configuration with Three-Valued Uncertainty Scoringcited by 0