A theory of formal synthesis via inductive learning
A theory of formal synthesis via inductive learning
复制标题
DOI：
10.1007/s00236-017-0294-5
复制
发表时间：
2017-11-01
期刊：
影响因子：
0.6
通讯作者：
Seshia, Sanjit A.
中科院分区：
文献类型：
--
作者：
Jha, Susmit;Seshia, Sanjit A.
形式综合是生成满足高级形式规格说明的程序的过程。近年来，有效的形式化综合方法已经提出了基于使用归纳学习。我们把这类从例子中学习程序的方法称为形式归纳综合。在本文中，我们提出了一个理论框架的形式归纳综合。我们讨论了形式归纳合成与传统机器学习的不同之处。然后，我们描述了甲骨文引导的归纳合成（OGIS），一个框架，捕获一个家庭的合成器，通过迭代查询一个甲骨文。OGIS的一个实例是反例引导归纳合成（CEGIS）。我们提出了一个理论表征CEGIS学习任何程序，计算递归语言。特别是，我们分析了CEGIS变体的相对功率，其中由Oracle生成的反例的类型各不相同。我们还考虑了有界与无界内存的学习算法的影响。在候选程序的宇宙是有限的特殊情况下，我们将收敛速度与机器学习理论中研究的教学维度的概念联系起来。总之，本文的结果采取了第一步的理论基础，为新兴领域的正式归纳综合。
Formal synthesis is the process of generating a program satisfying a high-level formal specification. In recent times, effective formal synthesis methods have been proposed based on the use of inductive learning. We refer to this class of methods that learn programs from examples as formal inductive synthesis. In this paper, we present a theoretical framework for formal inductive synthesis. We discuss how formal inductive synthesis differs from traditional machine learning. We then describe oracle-guided inductive synthesis (OGIS), a framework that captures a family of synthesizers that operate by iteratively querying an oracle. An instance of OGIS that has had much practical impact is counterexample-guided inductive synthesis (CEGIS). We present a theoretical characterization of CEGIS for learning any program that computes a recursive language. In particular, we analyze the relative power of CEGIS variants where the types of counterexamples generated by the oracle varies. We also consider the impact of bounded versus unbounded memory available to the learning algorithm. In the special case where the universe of candidate programs is finite, we relate the speed of convergence to the notion of teaching dimension studied in machine learning theory. Altogether, the results of the paper take a first step towards a theoretical foundation for the emerging field of formal inductive synthesis.