  In this paper, we introduce NNSynth, a new framework that uses machine
learning techniques to guide the design of abstraction-based controllers with
correctness guarantees. NNSynth utilizes neural networks (NNs) to guide the
search over the space of controllers. The trained neural networks are
"projected" and used for constructing a "local" abstraction of the system. An
abstraction-based controller is then synthesized from such "local"
abstractions. If a controller that satisfies the specifications is not found,
then the best found controller is "lifted" to a neural network for additional
training. Our experiments show that this neural network-guided synthesis leads
to more than $50\times$ or even $100\times$ speedup in high dimensional systems
compared to the state-of-the-art.
