CounterExample Guided Neural Synthesis
This addresses scalability and correctness issues in program synthesis for developers and researchers, offering a hybrid approach that is incremental over prior neural or formal methods.
The paper tackles the problem of program synthesis by combining neural networks with formal reasoning to generate programs from logical specifications, resulting in nearly double the number of benchmarks solved compared to existing methods.
Program synthesis is the generation of a program from a specification. Correct synthesis is difficult, and methods that provide formal guarantees suffer from scalability issues. On the other hand, neural networks are able to generate programs from examples quickly but are unable to guarantee that the program they output actually meets the logical specification. In this work we combine neural networks with formal reasoning: using the latter to convert a logical specification into a sequence of examples that guides the neural network towards a correct solution, and to guarantee that any solution returned satisfies the formal specification. We apply our technique to synthesising loop invariants and compare the performance to existing solvers that use SMT and existing techniques that use neural networks. Our results show that the formal reasoning based guidance improves the performance of the neural network substantially, nearly doubling the number of benchmarks it can solve.