Source-linked AI summary
Counterexamples as Feedback for Agent Self-Correction
Sidhesh Badrinarayan, Adithya Parthasarathy
TL;DR
Single-turn metrics do not measure whether agents efficiently repair wrong artifacts, preserve correct behavior, or remain robust under harder tests. A-CEGIS evaluates multi-turn regex refinement using deterministic full-match verification and concrete counterexample witnesses; diagnostic feedback reaches 0.900 Pass@final within four turns, while hardening exposes remaining robustness gaps.
Problem
Single-turn metrics such as pass@1 do not measure repair efficiency, revision stability, or robustness under harder tests.
Method
A-CEGIS measures agent repair by iteratively verifying proposed regexes with deterministic re.fullmatch semantics and returning concrete false-positive or false-negative witnesses.
Results
Diagnostic A-CEGIS reaches 0.900 Pass@final within four turns, and the full diagnostic loop solves all hidden-set tasks while hardening reports robust success of 0.767.
Takeaways & Limitations
A-CEGIS evaluates refinement as a trajectory, making convergence, regressions, repair behavior, and robustness visible beyond endpoint success.
Takeaways & Limitations
Hardening identifies seven non-robust cases involving boundary under-specification, wildcard overreach, and class-boundary confusion.
Abstract
from arXiv · showhide
Single-turn code-generation metrics understate a central property of deployed agents: whether they can repair a wrong artifact after receiving concrete feedback. This paper presents A-CEGIS, a lightweight framework that uses counterexamples as feedback for evaluating multi-turn refinement in natural-language-to-regex synthesis. An agent proposes a regex, a deterministic oracle checks it under full-match semantics, and compact false-positive or false-negative witnesses guide the next turn. On 30 NL-RX-Turk tasks, diagnostic counterexample feedback solves 90\% of tasks within a four-turn ablation budget, compared with 17% for zero-shot generation, 27% for generic self-correction, and 23% for error-only feedback. In a full diagnostic run with hardening, all tasks are solved on the hidden set by the final turn, with mean time-to-success of 2.7 turns and robust success of 77% after targeted probing. These results show that A-CEGIS measures how efficiently an agent improves across turns while adding a practical robustness check beyond the original held-out cases.
1 Introduction
A-CEGIS evaluates whether agents can repair incorrect regexes through concrete feedback, addressing limits of one-shot metrics. It uses deterministic counterexamples to measure multi-turn refinement.
- One-shot metrics do not measure repair efficiency, revision stability, or robustness after apparent success.
- Regex synthesis provides a controlled setting for studying refinement because artifacts are executable and correctness is deterministically testable.
- 0.900 hidden-set success was achieved within four turns with diagnostic A-CEGIS, versus 0.167 zero-shot, 0.267 generic self-correction, and 0.233 error-only feedback.
- A full diagnostic run reached 1.0 hidden-set success and 0.767 robust success after targeted hardening.
2 Background and Related Work
Prior work emphasizes first-attempt quality, while newer research motivates process-level evaluation for repair and interaction. A-CEGIS isolates whether deterministic evidence enables efficient repair of compact formal artifacts.
- Existing evaluations emphasize first-attempt quality, exact match, and single-step completion, motivating measures of error recovery and process.
- Generic feedback can be noisy, while tool-mediated benchmarks may mix repair skill with retrieval, action selection, and interface effects.
- A-CEGIS asks whether agents can efficiently repair compact formal artifacts when deterministic failure evidence is available.
- The framework adapts counterexample-guided revision to language-agent evaluation without claiming full equivalence proof from finite tests and targeted probes.
3 Methodology
The methodology combines deterministic regex evaluation, generated task-local tests, counterexample feedback, trajectory metrics, and targeted hardening. It distinguishes hidden-set success from robustness under semantic-boundary probing.
- 3.1 Oracle construction: The harness evaluates Python-compatible regexes deterministically using generated positive and negative examples for each task.The reported configuration uses 12 generated positives and 12 generated negatives.
- 3.1 Oracle construction: Generated negatives come from mutations and random samples retained only when rejected by the gold regex.
- 3.1 Oracle construction: At each turn, diagnostic feedback provides up to two false negatives and two false positives, indicating whether the candidate language should broaden or tighten.
- 3.1 Oracle construction: The strategy ablation varies only the information returned after failure across zero-shot, generic, error-only, and diagnostic feedback conditions.
- 3.2 Hardening protocol: Hardening searches task-local probes near description tokens, regex literals, examples, and simple string transformations after hidden-set success.
- 3.2 Hardening protocol: Robust success requires passing the expanded test set and a final probe pass with no remaining mismatches.
- 3.2 Hardening protocol: The benchmark reports endpoint and process metrics including Pass@1, Pass@final, time-to-success, MRR, repair locality, and refinement efficiency.Refinement efficiency uses fixed cases and regressions to characterize whether repair is net constructive.
4 Experiments and Results
The experiments evaluate diagnostic counterexample feedback against weaker feedback strategies and measure refinement through convergence, trajectory quality, stability, and targeted robustness. Diagnostic A-CEGIS solves all 30 tasks on the hidden set in the full run, while hardening exposes residual semantic errors that hidden-set success misses.
- Full diagnostic run: All 30 tasks are solved by the full diagnostic loop, despite only 5 being solved immediately.The mean initial pass rate is 0.706, indicating that initial regexes are often close but incomplete.
- Trajectory metrics: RER is 2.61, with 311 fixes against 99 breaks, indicating net constructive rather than oscillatory refinement.The MRR of 0.477 indicates that gains are distributed across a few turns rather than arising only from final-turn rescue.
- Feedback-strategy ablation: Diagnostic A-CEGIS solves 27 of 30 tasks within four turns, compared with 8 for generic self-correction, 7 for error-only feedback, and 5 for zero-shot generation.All strategies use the same model and task set under the same four-turn budget.
- Convergence: The first successful turn is typically early: 25 of 30 tasks are solved after turn 1, and no task requires more than six turns.The mode is turn 2, and trajectories often make a small number of semantically meaningful changes.
- Hardening and robustness: Only 23 of 30 tasks remain probe clean after hardening; seven pass sampled tests but fail targeted variants involving boundaries, repetitions, or broad character classes.These failures show that hidden-set success can validate sampled behavior while missing the intended language shape.
- Hardening and robustness: Hardening often removes permissiveness, such as tightening .*dog.*|\S to dog|[A-Za-z0-9_], while the reported stability score is 0.561.The recurring failures involve boundary under-specification, wildcard overreach, and class-boundary confusion.
- Interpretation: A-CEGIS exposes both recovery ability and residual robustness gaps that Pass@1 or final hidden success alone would miss.The measurement layers distinguish initial synthesis, convergence, constructive repair, and reliability under targeted probing.
5 Example A-CEGIS Run
A typical A-CEGIS run uses directional counterexamples to turn a near-miss regex into a targeted repair. The resulting traces distinguish local edits from larger rewrites and make the process auditable.
- Example A-CEGIS Run: A false negative signals that the regex is too narrow, while a false positive signals that it is too broad.The oracle separates failures by direction before the next candidate is generated.
- Example A-CEGIS Run: The next candidate is conditioned on a behavioral correction rather than a vague request for improvement.Typical repairs address a missed boundary condition after the oracle returns compact witnesses.
- Example A-CEGIS Run: Structural stability and RER distinguish local edits from larger rewrites by recording edit locality and whether changes fix more cases than they break.The released artifacts include per-task candidate sequences and probe-derived counterexamples for inspection.
6 Discussion
A-CEGIS evaluates agent repair as a measurable process using compact formal artifacts, deterministic verification, and concrete counterexamples. Its trajectory metrics and targeted hardening distinguish convergence from brittle success and support broader applications.
- 6 Discussion: 0.900 Pass@final within four turns shows diagnostic witnesses outperform generic self-correction and error-only feedback for targeted repair.The witnesses indicate whether the regex language should be broadened or tightened, rather than leaving the model to infer failure from a scalar score.
- 6 Discussion: Pass@1, final hidden success, RER, and stability measure initial difficulty, convergence, constructive revision, and local repair behavior.These trajectory metrics add information that endpoint scores cannot provide.
- 6 Discussion: Targeted hardening probes semantic boundaries after hidden-set success to test whether recovered expressions remain reliable under additional cases.The probes focus on description tokens, regex literals, and existing examples.
- 6 Discussion: A-CEGIS can generalize beyond regexes when a task has a compact formal artifact, deterministic oracle, and renderable counterexamples.The discussion names SQL queries, schemas, and configuration policies as candidate domains.
7 Conclusion and Future Work
A-CEGIS argues that agent refinement should be evaluated as a trajectory rather than by a single endpoint score. It records failures, fixes, regressions, and robustness probes so evaluations can distinguish success from reliable improvement.
- 7 Conclusion and Future Work: 0.900 four-turn Pass@final and 1.0 full diagnostic hidden-set success show strong repair performance, while hardening exposes a remaining robustness gap.The framework reports both endpoint success and performance under additional probing.
- 7 Conclusion and Future Work: Future work can scale the benchmark across models, add exact equivalence checks where available, and extend the pattern to other formal artifacts.Proposed domains include SQL queries, schemas, configuration policies, and program fragments.
- 7 Conclusion and Future Work: Trajectory evaluation preserves candidate sequences, counterexamples, fixes, and breaks to show how agents improve across turns.This distinguishes whether agents succeed from how they reach success.