Interval Weight-Based Abstraction for Neural Network Verification

In recent years, neural networks (NNs) have gained much maturity and efficiency, and their applications have spread to various domains, including some modules of safety-critical systems. On the other hand, recent studies have demonstrated that NNs are vulnerable to adversarial attacks, thus a neural network model must be verified and certified before its deployment. Despite the number of existing formal verification methods of neural networks, verifying a large network remains a major challenge for these methods. This is mostly due to the scalability limitations of these approaches and the non-linearity introduced by the activation functions in the NNs. To help tackle this issue, we propose a novel abstraction method that allows the reduction of the NN size while preserving its behavioural features. The main idea of the approach is to reduce the size of the original neural network by merging neurons belonging to the same layer, and defining the new weights as intervals and sums of absolute values of those of the merged neurons. The approach allows for producing an abstract (i.e., reduced) model that is smaller and simpler to verify, while guaranteeing that this abstract model is an over-approximation of the original one. Our early experiments show that the approach enhances the scalability when performing verification operations, such as output range computation, on the abstract model.