AI systems research / Course research / 2026
Can symbolic counterexamples
help an AI repair code?
I built a software-repair loop that combines language-model patches with program context, solver checks, counterexamples, and real tests. On one held-out SymPy subset, the full feedback loop solved more tasks—while using more time and tokens.
01 / The research question
A failed patch contains
information for the next one.
Language models can propose plausible edits, but plausibility is not the same as correctness. The project asked whether program structure and symbolic counterexamples could turn a failed attempt into useful, targeted feedback for another repair.
The test was deliberately narrow: compare four repair conditions through the same harness, then judge each result with the repository’s real tests.
02 / System
Generate. Check.
Learn from the failure.
The system preserves a simple loop: choose relevant context, generate a patch, test it, and send structured failure evidence back into the next attempt.
Select context
Use the failure and repository structure to collect the code most likely to matter.
→Generate a patch
Ask the language model for a concrete repair against that bounded context.
→Check behavior
Apply the patch, run tests, and optionally inspect affected paths with slicing and a solver.
→Return evidence
Convert failures and symbolic counterexamples into feedback for the next repair attempt.
03 / Role
My contribution
I built the Python repair system that connects LLM patch generation, repository context selection, program slicing, CrossHair and Z3 verification, counterexample-guided critique, patch application, pytest evaluation, and reproducible experiment artifacts.
Repair orchestration
Coordinated prompt context, patch attempts, application failures, feedback, and iteration budgets.
Symbolic feedback
Translated solver checks and counterexamples into critique the next repair attempt could use.
Evaluation
Ran the same held-out tasks across four conditions and retained per-task evidence instead of only aggregate scores.
The public repository documents the implementation and reproducible experiment workflows. The result below describes one final held-out study, not a general benchmark claim.
04 / Evidence
The complete loop solved more.
It also cost more.
Across a held-out 14-task SymPy subset, the neural-only condition resolved 2 of 14 tasks (14.3%). The full counterexample-guided condition resolved 5 of 14 (35.7%).
neural_only 2 of 14 · 14.3% neural_slicing 3 of 14 · 21.4% neural_solver 3 of 14 · 21.4% neural_cegf 5 of 14 · 35.7% The tradeoff matters
The strongest condition also had a higher token and runtime cost: about 30,026 average tokens and 16.6 seconds, compared with about 16,747 tokens and 8.6 seconds for neural_only.
05 / Friction
What the result does not prove
Narrow scope. The study covers one repository family and 14 tasks; it cannot establish performance across software repair broadly.
Incomplete solver reach. Symbolic checks covered 11 of the 14 tasks, so the feedback mechanism was not equally available everywhere.
Patch reliability. Some generated edits still failed to apply cleanly, limiting how much the later checks could help.
Resource cost. More context and feedback improved this small result while nearly doubling average runtime and substantially increasing tokens.
06 / Next action
Make the loop more selective.
The supported conclusion is modest: symbolic feedback improved one small held-out result, and the next problem is making that gain cheaper, more reliable, and repeatable.
Return to selected work