Improved Incremental Verification for Neural Networks

The formal verification of deep neural networks (DNNs) guarantees their robustness. However, DNNs deployed in real-world applications frequently undergo adjustments due to, for instance, quantization and model repair, necessitating the repetition of computationally expensive formal verification. To efficiently verify the robustness of such adjusted DNNs, incremental techniques for DNN verification are proposed recently. These techniques use the information obtained from the verification of original networks to expedite the verification of their adjusted counterparts. In particular, the state-of-the-art incremental technique based on the Branch-and-Bound method exploits branching information from verifying original DNNs, to efficiently generate subproblems for verifying the adjusted counterparts. This paper goes beyond this idea. When verifying adjusted DNNs, we prioritize checking subproblems that falsify the robustness of the original ones, with the expectation of prompt falsification. Furthermore, we collect information from the Bound processes while verifying original DNNs, then utilize it for more efficient Bound processes when verifying the adjusted networks. We propose a DNN incremental verification framework I-IVAN and realize it for evaluation. It is compared against IVAN, the state-of-the-art DNN verification tool with incremental techniques, on networks trained by datasets MNIST and CIFAR-10. The experimental results show that I-IVAN is much more efficient than IVAN within 7.71 times faster than IVAN at most.