  While abstraction is a classic tool of verification to scale it up, it is not
used very often for verifying neural networks. However, it can help with the
still open task of scaling existing algorithms to state-of-the-art network
architectures. We introduce an abstraction framework applicable to
fully-connected feed-forward neural networks based on clustering of neurons
that behave similarly on some inputs. For the particular case of ReLU, we
additionally provide error bounds incurred by the abstraction. We show how the
abstraction reduces the size of the network, while preserving its accuracy, and
how verification results on the abstract network can be transferred back to the
original network.
