A wide range of verification methods have been proposed to verify the safety
properties of deep neural networks ensuring that the networks function
correctly in critical applications. However, many well-known verification tools
still struggle with complicated network architectures and large network sizes.
In this work, we propose a network reduction technique as a pre-processing
method prior to verification. The proposed method reduces neural networks via
eliminating stable ReLU neurons, and transforming them into a sequential neural
network consisting of ReLU and Affine layers which can be handled by the most
verification tools. We instantiate the reduction technique on the
state-of-the-art complete and incomplete verification tools, including
alpha-beta-crown, VeriNet and PRIMA. Our experiments on a large set of
benchmarks indicate that the proposed technique can significantly reduce neural
networks and speed up existing verification tools. Furthermore, the experiment
results also show that network reduction can improve the availability of
existing verification tools on many networks by reducing them into sequential
neural networks.

通过消除稳定的 ReLU 神经元并将其转化为由 ReLU 和仿射层组成的顺序神经网络，我们提出了一种网络削减技术作为预处理方法以便于验证，实验证明这种技术能够显著减小神经网络规模并加快验证过程。

通过网络简化加快神经网络验证

Expediting Neural Network Verification via Network Reduction

We improve the effectiveness of propagation- and linear-optimization-based
neural network verification algorithms with a new tightened convex relaxation
for ReLU neurons. Unlike previous single-neuron relaxations which focus only on
the univariate input space of the ReLU, our method considers the multivariate
input space of the affine pre-activation function preceding the ReLU. Using
results from submodularity and convex geometry, we derive an explicit
description of the tightest possible convex relaxation when this multivariate
input is over a box domain. We show that our convex relaxation is significantly
stronger than the commonly used univariate-input relaxation which has been
proposed as a natural convex relaxation barrier for verification. While our
description of the relaxation may require an exponential number of
inequalities, we show that they can be separated in linear time and hence can
be efficiently incorporated into optimization algorithms on an as-needed basis.
Based on this novel relaxation, we design two polynomial-time algorithms for
neural network verification: a linear-programming-based algorithm that
leverages the full power of our relaxation, and a fast propagation algorithm
that generalizes existing approaches. In both cases, we show that for a modest
increase in computational effort, our strengthened relaxation enables us to
verify a significantly larger number of instances compared to similar
algorithms.

我们通过一种新的被紧化的凸松弛优化算法来提高神经网络验证的效率，并针对 ReLU 神经元提出了一种新的凸松弛方案，使得我们在设计两种多项式时间算法，包括利用全面的松弛力量的基于线性规划的算法和快速传播算法时能够比类似算法更好地验证神经网络