Verifying and Improving Neural Networks Using Testing-Based Formal Verification

Neural networks have been widely used in safety-critical systems, but those safety-critical systems containing neural networks still have security risks due to the existence of adversarial examples. The security of neural networks can be ensured to some extent by verifying them. However, since the verification of neural networks is a NP-hard problem, it is still impossible to apply the verification algorithm to large-scale neural networks. For this reason, we propose TBFV-INN, a new framework for verification and improving neural networks. First, we propose a testing-based neural network pruning algorithm, which obtains the execution path of each test case in the neural network by executing them. Secondly, test-based neural network pruning divides the original neural network into several sub neural networks. Finally, for divided sub neural network, a verification algorithm is used to verify and construct the data set to retrain the neural network, thus ensuring that each sub neural network is reliable in a particular input-output interval. We show a case study to demonstrate the feasibility of the framework.