Synthesis from Examples
Abstract
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.