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.

CoVerD 是一种通过预测其块大小分布选择不同候选覆盖的 $L_0$ 鲁棒性验证器，能够减少验证时间并适用于更大的 $L_0$ε- 球。

通过覆盖验证设计增强少像素的鲁棒性验证

Boosting Few-Pixel Robustness Verification via Covering Verification  Designs

Formal verification of neural networks is essential before their deployment
in safety-critical settings. However, existing methods for formally verifying
neural networks are not yet scalable enough to handle practical problems that
involve a large number of neurons. In this work, we propose a novel approach to
address this challenge: A conservative neural network reduction approach that
ensures that the verification of the reduced network implies the verification
of the original network. Our approach constructs the reduction on-the-fly,
while simultaneously verifying the original network and its specifications. The
reduction merges all neurons of a nonlinear layer with similar outputs and is
applicable to neural networks with any type of activation function such as
ReLU, sigmoid, and tanh. Our evaluation shows that our approach can reduce a
network to less than 5% of the number of neurons and thus to a similar degree
the verification time is reduced.

本文提出了一种保守的神经网络缩减方法，该方法能够在验证减小的网络的同时，确保验证原始网络，可以适用于任何类型的激活函数，使得网络能够被缩小到不到原来的 5% 的大小，从而显著减少了验证时间。

基于规格的神经网络简化用于可扩展形式验证

Specification-Driven Neural Network Reduction for Scalable Formal  Verification

Formal verification of neural networks is essential for their deployment in
safety-critical areas. Many available formal verification methods have been
shown to be instances of a unified Branch and Bound (BaB) formulation. We
propose a novel framework for designing an effective branching strategy for
BaB. Specifically, we learn a graph neural network (GNN) to imitate the strong
branching heuristic behaviour. Our framework differs from previous methods for
learning to branch in two main aspects. Firstly, our framework directly treats
the neural network we want to verify as a graph input for the GNN. Secondly, we
develop an intuitive forward and backward embedding update schedule.
Empirically, our framework achieves roughly $50\%$ reduction in both the number
of branches and the time required for verification on various convolutional
networks when compared to the best available hand-designed branching strategy.
In addition, we show that our GNN model enjoys both horizontal and vertical
transferability. Horizontally, the model trained on easy properties performs
well on properties of increased difficulty levels. Vertically, the model
trained on small neural networks achieves similar performance on large neural
networks.

通过训练图神经网络来设计一个有效的分支策略，能够在形式化验证神经网络的过程中减少验证时间并获得更好的验证结果。