Specifications Are Decision Boundaries

“Make only the door blue.” Give that instruction to a model along with an SVG of a house and you get back a house with a blue door. The render is identical to the one you wanted. Open the XML and the roof has moved up one pixel, and the right window has been re-rendered with different path data. CLIP similarity says pass. FID says pass. Pixel IoU says pass. Anyone who reads the diff says no.

That gap is the subject of this essay, and of the paper that grew out of it: SVGym, a benchmark for surgical SVG editing, and SCALPEL, the RL recipe that trains a 7B open model on it. Pixel metrics will not close the gap. RLHF will not close it. Four old ideas from program synthesis will: mutation testing, counterexample-guided induction, version-space algebras, refinement types. Put together the right way they become a way to train agents that know what not to change. The idea generalises far past SVGs.

The silent rewrite

Here is the instruction and three outputs. The rasters are indistinguishable. The XML is not:

Original

rasterspec

Looks correct

raster passspec fail

Spec-correct

raster passspec pass

One prompt, three outputs Fig. 01 · Interactive One prompt, three outputs. The middle one drifted the roof up a pixel and re-rendered the right window. CLIP, FID and pixel IoU all pass it. The diff does not.

Notice that the third panel and the second panel render to the same pixels. The only thing that separates them is a tree diff. This is the visual analogue of a unit test that passes while corrupting an invariant nobody wrote a test for. Surface metrics reward the picture. Specifications care about the diff.

Specification leakage

This is one failure mode wearing many costumes. The unit test passes and the migration corrupted a column. The lint is clean and the refactor renamed a public symbol. The render looks right and the SVG tree is unrecognisable. In every case the agent satisfied what was measured, not what was meant.

Call it specification leakage. It is the bottleneck on every agent domain with structured outputs: code, UI trees, CAD scripts, robot policies. Pixels are just the easiest place to watch it bite.

A verifier that hands back counterexamples

Grading a candidate against a structured set of accept and reject examples is not new. It has been the central loop of program synthesis since the 2000s.

Armando Solar-Lezama's Sketch system [Solar-Lezama 2006] introduced what is now the dominant pattern in the field: counterexample-guided inductive synthesis, CEGIS.¹ A synthesiser proposes a candidate program. A verifier, typically an SMT solver,² checks it against a logical spec. If the verifier finds a violation it returns a concrete counterexample input. The synthesiser refines on the expanded example set. Loop until the verifier signs off. Sketch, BRAHMA [Gulwani 2011], Rosette [Torlak and Bodík 2013], the synthesis-style superoptimisers: all CEGIS underneath. The verifier is the only sharp tool in the toolkit.

What we are doing has the same shape with two substitutions:

CEGIS, 2006

Synthesiserproposes a program

candidate

Verifier (SMT)checks it against a logical spec

violation

Counterexamplea concrete input that breaks it

add to example set

no violation: done

This work, 2026

Neural policy (7B)samples an edit

rollout

Mutant generatorprecomputed M⁺ / M⁻ per task

score

Rewardcloser to M⁺, farther from M⁻

gradient update

negative mutants = counterexamples · positive mutants = witnesses

CEGIS, and this work Fig. 02 · Two loops CEGIS, and the same loop with a neural policy proposing and a mutant generator refuting. The verifier stops solving constraints and starts precomputing accept/reject artifacts.

The verifier becomes a mutant generator: it does not solve constraints, it precomputes a family of accept and reject artifacts for each task. The synthesiser becomes a neural policy: it does not search over programs symbolically, it samples from a distribution and takes gradient updates. Negative mutants are exactly what CEGIS calls counterexamples, concrete artifacts the policy must learn not to produce. Positive mutants are witnesses, the synthesis literature's name for “this also satisfies the spec.”

The reason this works is the reason CEGIS works. A small set of well-chosen accept and reject examples nails down a specification much more precisely than any single reference output ever could.

Where the mutants come from

CEGIS needs a verifier. Ours comes from a fifty-year-old idea on the test-quality side of the same field: mutation testing³ [Lipton 1971; DeMillo, Lipton and Sayward 1978]. The original tool grades a test suite by programmatically perturbing a function and asking whether the tests notice. We flip its role entirely. Mutants are labels, not adversaries.

For every editing task, the same code that generates the task also generates two structured sets of nearby artifacts:

M⁺ · satisfy

door = blue

M⁻ · violate

The mutant lattice for “door = blue” Fig. 03 · M⁺ above, M⁻ below The mutant lattice for “door = blue”. Above the line, valid blues; the door is the door and only the colour varies. Below it, a window deleted, the roof shifted, the door moved, the wrong object recoloured. The spec is the line between the rows.

You now have ground truth without humans, without a learned judge, without a single canonical reference output. The mutants come from the same family-specific code that defines the task. They are free.

Specifications as decision boundaries

This is the load-bearing idea. A specification is a decision boundary: the line that separates M⁺ from M⁻. It is not a reference answer. It is a region of program space defined by what it is closer to than to its alternatives.

The type-theoretic name for this already exists. A refinement type⁴ [Freeman and Pfenning 1991; Liquid Haskell] is a base type sharpened by a predicate that carves out a subset of inhabitants. { door : Colour | door = blue ∧ ∀o ≠ door. o = o₀ } is the spec. The mutant lattice is a sampled view of that subset and its complement. Mutation-consistency RL, seen this way, is learning to produce refinement-typed outputs without ever writing the refinement down as a logical formula.

One example is never enough

When Sumit Gulwani's FlashFill [Gulwani 2011] shipped inside Excel it solved a deeper problem than its UI suggested: given one or two input-output examples, find the program that generalises the way the user actually meant. The mechanism was a version-space algebra,⁵ a compact representation of every program in some DSL consistent with the examples seen so far.

What FlashFill teaches is structural. One example is almost always ambiguous. The instruction “door = blue” on its own is consistent with at least six programs:

prompt · door = blue

π₁door.fill ← #3a7ad9 (one specific blue)
π₂door.fill ← any blue from BLUES
π₃∀ d ∈ doors: d.fill ← blue
π₄door.fill ← blue; door.stroke ← bluestroke changed
π₅delete door; insert new blue door at same coordspreservation violated
π₆tint entire scene with blue overlaypreservation violated

The version space for “door = blue” Fig. 04 · Six programs The version space for “door = blue”. Every program listed is consistent with the prompt alone. The negative mutants kill three of them; the three that survive are the spec.

The negative-mutant set is the disambiguator. It carves the version space down to the programs the instruction meant. Modern programming-by-example systems do this with example expansion. We do it with one shot of counterexamples per task. Same primitive, different optimiser.

Why imitation cannot learn preservation

Supervised fine-tuning is imitation: here is the right output, copy it. To teach “leave everything you weren't asked about alone” you would need a label for every non-change, and there are infinitely many of those. The space of things to preserve is unboundedly larger than the space of things to edit, and SFT scales with example count.

RL with a counterfactual reward sidesteps the asymmetry. The reward says “you lost points for moving anything I didn't mention,” and gradient descent does the rest. Preservation is the structurally hard part of editing, and it is precisely the part SFT cannot supervise cheaply.

The copy trap

Our first reward was naive: +1 for matching any positive mutant. Within a few hundred GRPO steps the policy converged on something technically optimal and obviously wrong. It learned to copy a positive mutant verbatim and ignore the prompt entirely. Maximum reward, zero understanding. A textbook reward hack.⁶

The fix is the geometry of the spec itself: subtract similarity to the negative mutants (repulsion), and gate on a preservation term that requires every object the prompt did not mention to remain bit-equivalent to the original.

Naive reward · M⁺ only

policy copies one M⁺

Mutation-consistency reward

policy spans the spec region

Two rewards, two policies Fig. 05 · 28 rollouts each Two rewards, two policies, 28 rollouts each after 1k GRPO steps. Pure attraction collapses every rollout onto one copied artifact. Repulsion from M⁻ plus a preservation gate spreads them across the valid region, which is exactly what the spec permits.

Any reward that is only attractive is gameable. You need repulsion. This is Goodhart's law⁷ in its ML form, and it shows up the moment your reward stops being a comparison.

The group is the baseline

We train with GRPO⁸ [Shao et al. 2024, DeepSeekMath], group-relative policy optimisation. Sample K = 8 rollouts per prompt, score each one, normalise advantages within the group, reinforce the above-average rollouts and push away the below-average ones. No value function. No critic. Just relative ranking inside a group:

group mean 0.56

rollout 1 · 0.91
rollout 2 · 0.84
rollout 3 · 0.78
rollout 4 · 0.62
rollout 5 · 0.55
rollout 6 · 0.41
rollout 7 · 0.28
rollout 8 · 0.12

Eight rollouts on one ruler Fig. 06 · GRPO Eight rollouts on one ruler. The group mean is the whole baseline; the rollouts above it are reinforced, the ones below it are suppressed, and no critic had to predict anything.

The match between GRPO and this reward is not accidental. The reward is already group-relative: better than the negatives, worse than the positives. PPO with a critic would be wasted machinery, learning to predict a number we can read directly off the mutant set.

Fifty-five years on one page

To place this in context, this is the sequence of ideas the paper rearranges. None of the pieces are new. The arrangement is:

1971Mutation testing (Lipton)Programmatic mutants as a measure of test-suite adequacy. The mutator is the primitive.
1980Inductive synthesis from examples (Summers, Shaw)Learn a recursive program from input-output pairs. The first version-space ideas.
2006Sketch / CEGIS (Solar-Lezama)Synthesiser proposes, SMT verifier returns counterexamples, repeat. The dominant pattern since.
2011FlashFill (Gulwani)Version-space algebras for string transformations from one or two examples. Ships in Excel.
2017RobustFill, DeepCoder (Balog, Devlin et al.)Neural policies learn to propose; symbolic verifiers still close the loop.
2024GRPO / verifiable rewards (Shao et al.)RL with executable reward functions overtakes RLHF on math and code. Critic-free, group-relative.
2026Mutation-consistency RL (this work)Mutators replace solvers; policy gradients replace candidate search; the spec is implicit in the lattice.

Fifty-five years of synthesis by example Fig. 07 · Timeline Fifty-five years of synthesis-by-example. The same primitive, a small set of structured examples grounds a specification, applied at every level of the stack, from test quality to type theory to optimiser design.

Read the descriptions in a column and the pattern is one sentence long: somebody finds a cheap way to generate structured accept/reject examples, and somebody else uses them to pin down what a program is supposed to mean.

The result that matters

Prompting matches pictures. SFT matches pictures. Only RL with counterfactual rewards matches the spec. The gap is largest exactly where you would expect it, on the Unintended Change Rate, the fraction of unmentioned objects that drift, because that is the metric the other two regimes were never trained to optimise.

More telling than the headline number is where SFT fails: on the long tail of small, plausible, locally invisible mutations. A minor recolour of an unmentioned object. Path data drifting under reformatting. An ID renamed in a way that breaks downstream tooling. Each of these slips past a human reviewer glancing at the render. Mutation rewards catch them because the output measurably drifts toward a known M⁻.

Five other domains

The recipe transfers wherever you have a structured program and a mutator. The same idea in five languages:

Domain	Positive mutant, M⁺	Negative mutant, M⁻
SVG edit	a different valid shade of blue	a window silently deleted
Code refactor	α-equivalent rename, tests pass	public type signature changed
UI edit	ARIA label updated, focus order intact	tabindex shuffled, focus broken
CAD script	hole moved, parent feature preserved	parent feature reparented
Robot policy	grasp succeeds, end-effector pose matches	grasp succeeds but knocks over object B

SVG is the cleanest demo. The unifying claim is stronger: every domain with a structured output has a mutator, and every mutator is a free oracle.

The recipe

If you want to train an agent that respects a specification, do not show it the right answer. Show it a small set of right answers and a small set of plausibly wrong answers, and let RL learn the boundary. The right answer is rarely unique; the boundary almost always is.

Two predictions I would defend in print. First, agent benchmarks will move from “one reference output” to “a set of acceptable outputs plus a set of forbidden ones,” because that is how you actually measure preservation. Second, RL on agents will look less like RLHF, with learned reward models that inherit the same surface-metric hacks they were meant to fix, and more like this: executable counterfactual oracles, written once per task family, free to call a million times during training.

The pivot is philosophical, not algorithmic. Once you stop treating the spec as an answer key and start treating it as a boundary, almost every interesting agent-training problem rearranges itself around the same ancient idea: meaning is operationalised by what you can distinguish from it. Two of the three houses at the top of this essay have a blue door. Only one of them is still the house you started with.

The benchmark (SVGym) and the training results (SCALPEL) live in the paper, published as Vector-Bench (opens in a new tab). This essay is the idea that makes them work.