Synthesis with Abstract Examples

The Problem

Programming by example is a powerful idea: show a synthesizer a few input-output pairs, and it finds a program that matches. But concrete examples have a fundamental limitation — they are finite. You can show the synthesizer that 2 → 4, 3 → 6, and 5 → 10, and it might learn to double its input. But you cannot express "for all positive integers, the output should be positive" using finitely many concrete examples.

This is more than a theoretical nuisance. In practice, concrete examples lead to ambiguity: many programs satisfy a small set of examples, and the synthesizer has no way to distinguish between correct generalizations and coincidental fits. You need a way to express what you really mean — properties that should hold across entire classes of inputs.

The Key Idea

The key insight is to borrow from abstract interpretation, a framework for reasoning about programs over abstract domains. Instead of giving the synthesizer concrete values, you give it abstract examples: pairs of abstract values that describe properties of the input and the expected properties of the output.

For instance, rather than saying 2 → 4, you say {positive} → {positive, even}. This single abstract example captures infinitely many concrete behaviors: for any positive input, the output must be both positive and even.

The synthesizer then searches for a program whose abstract semantics satisfies all the given abstract examples. It uses the abstract transformer of each candidate program — the same machinery used in static analysis — to check whether the abstract output is consistent with the specification.

Interactive Demo: Abstract vs. Concrete

How It Works

Abstract Interpretation Domains

Abstract interpretation provides a principled way to approximate the behavior of a program over sets of values. An abstract domain defines which properties we track — for example, the Sign domain tracks whether a value is positive, negative, or zero; the Parity domain tracks whether a value is even or odd.

Each operation in the programming language has an abstract transformer that describes how it maps abstract values. For instance, in the Sign domain, multiplying two positive values yields a positive value: positive * positive = positive. These transformers let us check whether a candidate program satisfies an abstract example without running it on every possible input.

Abstract Example Checking

Given a candidate program and an abstract example, the synthesizer evaluates the program's abstract transformer on the abstract input. If the abstract output is subsumed by (i.e., at least as precise as) the required abstract output, the candidate passes. Otherwise, it is rejected.

This is a sound check: if the abstract transformer says the output is positive, then the program truly produces a positive output for all inputs in the abstract input set. The synthesizer can therefore prune entire families of incorrect programs in a single check, rather than testing them one example at a time.

Results

The paper demonstrates that abstract examples lead to faster and more precise synthesis. Key findings include:

• Fewer examples needed. Because each abstract example encodes infinitely many concrete behaviors, the synthesizer reaches a correct program with fewer user-provided specifications.
• Stronger guarantees. The synthesized programs satisfy properties over entire abstract domains, not just the specific inputs given. This closes the gap between "works on my examples" and "works correctly."
• Efficient pruning. Abstract checking eliminates large portions of the search space early, speeding up the synthesis process compared to approaches that rely solely on concrete tests.