Neural Network Verification Accelerated by a Novel Abstract Framework

Due to the gradual increase in the application of neural networks in various aspects, ensuring that they do not make errors in critical areas to maintain stability has become a hotspot. The research challenge lies in their black box nature. To address this issue, researchers have proposed various methods for neural network verification. However, the scalability of these methods is limited, making it difficult to apply them to large-scale networks. To address this limitation, this paper proposes an abstract framework. Abstraction, although a classic tool for verification, is rarely used to verify neural networks. However, abstraction aids in addressing the difficulty of extending existing algorithms to the latest network architectures. This framework is applicable to fully connected feedforward neural networks, built upon clustering neurons that exhibit similar output behaviors under specific inputs. For ReLU neural networks, the error bounds generated by the abstraction are also analyzed. Moreover, the framework is shown to minimize the network size while preserving accuracy to the greatest extent possible. We also show how to apply the validation results on the abstract network to the original network. Finally, this framework is independent of existing verification techniques, allowing integration with various verification methods.