Proving local robustness is crucial to increase the reliability of neural networks. While many verifiers prove robustness in $L_\infty$ $\epsilon$-balls, very little work deals with robustness verification in $L_0$ $\epsilon$-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$ neighborhoods, which if proven robust imply that the $L_0$ $\epsilon$-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 $L_0$ 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 $L_0$ 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 $L_0$ $\epsilon$-balls.

翻译：证明局部鲁棒性对于提升神经网络的可靠性至关重要。尽管许多验证器在$L_\infty$ $\epsilon$-球内证明鲁棒性，但针对$L_0$ $\epsilon$-球（捕获对少像素攻击的鲁棒性）的验证研究极少。此类验证引入了组合挑战，因为待扰动像素空间是离散且呈指数规模的。先前工作依赖覆盖设计来识别用于定义$L_\infty$邻域的子集，若这些邻域被证明具有鲁棒性，则可推导出$L_0$ $\epsilon$-球具有鲁棒性。然而，需要验证的邻域数量仍然极高，导致分析时间过长。我们提出覆盖验证设计——一种将高效但与分析不兼容的覆盖方案适配于$L_0$鲁棒性验证的组合设计。其挑战在于计算覆盖验证设计会产生较高的时间和内存开销，而在需要多个候选覆盖以确定如何降低总体分析时间的场景中，该问题尤为突出。我们提出CoVerD，一种通过预测候选覆盖的区块大小分布（而非直接构建覆盖）来从中进行选择的$L_0$鲁棒性验证器。该预测基于一个定理，该定理为此分布提供了均值与方差的闭式表达式。CoVerD在验证过程中动态构建选定的覆盖验证设计，同时保持最低内存消耗并支持并行化分析。实验结果表明，与现有工作相比，CoVerD平均将验证时间降低至多5.1倍，并能扩展到更大的$L_0$ $\epsilon$-球。