CEGIS: Counterexample-Guided Program Synthesis

Synthesis Run

Search domain radius D 6

Candidate lattice radius R 6

Playback speed 1.0×

Verifier State

spec: f(x) = a·x + b (a, b hidden)

Iteration

Consistent candidates

Counterexamples

Current guess (a,b)

—

Press Step or Play to run CEGIS.

How it works

Counterexample-Guided Inductive Synthesis (CEGIS) alternates two roles until they agree:

loop:
  candidate ← Synthesizer.propose(E)   // any program
                                        // consistent with examples E
  x* ← Verifier.check(candidate, spec) // ∃x: candidate(x) ≠ spec(x) ?
  if x* is none:  return candidate     // proved equivalent
  else:           E ← E ∪ {x*}         // add counterexample, retry

Here the program space is every affine function f(x) = a·x + b with integer a, b on a lattice of radius R. The hidden spec is one such function the synthesizer cannot see directly. The Synthesizer enumerates the lattice in a fixed order and proposes the first candidate whose outputs match all counterexamples collected so far — that plane of spheres is the whole candidate space. The Verifier scans x = −D…D and returns the first input where the candidate disagrees with the hidden spec. Points that no longer match a counterexample fade out; the search space provably shrinks every round, exactly as it does for SMT-backed synthesizers over richer program grammars (loop bodies, sorting routines, SQL queries).

New Hidden Program — picks a fresh random (a*, b*) and restarts the loop with zero counterexamples.
Step / Play — advances the CEGIS loop one round at a time, or auto-plays it.
Domain radius D — how many integer inputs the verifier is allowed to probe.
Lattice radius R — how large the (a, b) candidate program space is; a bigger space takes more counterexamples to pin down.

Termination is guaranteed here because the lattice is finite and every counterexample removes at least the current candidate — the same finite-progress argument used to prove real CEGIS loops (over SAT/SMT-encoded program spaces) always halt.

Eliminated candidate Still consistent Proposed this round Verified = hidden program

⚠ Couldn't load the 3D engineThree.js failed to load from the CDN. Check your connection and reload.