# Boosting Few-Pixel Robustness Verification via Covering Verification Designs

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- Builds on 21 of its 40 references that are in the map.
- First posted on arXiv 17 May 2024.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Towards Evaluating the Robustness of Neural Networks](https://mlsanity.com/paper/1608.04644/) (2016)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [The Limitations of Deep Learning in Adversarial Settings](https://mlsanity.com/paper/1511.07528/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Provably Robust Deep Learning via Adversarially Trained Smoothed Classifiers](https://mlsanity.com/paper/1906.04584/) (2019)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Certified Adversarial Robustness with Additive Noise](https://mlsanity.com/paper/1809.03113/) (2018)
- [Randomized Smoothing of All Shapes and Sizes](https://mlsanity.com/paper/2002.08118/) (2020)
- [Globally-Robust Neural Networks](https://mlsanity.com/paper/2102.08452/) (2021)
- [Sparse-RS: a versatile framework for query-efficient sparse black-box adversarial attacks](https://mlsanity.com/paper/2006.12834/) (2020)
- [Training Certifiably Robust Neural Networks with Efficient Local Lipschitz Bounds](https://mlsanity.com/paper/2111.01395/) (2021)
- [Mind the box: l1-APGD for sparse adversarial attacks on image classifiers](https://mlsanity.com/paper/2103.01208/) (2021)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [Adversarial Perturbations Against Deep Neural Networks for Malware Classification](https://mlsanity.com/paper/1606.04435/) (2016)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [Parallelization Techniques for Verifying Neural Networks](https://mlsanity.com/paper/2004.08440/) (2020)
- [Boosting Robustness Verification of Semantic Feature Neighborhoods](https://mlsanity.com/paper/2209.05446/) (2022)

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

- [Tight Robustness Certification Through the Convex Hull of ℓ0 Attacks](https://mlsanity.com/paper/2511.10576/) (2025)
- [Uncovering the Limits of Proof Sharing for Neural Networks](https://mlsanity.com/paper/2608.19351/) (2026)

## Abstract (arXiv)

Proving local robustness is crucial to increase the reliability of neural networks. While many verifiers prove robustness in L_∞ ε-balls, very little work deals with robustness verification in L0 ε-balls, capturing robustness to few pixel attacks. This verification introduces a combinatorial challenge, because the space of pixels to perturb is discrete and of exponential size. A previous work relies on covering designs to identify sets for defining L_∞ neighborhoods, which if proven robust imply that the L0 ε-ball is robust. However, the number of neighborhoods to verify remains very high, leading to a high analysis time. We propose covering verification designs, a combinatorial design that tailors effective but analysis-incompatible coverings to L0 robustness verification. The challenge is that computing a covering verification design introduces a high time and memory overhead, which is intensified in our setting, where multiple candidate coverings are required to identify how to reduce the overall analysis time. We introduce CoVerD, an L0 robustness verifier that selects between different candidate coverings without constructing them, but by predicting their block size distribution. This prediction relies on a theorem providing closed-form expressions for the mean and variance of this distribution. CoVerD constructs the chosen covering verification design on-the-fly, while keeping the memory consumption minimal and enabling to parallelize the analysis. The experimental results show that CoVerD reduces the verification time on average by up to 5.1x compared to prior work and that it scales to larger L0 ε-balls.