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.

翻译：遮挡是一种普遍且易于实现的针对深度神经网络的语义扰动。通过遮挡输入图像的某些区域，可能误导深度神经网络导致错误分类，进而引发严重后果。因此，部署在安全关键系统中的深度神经网络在投入使用前必须验证其对遮挡的鲁棒性。然而，现有大多数深度神经网络鲁棒性验证方法主要针对非语义扰动，并不适用于遮挡场景。本文首次提出基于可满足性模理论的高效形式化验证方法，用于验证深度神经网络的遮挡鲁棒性。我们形式化定义了遮挡鲁棒性验证问题，并证明其为NP完全问题。随后设计了一种将遮挡编码为神经网络组成部分的新颖方法，并提出两种加速技术，使得扩展后的神经网络可通过现有基于SMT的神经网络验证工具高效验证。我们实现了原型系统OccRob，并在包含多种遮挡变体的基准数据集上进行了全面评估。实验结果表明，该方法在验证深度神经网络对各类遮挡的鲁棒性方面具有有效性和高效性，且能在网络不鲁棒时自动生成反例。