# Do AI models help produce verified bug fixes?

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 11 of its 32 references that are in the map.
- First posted on arXiv 21 Jul 2025.

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

- [Grounded Copilot: How Programmers Interact with Code-Generating Models](https://mlsanity.com/paper/2206.15000/) (2022)
- [Keep the Conversation Going: Fixing 162 out of 337 bugs for 0.42 each using ChatGPT](https://mlsanity.com/paper/2304.00385/) (2023)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- ["It's Weird That it Knows What I Want": Usability and Interactions with Copilot for Novice Programmers](https://mlsanity.com/paper/2304.02491/) (2023)
- [How Novices Use LLM-Based Code Generators to Solve CS1 Coding Tasks in a Self-Paced Learning Environment](https://mlsanity.com/paper/2309.14049/) (2023)
- [Copiloting the Copilots: Fusing Large Language Models with Completion Engines for Automated Program Repair](https://mlsanity.com/paper/2309.00608/) (2023)
- [A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification](https://mlsanity.com/paper/2305.14752/) (2023)
- [VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Search](https://mlsanity.com/paper/2402.08147/) (2024)
- [How Novice Programmers Use and Experience ChatGPT when Solving Programming Exercises in an Introductory Course](https://mlsanity.com/paper/2407.20792/) (2024)
- [Next Steps in LLM-Supported Java Verification](https://mlsanity.com/paper/2502.01573/) (2025)
- [AutoProof: Auto-active Functional Verification of Object-oriented Programs](https://mlsanity.com/paper/1501.03063/) (2015)

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

- [Uplifted Attackers, Human Defenders: The Cyber Offense-Defense Balance for Trailing-Edge Organizations](https://mlsanity.com/paper/2508.15808/) (2025)
- [AI for software engineering: from probable to provable](https://mlsanity.com/paper/2511.23159/) (2025)

## Abstract (arXiv)

Among areas of software engineering where AI techniques -- particularly, Large Language Models -- seem poised to yield dramatic improvements, an attractive candidate is Automatic Program Repair (APR), the production of satisfactory corrections to software bugs. Does this expectation materialize in practice? How do we find out, making sure that proposed corrections actually work? If programmers have access to LLMs, how do they actually use them to complement their own skills? To answer these questions, we took advantage of the availability of a program-proving environment, which formally determines the correctness of proposed fixes, to conduct a study of program debugging with two randomly assigned groups of programmers, one with access to LLMs and the other without, both validating their answers through the proof tools. The methodology relied on a division into general research questions (Goals in the Goal-Query-Metric approach), specific elements admitting specific answers (Queries), and measurements supporting these answers (Metrics). While applied so far to a limited sample size, the results are a first step towards delineating a proper role for AI and LLMs in providing guaranteed-correct fixes to program bugs. These results caused surprise as compared to what one might expect from the use of AI for debugging and APR. The contributions also include: a detailed methodology for experiments in the use of LLMs for debugging, which other projects can reuse; a fine-grain analysis of programmer behavior, made possible by the use of full-session recording; a definition of patterns of use of LLMs, with 7 distinct categories; and validated advice for getting the best of LLMs for debugging and Automatic Program Repair.