# CounterExample Guided Neural Synthesis

arXiv: https://arxiv.org/abs/2001.09245 · HTML: https://mlsanity.com/paper/2001.09245/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 25 Jan 2020.

## Built on by (most cited first, 4 of 4)

- [Formally Explaining Neural Networks within Reactive Systems](https://mlsanity.com/paper/2308.00143/) (2023)
- [Verifying Generalization in Deep Learning](https://mlsanity.com/paper/2302.05745/) (2023)
- [Can Language Models Falsify? Evaluating Algorithmic Reasoning with Counterexample Creation](https://mlsanity.com/paper/2502.19414/) (2025)
- [DelBugV: Delta-Debugging Neural Network Verifiers](https://mlsanity.com/paper/2305.18558/) (2023)

## Abstract (arXiv)

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.