# Automated Repair of AI Code with Large Language Models and Formal Verification

arXiv: https://arxiv.org/abs/2405.08848 · HTML: https://mlsanity.com/paper/2405.08848/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 35 references that are in the map.
- First posted on arXiv 14 May 2024.

## Builds on (most cited first, 15 of 15)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Language Models are Few-Shot Learners](https://mlsanity.com/paper/2005.14165/) (2020)
- [A Prompt Pattern Catalog to Enhance Prompt Engineering with ChatGPT](https://mlsanity.com/paper/2302.11382/) (2023)
- [Exploring the Limits of Out-of-Distribution Detection](https://mlsanity.com/paper/2106.03004/) (2021)
- [How is ChatGPT's behavior changing over time?](https://mlsanity.com/paper/2307.09009/) (2023)
- [A Framework for Understanding Sources of Harm throughout the Machine Learning Life Cycle](https://mlsanity.com/paper/1901.10002/) (2019)
- [Taxonomy of Real Faults in Deep Learning Systems](https://mlsanity.com/paper/1910.11015/) (2019)
- [Automated Repair of Programs from Large Language Models](https://mlsanity.com/paper/2205.10583/) (2022)
- [TensorFuzz: Debugging Neural Networks with Coverage-Guided Fuzzing](https://mlsanity.com/paper/1807.10875/) (2018)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [Pitfalls in Machine Learning Research: Reexamining the Development Cycle](https://mlsanity.com/paper/2011.02832/) (2020)
- [Bugs in Machine Learning-based Systems: A Faultload Benchmark](https://mlsanity.com/paper/2206.12311/) (2022)
- [Learning Density Distribution of Reachable States for Autonomous Systems](https://mlsanity.com/paper/2109.06728/) (2021)
- [NeuroCodeBench: a plain C neural network benchmark for software verification](https://mlsanity.com/paper/2309.03617/) (2023)
- [Mull it over: mutation testing based on LLVM](https://mlsanity.com/paper/1908.01540/) (2019)

## Built on by (most cited first, 3 of 3)

- [Frontier AI's Impact on the Cybersecurity Landscape](https://mlsanity.com/paper/2504.05408/) (2025)
- [From Code Foundation Models to Agents and Applications: A Comprehensive Survey and Practical Guide to Code Intelligence](https://mlsanity.com/paper/2511.18538/) (2025)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)

## Abstract (arXiv)

The next generation of AI systems requires strong safety guarantees. This report looks at the software implementation of neural networks and related memory safety properties, including NULL pointer deference, out-of-bound access, double-free, and memory leaks. Our goal is to detect these vulnerabilities, and automatically repair them with the help of large language models. To this end, we first expand the size of NeuroCodeBench, an existing dataset of neural network code, to about 81k programs via an automated process of program mutation. Then, we verify the memory safety of the mutated neural network implementations with ESBMC, a state-of-the-art software verifier. Whenever ESBMC spots a vulnerability, we invoke a large language model to repair the source code. For the latest task, we compare the performance of various state-of-the-art prompt engineering techniques, and an iterative approach that repeatedly calls the large language model.