Synthesis from Examples: Interaction Models and Algorithms
Examples are often a natural way to specify various computational
artifacts such as programs, queries, and sequences. Synthesizing such artifacts
from example based specifications has various applications in the
domains of end-user programming and intelligent tutoring systems.
Synthesis from examples involves addressing two key technical
challenges: (i) design of a user
interaction model to deal with the inherent ambiguity in the example
based specification. (ii) design of an efficient search algorithm - these
algorithms have been based on paradigms from various communities
including use of SAT/SMT solvers (formal methods community), version
space algebras (machine learning community), and A*-style
goal-directed heuristics (AI community).
This paper describes some effective user interaction models
and algorithmic methodologies
for synthesis from examples
while discussing synthesizers for a variety of artifacts ranging from
tricky bitvector algorithms, spreadsheet macros for automating
repetitive data manipulation tasks, ruler/compass based geometry
constructions, algebraic identities, and predictive intellisense for
repetitive drawings and mathematical terms.