1: \begin{abstract}

2: Formal synthesis is the process of generating a program satisfying a high-level formal specification.

3: In recent times, effective formal synthesis methods have been proposed based on 

4: the use of inductive learning. We refer to this class of methods that learn programs from examples 

5: as formal inductive synthesis.

6: In this paper, we present a theoretical framework for formal inductive synthesis. We discuss how

7: formal inductive synthesis differs from traditional machine learning.

8: We then describe oracle-guided inductive synthesis (OGIS), a framework that captures a

9: family of synthesizers that operate by iteratively querying an oracle.

10: An instance of OGIS that has had much practical impact is counterexample-guided inductive synthesis (CEGIS).

11: We present a theoretical characterization of CEGIS for learning any program that computes a recursive language.

12: In particular, we analyze the relative power of CEGIS variants where the types of counterexamples generated

13: by the oracle varies. We also consider the impact of bounded versus unbounded memory available to the learning algorithm.

14: In the special case where the universe of candidate programs is finite, we relate the speed of convergence

15: to the notion of teaching dimension studied in machine learning theory.

16: Altogether, the results of the paper take a first step towards a theoretical foundation for

17: the emerging field of formal inductive synthesis.

18: %This paper is a first step towards identification of a common paradigm of formal synthesis.

19: %This provides a framework to study theoretical decidability and complexity issues of formal synthesis.

20: %The theoretical results will enable

21: % principled design of practical formal synthesis techniques for different applications that combine

22: %inductive learning and deductive verification.

23: \end{abstract}

24: