论文标题

语法过滤的语法引导合成

Grammar Filtering For Syntax-Guided Synthesis

论文作者

Morton, Kairo, Hallahan, William, Shum, Elven, Piskac, Ruzica, Santolucito, Mark

论文摘要

逐示例编程(PBE)是一种合成范式,允许用户通过简单地提供输入输出示例来生成功能。尽管有希望的互动范式,但对于实时互动而言,合成仍然太慢了,并且采用了更广泛的采用。现有的PBE合成方法使用了自动推理工具,例如SMT求解器,以及应用机器学习技术的工作。自动推理方法的核心依赖于编程语言的高度领域特定知识。另一方面,机器学习方法利用了一个事实,即使用程序代码时,可以生成任意大型培训数据集。在这项工作中,我们提出了一个系统,用于与自动推理技术同时使用机器学习来求解语法引导的合成(SYGUS)样式PBE问题。通过使用神经网络预处理Sygus PBE问题,我们可以使用数据驱动的方法来减少搜索空间的大小,然后允许基于自动推理的求解器更快地分析解决方案。我们的系统能够在现有的Sygus PBE合成工具上运行,从而降低了2019年Sygus竞赛竞争对手PBE Strings Track的赢家,以优于所有竞争工具。

Programming-by-example (PBE) is a synthesis paradigm that allows users to generate functions by simply providing input-output examples. While a promising interaction paradigm, synthesis is still too slow for realtime interaction and more widespread adoption. Existing approaches to PBE synthesis have used automated reasoning tools, such as SMT solvers, as well as works applying machine learning techniques. At its core, the automated reasoning approach relies on highly domain specific knowledge of programming languages. On the other hand, the machine learning approaches utilize the fact that when working with program code, it is possible to generate arbitrarily large training datasets. In this work, we propose a system for using machine learning in tandem with automated reasoning techniques to solve Syntax Guided Synthesis (SyGuS) style PBE problems. By preprocessing SyGuS PBE problems with a neural network, we can use a data driven approach to reduce the size of the search space, then allow automated reasoning-based solvers to more quickly find a solution analytically. Our system is able to run atop existing SyGuS PBE synthesis tools, decreasing the runtime of the winner of the 2019 SyGuS Competition for the PBE Strings track by 47.65% to outperform all of the competing tools.

扫码加入交流群

加入微信交流群

微信交流群二维码

扫码加入学术交流群,获取更多资源