  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.
