基于神经网络的程序综合和验证

MMMar, 2021

Toward Neural-Network-Guided Program Synthesis and Verification

Naoki Kobayashi, Taro Sekiyama, Issei Sato, Hiroshi Unno

TL;DR提出一种神经网络引导的程序和不变量综合框架，其利用设计和训练神经网络提取出训练神经网络权重和偏置值上的整数逻辑公式，并用于正 / 反例和蕴含约束的公式合成，具有很好的实验结果，并在 ICE-learning-based CHC 求解、程序验证和归纳不变量合成等方面有重要应用。

Abstract

We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. 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. Base

neural network-guided synthesis program and invariant synthesis ice-learning-based chc solving program verification inductive invariant synthesis

发现论文，激发创造

基于神经引导的演绎式搜索：以示例为基础的实时程序综合

本文介绍了神经引导演绎搜索 (NGDS) 技术，应用于编写用户意图程序的问题，结合了符号逻辑技术和统计模型，通过演绎搜索框架来学习神经网络组件，以找到最适合提供的规范的程序，并在真实客户场景中验证其实用性。

Apr, 2018

一种可验证强化学习的归纳综合框架

本文研究如何使用形式化验证技术对增强学习 - enabled 机器学习系统进行验证，以保证其行为安全，并提出了一种基于黑盒方法的综合确定性程序的方法来实现系统验证。

Jul, 2019

神经引导的约束逻辑编程用于程序合成

使用神经模型指导 MiniKanren 解决编程 - by-example 问题。我们实现了基于 RNN 和 GNN 的神经模型，其输入为 MiniKanren 的内部表示。我们的方法能够更快地合成程序，并能够泛化到更大的问题。

Sep, 2018

使用查询的神经程序合成

本篇研究提出了一个基于查询的框架用于自动生成并交互式提供信息丰富的输入输出样例，其可用于编程合成中的无监督学习以解决缺少先验知识的问题。

May, 2022

神经符号程序合成

本文提出了一种 Neuro-Symbolic Program Synthesis 技术，通过计算机程序自动构建特定领域的语言。我们通过使用两种新颖的神经模型，交叉相关的 I/O 网络和递归反向递归神经网络，证明了该方法的有效性。

Nov, 2016

分层神经程序合成

本文提出了一种可扩展的程序合成框架，通过层级组合程序实现程序合成，该框架可以从输入 / 输出对中合成比之前更长、更复杂的程序，并通过任务嵌入空间和程序解码器将任务嵌入解码为程序。

Mar, 2023

学习推理程序草图

本文介绍一种用于程序自动合成的方法，通过结合模式识别和显式推理来解决这些复杂的编程问题，同时使用新颖的中间表示和训练算法，使程序合成系统能够自学，从而在简单的英文描述编程问题数据集上取得了最先进的性能表现。

Feb, 2019

我说，你验证：朝向值得信赖的神经程序合成

本文基于大型语言模型，提出了一种改进程序综合器可靠性和总体准确性的方法，通过语言模型自然语言描述求解程序问题，并且学习分析程序和断言的一致性，以判断哪个程序最有可能是正确的，从而通过提供可信的解决方案来改善可靠性

Sep, 2022

HOUDINI: 基于程序综合的终身学习

本文提出了一种神经符号框架，用于混合感知和程序推理算法任务的终身学习，介绍了一种结合了梯度下降和程序组合搜索的程序合成方法，并在三个基准测试中评估了其性能。

Mar, 2018

基于强化学习的语法引导综合

在这项研究中，我们将通用 SyGuS 问题作为树搜索框架，并提出了一种基于蒙特卡洛树搜索 (MCTS) 的增强学习引导合成算法。我们的算法结合了学习到的策略和值函数，以及平衡探索和利用的树上置信上界。我们还介绍了一种基于现有一阶可满足性问题的反合一方法自动生成 SyGuS 的训练数据。通过这些成果，我们的工具在训练和测试集中相比基准枚举算法提高了 26 个百分点，超过了 1 CVC5 等最先进工具的表现，同时我们还公开了我们的数据集以便于进一步应用机器学习方法解决 SyGuS 问题。

Jul, 2023