Evaluating Symbolic Feedback Granularity for LLM-Based Program Repair

Abstract

Large Language Models (LLMs) are increasingly incorporated into verifier-in-the-loop software engineering systems, yet it remains unclear how the representation of verifier feedback affects their ability to repair incorrect programs. We study this question by isolating feedback representation from model, task, and prompting effects. We compare five feedback modalities ranging from binary verification status to natural language explanations, concrete counterexamples, and raw symbolic traces. We evaluate four open-weight code models spanning 7B to 480B total parameters on a 540-task benchmark combining controlled verification tasks with contractannotated problems derived from HumanEval+ and MBPP+. Counterexample feedback achieves the strongest repair performance across the evaluated models, while full symbolic traces provide substantially more information without yielding corresponding gains. A token-matched padding control shows that prompt length explains only part of the observed gap, while a redundant-feedback ablation shows that adding a full trace to an already actionable counterexample does not improve repair performance. These results suggest that the interface between formal verification and neural program repair should be treated as a representation problem rather than simply an information-maximization problem.