Abstract
Formal synthesis is the process of learning a compositional concept satisfying a high-level formal specification. Programs, controllers, strategies, and logical specifications are examples of such compositional concepts. Over the last decade, we have developed several techniques for formal synthesis. In this talk, we will discuss a unifying view that describes these formal synthesis techniques as an interaction protocol between an oracle and a learner – both of which are co-designed for a target concept. We present a theoretical characterization of different formal synthesis techniques by considering oracles and learners with different properties. We also describe practical applications of this framework for scalable and interpretable learning.