Abstract Occlusion is a prevalent and easily realizable semantic perturbation to deep neural networks (DNNs). It can fool a DNN into misclassifying an input image by occluding some segments, possibly resulting in severe errors. Therefore, DNNs planted in safety-critical systems should be verified to be robust against occlusions prior to deployment. However, most existing robustness verification approaches for DNNs are focused on non-semantic perturbations and are not suited to the occlusion case. In this paper, we propose the first efficient, SMT-based approach for formally verifying the occlusion robustness of DNNs. We formulate the occlusion robustness verification problem and prove it is NP-complete. Then, we devise a novel approach for encoding occlusions as a part of neural networks and introduce two acceleration techniques so that the extended neural networks can be efficiently verified using off-the-shelf, SMT-based neural network verification tools. We implement our approach in a prototype called OccRob and extensively evaluate its performance on benchmark datasets with various occlusion variants. The experimental results demonstrate our approach’s effectiveness and efficiency in verifying DNNs’ robustness against various occlusions, and its ability to generate counterexamples when these DNNs are not robust.

Formal robustness verification of deep neural networks (DNNs) is a promising approach for achieving a provable reliability guarantee to AI-enabled software systems. Limited scalability is one of the main obstacles to the verification problem. In this paper, we propose eager falsification to accelerate the robustness verification of DNNs. It divides the verification problem into a set of independent subproblems and solves them in descending order of their falsification probabilities. Once a subproblem is falsified, the verification terminates with a conclusion that the network is not robust. We introduce a notion of label affinity to measure the falsification probability and present an approach to computing the probability based on symbolic interval propagation. Our approach is orthogonal to existing verification techniques. We integrate it into four state-of-the-art verification tools, i.e., MIPVerify, Neurify, DeepZ, and DeepPoly, and conduct extensive experiments on 8 benchmark datasets. The experimental results show that our approach can significantly improve these tools by up to 200x speedup when the perturbation distance is in a reasonable range.