Abstract Learning Frameworks for Synthesis

TL;DR

This paper introduces abstract learning frameworks (ALFs) for synthesis, unifying various algorithms under a common iterative learning paradigm and proposing new convergence techniques.

Contribution

It formalizes a general abstract framework for synthesis algorithms, embedding existing methods and proposing novel convergence strategies.

Findings

Unified synthesis algorithms within a common framework

Generalized synthesis problems using learning principles

Proposed three convergence techniques, including a novel one

Abstract

We develop abstract learning frameworks (ALFs) for synthesis that embody the principles of CEGIS (counter-example based inductive synthesis) strategies that have become widely applicable in recent years. Our framework defines a general abstract framework of iterative learning, based on a hypothesis space that captures the synthesized objects, a sample space that forms the space on which induction is performed, and a concept space that abstractly defines the semantics of the learning process. We show that a variety of synthesis algorithms in current literature can be embedded in this general framework. While studying these embeddings, we also generalize some of the synthesis problems these instances are of, resulting in new ways of looking at synthesis problems using learning. We also investigate convergence issues for the general framework, and exhibit three recipes for convergence in finite time. The first two recipes generalize current techniques for convergence used by existing synthesis engines. The third technique is a more involved technique of which we know of no existing instantiation, and we instantiate it to concrete synthesis problems.