# OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks

arXiv: https://arxiv.org/abs/2301.11912 · HTML: https://mlsanity.com/paper/2301.11912/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 27 of its 45 references that are in the map.
- First posted on arXiv 27 Jan 2023.

## Builds on (most cited first, 27 of 27)

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Continuous control with deep reinforcement learning](https://mlsanity.com/paper/1509.02971/) (2015)
- [Spatial Transformer Networks](https://mlsanity.com/paper/1506.02025/) (2015)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [One pixel attack for fooling deep neural networks](https://mlsanity.com/paper/1710.08864/) (2017)
- [Adversarial Patch](https://mlsanity.com/paper/1712.09665/) (2017)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [DeepXplore: Automated Whitebox Testing of Deep Learning Systems](https://mlsanity.com/paper/1705.06640/) (2017)
- [Certified Defenses against Adversarial Examples](https://mlsanity.com/paper/1801.09344/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [DeepTest: Automated Testing of Deep-Neural-Network-driven Autonomous Cars](https://mlsanity.com/paper/1708.08559/) (2017)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Certified Defenses for Adversarial Patches](https://mlsanity.com/paper/2003.06693/) (2020)
- [An Abstraction-Based Framework for Neural Network Verification](https://mlsanity.com/paper/1910.14574/) (2019)
- [Occlusion Robust Face Recognition Based on Mask Learning with PairwiseDifferential Siamese Network](https://mlsanity.com/paper/1908.06290/) (2019)
- [Certified Defense to Image Transformations via Randomized Smoothing](https://mlsanity.com/paper/2002.12463/) (2020)
- [CNN-Cert: An Efficient Framework for Certifying Robustness of Convolutional Neural Networks](https://mlsanity.com/paper/1811.12395/) (2018)
- [An SMT-Based Approach for Verifying Binarized Neural Networks](https://mlsanity.com/paper/2011.02948/) (2020)
- [Fastened CROWN: Tightened Neural Network Robustness Certificates](https://mlsanity.com/paper/1912.00574/) (2019)
- [Compositional Convolutional Neural Networks: A Robust and Interpretable Model for Object Recognition under Occlusion](https://mlsanity.com/paper/2006.15538/) (2020)
- [Repairing Deep Neural Networks: Fix Patterns and Challenges](https://mlsanity.com/paper/2005.00972/) (2020)
- [Analyzing Deep Neural Networks with Symbolic Propagation: Towards Higher Precision and Faster Verification](https://mlsanity.com/paper/1902.09866/) (2019)
- [Reachability Is NP-Complete Even for the Simplest Neural Networks](https://mlsanity.com/paper/2108.13179/) (2021)
- [Robustness of Object Recognition under Extreme Occlusion in Humans and Computational Models](https://mlsanity.com/paper/1905.04598/) (2019)
- [Towards Evaluating and Training Verifiably Robust Neural Networks](https://mlsanity.com/paper/2104.00447/) (2021)

## Built on by (most cited first, 5 of 5)

- [Robustness of SAM: Segment Anything Under Corruptions and Beyond](https://mlsanity.com/paper/2306.07713/) (2023)
- [Analyzing Effects of Mixed Sample Data Augmentation on Model Interpretability](https://mlsanity.com/paper/2303.14608/) (2023)
- [Benchmarking Local Robustness of High-Accuracy Binary Neural Networks for Enhanced Traffic Sign Recognition](https://mlsanity.com/paper/2310.03033/) (2023)
- [Robustness Verifcation in Neural Networks](https://mlsanity.com/paper/2403.13441/) (2024)
- [Some Complexity Results for Robustness Verification for Binarized Neural Networks](https://mlsanity.com/paper/2606.18918/) (2026)

## Abstract (arXiv)

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.