# Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 14 of its 42 references that are in the map.
- First posted on arXiv 19 Dec 2024.

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

- [LLaMA: Open and Efficient Foundation Language Models](https://mlsanity.com/paper/2302.13971/) (2023)
- [Code Llama: Open Foundation Models for Code](https://mlsanity.com/paper/2308.12950/) (2023)
- [CodeGemma: Open Code Models Based on Gemma](https://mlsanity.com/paper/2406.11409/) (2024)
- [Graph-based, Self-Supervised Program Repair from Diagnostic Feedback](https://mlsanity.com/paper/2005.10636/) (2020)
- [CodeHelp: Using Large Language Models with Guardrails for Scalable Support in Programming Classes](https://mlsanity.com/paper/2308.06921/) (2023)
- [Repair Is Nearly Generation: Multilingual Program Repair with LLMs](https://mlsanity.com/paper/2208.11640/) (2022)
- [Automated Clustering and Program Repair for Introductory Programming Assignments](https://mlsanity.com/paper/1603.03165/) (2016)
- [Learning Syntactic Program Transformations from Examples](https://mlsanity.com/paper/1608.09000/) (2016)
- [sk_p: a neural program corrector for MOOCs](https://mlsanity.com/paper/1607.02902/) (2016)
- [Data-Driven Feedback Generation for Introductory Programming Exercises](https://mlsanity.com/paper/1711.07148/) (2017)
- [Verifix: Verified Repair of Programming Assignments](https://mlsanity.com/paper/2106.16199/) (2021)
- [C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments](https://mlsanity.com/paper/2206.08768/) (2022)
- [InvAASTCluster: On Applying Invariant-Based Program Clustering to Introductory Programming Assignments](https://mlsanity.com/paper/2206.14175/) (2022)
- [Combining Logic with Large Language Models for Automatic Debugging and Repair of ASP Programs](https://mlsanity.com/paper/2410.20962/) (2024)

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

- [Are Large Language Models Robust in Understanding Code Against Semantics-Preserving Mutations?](https://mlsanity.com/paper/2505.10443/) (2025)
- [Procedural Refinement by LLM-driven Algorithmic Debugging for ARC-AGI-2](https://mlsanity.com/paper/2603.20334/) (2026)
- [MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku](https://mlsanity.com/paper/2607.12711/) (2026)
- [SkillEvoReg: Regularizing Agent Skill Evolution Against Overfitting](https://mlsanity.com/paper/2609.30861/) (2026)
- [Model-Based Diagnosis with Multiple Observations: A Unified Approach for C Software and Boolean Circuits](https://mlsanity.com/paper/2512.02898/) (2025)
- [Property-Guided LLM Program Synthesis for Planning](https://mlsanity.com/paper/2605.16142/) (2026)
- [Bulkhead: Automated Semantic Detection and Remediation of Container Escape Vulnerabilities](https://mlsanity.com/paper/2607.12723/) (2026)
- [Natural-Language to SysMLv2 Translation via Conformance-Driven Iterative Refinement](https://mlsanity.com/paper/2607.14162/) (2026)

## Abstract (arXiv)

Automated Program Repair (APR) for introductory programming assignments (IPAs) is motivated by the large number of student enrollments in programming courses each year. Since providing feedback on IPAs requires substantial time and effort from faculty, personalized feedback often involves suggesting fixes to students' programs. Formal Methods (FM)-based semantic repair approaches, check a program's execution against a test suite or reference solution, are effective but limited. These tools excel at identifying buggy parts but can only fix programs if the correct implementation and the faulty one share the same control flow graph. Conversely, Large Language Models (LLMs) are used for APR but often make extensive instead of minimal rewrites. This leads to more invasive fixes, making it harder for students to learn from their mistakes. In summary, LLMs excel at completing strings, while FM-based fault localization excel at identifying buggy parts of a program. In this paper, we propose a novel approach that combines the strengths of both FM-based fault localization and LLMs, via zero-shot learning, to enhance APR for IPAs. Our method uses MaxSAT-based fault localization to identify buggy parts of a program, then presents the LLM with a program sketch devoid of these buggy statements. This hybrid approach follows a CEGIS loop to iteratively refine the program. We ask the LLM to synthesize the missing parts, which are then checked against a test suite. If the suggested program is incorrect, a counterexample from the test suite is fed back to the LLM. Our experiments show that our counterexample guided approach, using MaxSAT-based bug-free program sketches, significantly improves the repair capabilities of all six evaluated LLMs. This method allows LLMs to repair more programs with smaller fixes, outperforming other configurations and state-of-the-art symbolic program repair tools.