Program synthesis using conflict-driven learning
Program synthesis using conflict-driven learning
复制标题
DOI：
10.1145/3296979.3192382
复制
发表时间：
2017-11
影响因子：
--
通讯作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
中科院分区：
文献类型：
--
作者：
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
我们提出了一种新的冲突驱动的程序合成技术，能够从过去的错误中学习。给定一个违反所需规范的虚假程序，我们的合成算法识别冲突的根本原因，并学习新的引理，可以防止类似的错误在未来。具体来说，我们引入了等价模冲突的概念，并展示了如何使用这个想法来学习有用的引理，使合成器修剪大部分的搜索空间。我们已经实现了一个通用的CDCL风格的程序合成器称为新的，并评估它在两个不同的应用领域，即数据争吵在R和函数式编程列表。我们的实验证明了冲突驱动学习的实质性好处，并表明Neo优于两个最先进的合成工具Morpheus和Deepcoder，它们分别针对这些领域。
We propose a new conflict-driven program synthesis technique that is capable of learning from past mistakes. Given a spurious program that violates the desired specification, our synthesis algorithm identifies the root cause of the conflict and learns new lemmas that can prevent similar mistakes in the future. Specifically, we introduce the notion of equivalence modulo conflict and show how this idea can be used to learn useful lemmas that allow the synthesizer to prune large parts of the search space. We have implemented a general-purpose CDCL-style program synthesizer called Neo and evaluate it in two different application domains, namely data wrangling in R and functional programming over lists. Our experiments demonstrate the substantial benefits of conflict-driven learning and show that Neo outperforms two state-of-the-art synthesis tools, Morpheus and Deepcoder, that target these respective domains.