Toward Neural-Network-Guided Program Synthesis and Verification

TL;DR

This paper introduces a neural network-guided framework for program and invariant synthesis, enabling extraction of logical formulas from neural networks and demonstrating applications in program verification and development.

Contribution

It presents a novel method to synthesize logical formulas from neural network weights and applies this to program verification and oracle-based programming.

Findings

Successfully synthesized formulas from examples and constraints.

Applied the method to qualifier discovery in CHC solving.

Enabled neural-network-guided program development framework.

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. 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.