Few-pixel attacks mislead a classifier by modifying a few pixels of an image. Their perturbation space is an ℓ₀-ball, which is not convex, unlike ℓₚ-balls for p ≥ 1. However, existing local robustness verifiers typically scale by relying on linear bound propagation, which captures convex perturbation spaces. We show that the convex hull of an ℓ₀-ball is the intersection of its bounding box and an asymmetrically scaled ℓ₁-like polytope. The volumes of the convex hull and this polytope are nearly equal as the input dimension increases. We then show a linear bound propagation that precisely computes bounds over the convex hull and is significantly tighter than bound propagations over the bounding box or our ℓ₁-like polytope. This bound propagation scales the state-of-the-art ℓ₀ verifier on its most challenging robustness benchmarks by 1.24x-7.07x, with a geometric mean of 3.16.

Abstract Proving local robustness is crucial to increase the reliability of neural networks. While many verifiers prove robustness in $$L_\infty \ \epsilon $$ L∞ϵ -balls, very little work deals with robustness verification in $$L_0\ \epsilon $$ 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_\infty $$ L∞ neighborhoods, which if proven robust imply that the $$L_0\ \epsilon $$ L0ϵ -ball is robust. However, the number of neighborhoods to verify remains very high, leading to a high analysis time. We proposecovering verification designs, a combinatorial design that tailors effective but analysis-incompatible coverings to $$L_0$$ 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 , an $$L_0$$ L0 robustness verifier that selects between different candidate coveringswithout 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. constructs the chosen covering verification designon-the-fly, while keeping the memory consumption minimal and enabling to parallelize the analysis. The experimental results show that reduces the verification time on average by up to 5.1x compared to prior work and that it scales to larger $$L_0\ \epsilon $$ L0ϵ -balls.

While successful, neural networks have been shown to be vulnerable to adversarial example attacks. In L 0 adversarial attacks, also known as few-pixel attacks, the attacker picks t pixels from the image and arbitrarily perturbs them. To understand the robustness level of a network to these attacks, it is required to check the robustness of the network to perturbations of every set of t pixels. Since the number of sets is exponentially large, existing robustness verifiers, which can reason about a single set of pixels at a time, are impractical for L 0 robustness verification. We introduce Calzone, an L 0 robustness verifier for neural networks. To the best of our knowledge, Calzone is the first to provide a sound and complete analysis for L 0 adversarial attacks. Calzone builds on the following observation: if a classifier is robust to any perturbation of a set of k pixels, for k > t , then it is robust to any perturbation of its subsets of size t . Thus, to reduce the verification time, Calzone predicts the largest k that can be proven robust, via dynamic programming and sampling. It then relies on covering designs to compute a covering of the image with sets of size k . For each set in the covering, Calzone submits its corresponding box neighborhood to an existing L ∞ robustness verifier. If a set’s neighborhood is not robust, Calzone repeats this process and covers this set with sets of size k ′< k . We evaluate Calzone on several datasets and networks, for t ≤ 5. Typically, Calzone verifies L 0 robustness within few minutes. On our most challenging instances (e.g., t =5), Calzone completes within few hours. We compare to a MILP baseline and show that it does not scale already for t =3.