Agentic Synthesis against Counterexample-Supplemented Sketches

🕒 Published (v1): 2026-07-17 11:11 UTC · Source: Arxiv · link

Why this paper was selected

Counterexample-supplemented synthesis prevents coding agents from repeating domain-rule violations

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

Coding agents can satisfy a failing test while violating the domain rule that caused the failure, leaving that rule unrecorded so future runs repeat the same mistake. This paper introduces Sketch-CE (counterexample-supplemented sketches), a repository-native loop where every operator-approved failure forces a reviewed revision of a governing sketch before a new candidate implementation is generated. A synthetic experiment with GPT-5.4-mini shows that rebuilding from the evolved sketch passes 19/21 withheld cases versus 15/21 when rebuilding from the initial sketch with all examples replayed.

Problem

LLM coding agents produce plausible patches — ones that pass available tests and match local style — while violating unencoded domain rules. Because those rules live only in chat transcripts, reviewer memory, or PR comments, the next agent invocation can make the identical forbidden repair. Existing workflows (tests, prompts, CEGIS under formal assumptions) do not provide a repository-level mechanism that (a) ties an SME correction to a reviewed sketch clause and (b) enforces that no new implementation is accepted until the clause passes a regression gate.

Method

Sketch-CE organizes synthesis around six repository artifacts:

1. Sketch \(S\) — a human-authored, agent-editable partial program (prose + code-shaped structure) recording permitted and forbidden repairs.
2. Archive \(A\) — the complete set of operator-approved counterexamples, each carrying observed input, corrected output, tempting wrong output, the rule distinguishing them, and the sketch revision it caused.
3. Regression set \(R \subseteq A\) — a curated executable subset that discriminates against known-wrong implementations without requiring the full archive to run as generation context.
4. Known-code anchors \(K\) — existing APIs, result types, fixtures, and conventions the agent must not reinvent.
5. Implementation surface — either Oracle A (deterministic code for encodable rules) or Oracle B (prompt-mediated completion for narrative/under-encoded rules), both constrained by \(S\) and checked by \(G\).
6. Gate \(G\) — a two-layer validator: replay checks that the world state reaches the approved expected state; semantic compare checks that policy-bearing fields (operation, target, date, status) match the approved output.

The loop is: observe a failure → SME provides corrected output + rule → operator explicitly approves → Developer revises \(S\), code, and prompt for that one counterexample → \(G\) runs over the active case and \(R\) → green: curate \(R\) and reveal next case; red: return one failed regression for implementation repair. Crucially, the agent never sees the archive as bulk context; it sees one active failure at a time under the evolved \(S\).

The design adapts CEGIS to a repository setting where templates, specifications, and checkers cannot all fit inside a formal language, replacing the solver-backed search with a coding agent and replacing formal proof with a finite-regression predicate over \(R\).

Key Contributions

• Counterexample-supplemented sketch: a repository-native artifact that co-locates sketch clause, operator decision, archive record, implementation surface, and gate check for every accepted counterexample.
• Process model: formalizes the operator-approval step as the only authority that promotes a failure to specification status and mandates a sketch revision before implementation is accepted.
• Dual-oracle decomposition: Oracle A (deterministic code) for fully encodable rules; Oracle B (prompt-mediated) for narrative/judgment holes — both subject to the same gate pressure.
• Finite-regression theorem (with stated proof obligation): the gate's replay/compare predicate provides a bounded correctness claim over \(R\) under current repo semantics.
• CatSynth: a fully inspectable synthetic browser application with captured experiment logs and reproduction supplement (Appendix A) demonstrating the complete artifact chain.

Results

All figures are from a single open-world run with GPT-5.4-mini on CatSynth with one reveal order:

• 8 of 14 frozen candidate cases were promoted to counterexamples.
• Rebuild from evolved sketch: 19/21 withheld cases passed.
• Rebuild from initial sketch + replay all accepted examples: 15/21 withheld cases passed.
• Retain code across counterexamples (incremental repair): 18/21 withheld cases passed, with 9 Developer calls and 719 lines of cumulative artifact churn.
• Replay-all path: 15/21 withheld cases passed, with 15 Developer calls and 2,394 lines of artifact churn.
• Authors explicitly state results "do not establish general superiority or correctness beyond the encoded checks."

Limitations

• Single model (GPT-5.4-mini) and single reveal order; no statistical replication or multi-model comparison.
• CatSynth uses synthetic data and public rules; the enterprise deployment that motivated the method is described but its data is not publicly available.
• The gate provides only a bounded claim over \(R\); it is not a proof of correctness outside those artifacts.
• The regression set \(R\) must be manually curated; no principled selection algorithm is provided.
• Oracle B prompt surfaces still rely on LLM-completion, carrying the usual prompt-fragility risks even when versioned in the repository.
• The operator approval step is a process requirement with no automated enforcement; the paper acknowledges that if Developer silently rewrites the sketch, "the protocol has failed."

Relevance to Agentic AI / LLM Agents

This paper directly addresses one of the core failure modes of agentic coding systems: agents optimize for locally checkable signals (tests, style) while violating domain rules that have not been encoded as repository artifacts. The Sketch-CE loop provides a concrete protocol for incrementally transferring domain knowledge from SME judgment into the repository through operator-gated counterexample approval — a human-in-the-loop mechanism that is formal enough to be enforced by tooling. It connects to the emerging spec-driven agent paradigm (Kiro, GitHub Spec Kit) but distinguishes itself by placing counterexample approval and sketch revision inside the repair protocol rather than treating them as upstream exceptions. For researchers tracking agentic workflows, this paper provides both a formal artifact model and a worked empirical trace that is more transparent about its evidentiary limits than most benchmark-driven agent papers.