CEGIS 2D: 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*, spec(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 (a, b) lattice in a fixed row-major order and proposes the first candidate whose graph matches every counterexample collected so far — that grid on the left is the whole candidate space. The Verifier (right panel) scans x = −D…D and returns the first input where the candidate's line disagrees with the hidden spec's line; that (x, spec(x)) pair becomes the new counterexample, plotted in red. Points that no longer match a counterexample fade to gray on the grid; 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.
Drag / scroll the left grid — pan and zoom the candidate lattice; the function graph on the right always auto-fits.

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.

drag to pan · scroll to zoom (left grid)

Eliminated candidate Still consistent Proposed this round Verified = hidden program Counterexample