This is the implementation of Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization [1] accepted at AAAI 2025.
In this work, we propose a novel approach that combines the strengths of both Formal Methods (FM)-based fault localization and Large Language Models (LLMs), via zero-shot learning, to enhance Automated Progra Repair (APR) for introductory programming assignments (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 Counterexample Guided Inductive Synthesis (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 for revised synthesis.
All the python requirements are in the requirements.txt file.
Our work has been evaluated using one benchmark of C programs: C-Pack-IPAs [2]. C-Pack-IPAs is a set of student programs collected during an introductory programming course for twenty-five assignments over three distinct academic years, comprising 1431 faulty programs.
For the fault localization module we used CFaults [3], which is a Formula-Based Fault Localization in C with Multiple Test Cases.
Our results can be found in a sqlite3 database in database/aaai25-results.db.
-
repair_CPackIPAs.shCalls our LLM-based repair agent on the C-Pack-IPAs dataset. This script can be run with the -h flag to display a help message.
-
repair.pyLLM-based repair using BentoML servers.
-
how_to_run_RepairAgents.shCommands to run all the RepairAgents.
-
how_to_run_LLMs.shCommands to launch all LLMs in different GPUs.
-
LLMs/Contains the BentoML servers for each different LLM.
-
mentor/Contains several python3 classes that help in the repair process.
The source code for this work is also publicly available at https://github.com/pmorvalho/LLM-CEGIS-Repair.
This repository should not be used to reproduce the paper, but it contains the current version of our code and will continue to be developed and shared with the research community.
[1] P. Orvalho, M. Janota, and V. Manquinho. Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization. In the 39th Annual AAAI Conference on Artificial Intelligence, AAAI 2025. PDF.
[2] P. Orvalho, M. Janota, and V. Manquinho. C-Pack of IPAs: A C90 Program Benchmark of Introductory Programming Assignments. In the 5th International Workshop on Automated Program Repair, APR 2024, co-located with ICSE 2024. GitHub. PDF.
[3] P. Orvalho, M. Janota, and V. Manquinho. CFaults: Model-Based Diagnosis for Fault Localization in C with Multiple Test Cases. The 26th International Symposium on Formal Methods, FM 2024. GitHub. PDF.