Synthesis from Examples

Examples are often a natural way to specify computational structures such as programs, queries, and sequences. Synthesizing such structures from example based specification has applications in automating end-user programming and in building intelligent tutoring systems. Synthesis from examples involves addressing two key technical challenges: (i) design of an efficient search algorithm — these algorithms have been based on various paradigms including version-space algebras, SAT/SMT solvers, numerical methods, and even exhaustive search, (ii) design of a user interaction model to deal with the inherent ambiguity in the example based specification. This paper illustrates various algorithmic techniques and user interaction models by describing inductive synthesizers for varied applications including synthesis of tricky bitvector algorithms, spreadsheet macros for automating repetitive data manipulation tasks, ruler/compass based geometry constructions, new algebra problems, sequences for mathematical intellisense, and grading of programming problems.