A Sound Abstraction Method Towards Efficient Neural Networks Verification

With the increasing application of neural networks (NN) in safety-critical systems, the (formal) verification of NN is becoming more than essential. Although several NN verification techniques have been developed in recent years, these techniques are often limited to small networks and do not scale well to larger NN. The primarily reason for this limitation is the complexity and non-linearity of neural network models. Abstraction and model reduction approaches, that aim to reduce the size of the neural networks and over-approximate their outcomes, have been seen as a promising research direction to help existing verification methods to handle larger models. In this paper, we introduce a model reduction method for neural networks with non-negative activation functions (e.g., ReLU and Sigmoid). The method relies on merging neurons while ensuring that the obtained model (i.e., the abstract model) over-approximates the original one. Concretely, it consists in merging a set of neurons that have positive outgoing weights and substituting it with a single abstract neuron, while ensuring that if a given property holds on the abstract network, it necessarily holds on the original one. In order to assess the efficiency of the approach, we perform an experimental comparison with two existing model reduction methods on the ACAS Xu benchmark. The obtained results show that our approach outperforms both methods in terms of precision and execution time.