Toward Neural-Network-Guided Program Synthesis and Verification
Toward Neural-Network-Guided Program Synthesis and Verification
复制标题
DOI：
10.1007/978-3-030-88806-0_12
复制
发表时间：
2021-03
期刊：
影响因子：
--
通讯作者：
N. Kobayashi;Taro Sekiyama;Issei Sato;Hiroshi Unno
中科院分区：
文献类型：
--
作者：
N. Kobayashi;Taro Sekiyama;Issei Sato;Hiroshi Unno
我们提出了一种新颖的程序和不变综合框架，称为神经网络引导综合（NeuGuS）。我们首先表明，通过适当地设计和训练神经网络，我们可以从经过训练的神经网络的权重和偏差中提取整数上的逻辑公式。基于这个想法，我们实现了一种从正/反例和蕴涵约束合成公式的工具，并获得了有希望的实验结果。我们还讨论了我们的合成方法的两个应用。一是在基于 ICE 学习的 CHC 求解框架中使用我们的限定符发现工具，该工具又可应用于程序验证和归纳不变综合。另一个应用是一种称为基于预言机编程的新程序开发框架，它是 Solar-Lezama 通过草图进行程序合成的神经网络引导变体。
We propose a novel framework of program and invariant synthesis called neural network-guided synthesis (NeuGuS). We first show that, by suitably designing and training neural networks, we can extract logical formulas over integers from the weights and biases of the trained neural networks. Based on the idea, we have implemented a tool to synthesize formulas from positive/negative examples and implication constraints, and obtained promising experimental results. We also discuss two applications of our synthesis method. One is the use of our tool for qualifier discovery in the framework of ICE-learning-based CHC solving, which can in turn be applied to program verification and inductive invariant synthesis. Another application is to a new program development framework called oracle-based programming, which is a neural-network-guided variation of Solar-Lezama’s program synthesis by sketching.