Synthesis from Examples: Interaction Models and Algorithms

Abstract

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.