Deductive Techniques for Synthesis from Inductive Specifications

We propose two key ideas for designing efficient algorithms for inductive synthesis problems. (i) restrict the search space to an appropriate domain-specific language that provides the right set of abstractions that enable readability and balanced expressivity (i.e., expressive enough to capture a wide range of tasks, but restricted enough to allow efficient search). (ii) design a domain-specific search algorithm using the divide-and-conquer paradigm that reduces the problem of synthesizing an expression of a given kind that satisfies a given specification into sub-problems that refer to sub-expressions or sub-specifications.

The problem reduction logics can be refactored into domain-independent parts and operator-specific parts. We leverage this observation to develop a general framework that allows construction of efficient inductive synthesizers from a mere description of the domain-specific language and inverse properties of operators that are used in the underlying DSL.