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验证器，它通过预测候选覆盖的区块大小分布（无需实际构建）来实现不同候选覆盖间的智能选择。该预测基于一个提供该分布均值与方差闭式表达的理论定理。CoVerD在验证过程中动态构建选定的覆盖验证设计，同时保持最低内存消耗并支持并行化分析。实验结果表明，相较于现有方法，CoVerD平均将验证时间缩短至多5.1倍，并能扩展到更大的$L_0$ $\epsilon$球。