Expediting Neural Network Verification via Network Reduction
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.
Yuyi Zhong, Ruiwei Wang, Siau-Cheng Khoo
# Expediting Neural Network Verification via Network Reduction

###### Abstract

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.

 Neural Network Verification, Network Reduction, Pre-processing

## I Introduction

Deep neural networks have been widely applied in real-world applications. At the same time, it is indispensable to guarantee the safety properties of neural networks in those critical scenarios. As neural networks are trained to be larger and deeper, researchers have deployed various techniques to speed up the verification process. For example, to over-approximate the whole network behavior [1, 2, 3, 4]; to deploy GPU implementation [5, 6, 7]; or to merge neurons in the same layer in an over-approximate manner so as to reduce the number of neurons [8, 9].

This work aims to further accelerate the verification process by "pre-processing" the tested neural network with ReLU activation function and constructing a _reduced_ network with _fewer_ number of neurons and connections. We propose the _network reduction_ technique, which returns a reduced network (named as _REDNet_) that captures the _exact_ behavior of the original network rather than over-approximating the original network. Therefore verification over the reduced network equals the original verification problem yet requires less execution cost.

The REDNet could be instantiated on different verification techniques and is beneficial for complex verification processes such as branch-and-bound based (bab) or abstract refinement based methods. For example, branch-and-bound based methods [6, 7, 10, 11] generate a set of sub-problems to verify the original problem. Once deployed with REDNet before the branch-and-bound phase, all the sub-problems are built on the reduced network, thus achieving overall speed gain. For abstract refinement based methods, like [12, 13, 4], they collect and encode the network constraints and refine individual neuron bounds via LP (linear program) or MILP (mixed-integer linear program) solving. This refinement process could be applied to a large set of neurons, and the number of constraints in the network encoding can be significantly reduced with the deployment of REDNet.

We have implemented our proposed network reduction technique in a prototypical system named REDNet (the reduced network), which is available at [https://github.com/REDNet-verifier/IDNN](https://github.com/REDNet-verifier/IDNN). The experiments show that the ReLU neurons in the reduced network could be up to 95 times smaller than those in the original network in the best case and 10.6 times smaller on average. We instantiated REDNet on the state-of-the-art complete verifier \(\alpha,\beta\)-CROWN [14], VeriNet [15] and incomplete verifier PRIMA [12] and assessed the effectiveness of REDNet over a wide range of benchmarks. The results show that, with the deployment of REDNet, \(\alpha,\beta\)-CROWN could verify more properties given the same timeout and gain average \(1.5\times\) speedup. Also, VeriNet with REDNet verifies 25.9% more properties than the original and can be \(1.6\times\) faster. REDNet could also assist PRIMA to gain \(1.99\times\) speedup and verifies 60.6% more images on average. Lastly, REDNet is constructed in a simple network architecture and making it amenable for existing tools to handle network architectures that they could not support previously.

We summarize the contributions of our work as follows:

* We define stable ReLU neurons and deploy the state-of-the-art bounding method to detect such stable neurons.
* We propose a _network reduction_ process to _remove_ stable neurons and generate REDNet that contains a smaller number of neurons and connections, thereby boosting the efficiency of existing verification methods.
* We prove that the generated REDNet preserves the input-output equivalence of the original network.
* We instantiate the REDNet on several state-of-the-art
verification methods. The experiment results indicate that the same verification processes execute faster on the REDNet than on the original network; it can also respond accurately to tougher queries the verification of which were timeout when running on the original network.
* REDNet is constructed with a simple network architecture, it can assist various tools in handling more networks that they have failed to be supported previously.
* Lastly, we export REDNet as a fully-connected network in ONNX, which is an open format that is widely accepted by the most verification tools.

## II Preliminaries

A _feedforward neural network_ is a function \(\mathcal{F}\) defined as a directed acyclic diagram \((\mathcal{V},\mathcal{E})\) where every node \(L_{i}\) in \(\mathcal{V}\) represents a layer of \(|L_{i}|\) neurons and each arc \((L_{i},L_{j})\) in \(\mathcal{E}\) denotes that the outputs of the neurons in \(L_{i}\) are inputs of the neurons in \(L_{j}\). For each layer \(L_{i}\in\mathcal{V}\), \(in(L_{i})=\{L_{j}|(L_{j},L_{i})\in\mathcal{E}\}\) is the _preceding layers_ of \(L_{i}\) and \(out(L_{i})=\{L_{j}|(L_{i},L_{j})\in\mathcal{E}\}\) denotes the _succeeding layers_ of \(L_{i}\). If the set \(in(L_{i})\) of preceding layers is non-empty, then the layer \(L_{i}\) represents a computation operator, e.g. the ReLU and GEMM operators; otherwise \(L_{i}\) is an input layer of the neural network. In addition, \(L_{i}\) is an _output layer_ of the neural network if \(out(L_{i})\) is empty.

In this paper, we consider the ReLU-based neural network with one input layer and one output layer. Note that multiple input layers (and output layers) can be concatenated as one input layer (and one output layer). Then a neural network is considered as a _sequential neural network_ if \(|in(L_{i})|=1\) and \(|out(L_{i})|=1\) for all layers \(L_{i}\) in the neural network except the input and output layers.

We use a vector \(\vec{a}\) to denote the input of a neural network \(\mathcal{F}\), and the _input space_\(I\) of \(\mathcal{F}\) includes all possible inputs of \(\mathcal{F}\). For any input \(\vec{a}\in I\), \(L_{i}(\vec{a})\) is a vector denoting the outputs of neurons in a layer \(L_{i}\) given this input \(\vec{a}\). The output \(\mathcal{F}(\vec{a})\) of the neural network is the output of its output layer.

The _neural network verification problem_ is to verify that for all possible inputs \(\vec{a}\) from a given input space \(I\), the outputs \(\mathcal{F}(\vec{a})\) of a neural network \(\mathcal{F}\) must satisfy a specific condition. For example, the robustness verification problem is to verify that for all inputs within a specified input space, the neural network's output must satisfy that the value of the neuron corresponding to the ground truth label is greater than the values of the other neurons in the output layer.

## III Overview

In this section, we present a simple network \(\mathcal{F}\) and illustrate how to construct the reduced network via the deletion of stable neurons, where stable neurons refer to those ReLU neurons whose inputs are completely non-negative or non-positive.

The example is a fully-connected network with ReLU activation function \(y=\text{max}(0,x)\) as shown in Figure 1, where the connections are recorded in the linear constraints near each affine neuron. We set the input space \(I\) to be \([-1,1]\times[-1,1]\), and apply one of the state-of-the-art bound propagators CROWN [16] to propagate the input intervals to other neurons of the network. The deployment of CROWN returns us the concrete bounds for intermediate neurons, which are displayed next to the corresponding neurons in Figure 1.

From this initial computation, we observe that four ReLU neurons are _stable_: \(x_{8}\) is stably deactivated as its input \(x_{3}\leq 0\) yields \(x_{8}=0\); \(x_{9},x_{10},x_{11}\) are stably activated as their inputs are always greater or equal to zero, yielding \(x_{9}=x_{4},x_{10}=x_{5},x_{11}=x_{6}\). Given the observation, we could _remove_ those stable ReLU neurons together with their input neurons: we could directly eliminate neurons \(x_{3},x_{8}\); and delete \(x_{4},x_{5},x_{6},x_{9},x_{10},x_{11}\) while _connecting_\(y_{1},y_{2}\) directly to the preceding neurons of \(x_{4},x_{5},x_{6}\), which are \(x_{1},x_{2}\).

After removal, the connections are updated as in Figure 2. The new affine constraint of \(y_{1}\) is computed as follows:

\[y_{1} = x_{8}-x_{9}+x_{10}+x_{11}-x_{12}\] \[= 0-x_{4}+x_{5}+x_{6}-x_{12}\] \[= x_{1}-x_{2}+1-x_{12}\]

Similarly, the computation of \(y_{2}\) is updated as follows:

Figure 1: The example network with initial concrete bounds

Figure 2: The network connections after neuron removal
\[y_{2} = x_{8}+x_{9}+x_{10}+x_{11}+x_{12}\] \[= 0+x_{4}+x_{5}+x_{6}+x_{12}\] \[= 3x_{1}+x_{2}+7+x_{12}\]

The above computation only involves equality replacement; therefore, the two networks in Figure 2 and Figure 1 functions _the same_ given the specified input space \(I\). However, the network architecture has been modified, and the output neurons are now defined over its preceding layer together with the input layer. To preserve the network architecture without introducing new connections between layers, we _merge_ the stably activated neurons into _a smaller set_ of neurons instead of directly deleting them.

The final reduced network is shown below in Figure 3, where we transform the connection between \(y_{1},y_{2}\) and \(x_{1},x_{2}\) in Figure 2 into two merged neurons \(m_{1}=x_{1}-x_{2}+1;m_{2}=3x_{1}+x2+7\). Since \(m_{2}\) is stably activated given the input space, we have \(m_{4}=m_{2}\), thus \(y_{2}=m_{4}+x_{12}\) which equals to the definition of \(y_{2}\) in Figure 2. To further enforce \(m_{1}\) to remain stably activated, we increase the bias of \(m_{1}\) to be 2, which leads to \(m_{3}=m_{1}\), thus \(y_{2}=m_{3}-x_{12}-1\). Therefore, the final reduced network in Figure 3 remains to be a fully-connected network, but the stably deactivated neuron \(x_{3}\) has been removed, and the original set of stably activated neurons \(x_{4},x_{5},x_{6}\) are merged into a smaller set of stably activated neurons \(m_{1},m_{2}\). Note that the connection between \(y_{1},y_{2}\) and \(m_{1},m_{2}\) are actually identity matrix:

\[\begin{bmatrix}y_{1}\\ y_{2}\end{bmatrix}=\begin{bmatrix}1&0\\ 0&1\end{bmatrix}\cdot\begin{bmatrix}m_{1}\\ m_{2}\end{bmatrix}+\begin{bmatrix}-1\\ 1\end{bmatrix}\cdot x_{12}+\begin{bmatrix}-1\\ 0\end{bmatrix} \tag{3}\]

Therefore, the number of merged neurons depends on the number of neurons in the succeeding layer (e.g., the output layer in this example). Generally speaking, the number of output neurons is significantly smaller than the number of intermediate neurons. Therefore we conduct the reduction in a backward manner from the last hidden layer to the first hidden layer, and the experiments in section VI show that a major proportion of the neurons could be deleted, which boosts verification efficiency and therefore improve precision within a given execution timeout.

## IV Stable ReLU Neurons Reduction

### _Stable ReLU neurons_

Given a ReLU layer \(X\) in a neural network and an input \(\vec{a}\), the layer \(X\) has exactly one preceding layer \(Y\) (i.e. \(in(X)=\{Y\}\)) and the _pre-activation_ of the \(k^{th}\) ReLU neuron \(x\) in \(X\) is the output \(y(\vec{a})\) of the \(k^{th}\) neuron \(y\) in \(Y\). For simplicity, we use \(\hat{x}(\vec{a})=y(\vec{a})\) to denote the pre-activation of \(x\).

**Definition 1**.: A ReLU neuron \(x\) in a neural network is _deactivated_ w.r.t. (with respect to) an input space \(I\) if \(\hat{x}(\vec{a})\leq 0\) for all inputs \(\vec{a}\in I\), and \(x\) is _activated_ w.r.t. the input space \(I\) if \(\hat{x}(\vec{a})\geq 0\) for all \(\vec{a}\in I\). Then \(x\) is _stable_ w.r.t. \(I\) if \(x\) is deactivated or activated w.r.t. \(I\).

It is NP-complete to check whether the output of a neural network is greater than or equal to 0 [17]. In addition, we can add an additional ReLU layer behind the output layer of the neural network where the output of the original neural network becomes the pre-activation of ReLU neurons, therefore, it is straightforward that checking the stability of ReLU neurons w.r.t. an input space is NP-hard.

**Theorem 1**.: It is NP-hard to check whether a ReLU neuron is stable w.r.t. an input space \(I\).

Many methods have been proposed to compute the lower and upper bounds of the pre-activation of ReLU neurons. Usually, these methods use different constraints to tighten the pre-activation bounds, such as linear relaxations, split constraints, global cuts and output constraints. For detecting the stability of ReLU neurons w.r.t. an input space, we only consider the methods which employ the linear relaxations of ReLU neurons alone, as the other constraints may filter out inputs from the input space, e.g. a ReLU neuron is compulsory to be stably deactivated despite the input space if the propagator uses a split constraint to enforce that the pre-activation input value is always non-positive. We enumerate various bound propagation methods in Table I. The methods using other constraints are not suitable for detecting the stability of intermediate neurons, such as \(\beta\)-Crown employs split constraints.

In our experiments, we use the GPU-based bound propagation method CROWN to detect stable ReLU neurons, which leads to a reasonably significant reduction with a small time cost, as displayed in Table III.

### _ReLU layer reduction_

As illustrated in the example given in section III, after computation of concrete neuron bounds, we detect and handle those stable ReLU neurons in the following ways:

\begin{table}
\begin{tabular}{|c|c|} \hline Methods for Stability Detection & Other Methods \\ \hline \hline Interval [18], DeepZ/Symbolic [2, 19, 20] & \(\beta\)-Crown [21] \\ CROWN [16], FCrown [22], \(\alpha\)-Crown [23] & GCP-Crown [24] \\ Deeply [25], KPoly [26], PRIMA [12] & ARENA [13] \\ RefineZon [27],OptC2V [28] & DeepSRGR [4] \\ SDP-Relaxation [29, 30, 31] & \\ LP/Lagrangian Dual [32, 33, 34] & \\ \hline \end{tabular}
\end{table}
Table I: Bound propagation methods

Figure 3: The final network after reduction (REDNet), where the dashed connection means the coefficient equals to 0
* For a stably deactivated ReLU neuron whose input value is always non-positive, it is always evaluated as \(0\) and thereby will be directly deleted from the network as it has no effect on the actual computation;
* For a stably activated ReLU neurons (the input values of which are always non-negative) in the same layer, we reconstruct this set of stably activated neurons into _a smaller_ set of stably activated neurons as we reduce \(x_{4},x_{5},x_{6}\) into \(m_{1},m_{2}\) in section III.

**Reconstruction of Stably Activated Neurons.** Figure 2 illustrates that the deletion of stably activated neurons requires creating new connections between the preceding and succeeding neurons of the deleted neurons. We follow the convention that every intermediate ReLU layer only directly connects to one preceding layer and one succeeding layer, which conducts linear computation (and we defer the details of how to simplify a complicated network with multiple preceding/succeeding connections into such simpler architecture in section V).

An example of a ReLU layer pending reduction is shown in Figure 4, where \(M_{1}\) indicates the linear connection between layer \(V\) and \(X\); \(M_{2}\) indicates the connection between layer \(Y\) and \(Z\). Biases are recorded in \(B_{1}\) and \(B_{2}\) respectively. Suppose that the uppermost \(k\) neurons in layer \(Y\) are stably activated, and we delete them together with their inputs in layer \(X\) from Figure 4. After deletion, we need to generate a new connection between layers \(Z\) and \(V\). As stably activated ReLU neurons behave as identity functions, the new connection matrix between layer \(Z\) and \(V\) can be computed from existing connection matrices \(M_{1}\) (size \(m\times q\)) and \(M_{2}\) (matrix with size \(n\times m\)). Assume that \(M[0:k,:]\) indicates that we slice the matrix to contain only the first \(k\) rows; and \(M[:0:k]\) means we only take the leftmost \(k\) columns of the matrix, we define a matrix \(M^{\prime}_{VZ}\) with size \(n\times q\) that is computed as:

\[M^{\prime}_{VZ}=M_{2}[:,0:k]\cdot M_{1}[0:k,:] \tag{4}\]

We consider this new connection \(M^{\prime}_{VZ}\) with size \(n\times q\) as:

\[M^{\prime}_{VZ}=M_{I}\cdot M^{\prime}_{VX}, \tag{5}\]

where \(M^{\prime}_{VX}\) _equals to \(M^{\prime}_{VZ}\)_ and functions as the affine connection between layers \(V\) and _newly constructed_ neurons in layer \(X\); \(M_{I}\) denotes an \(n\times n\) identity matrix and is the affine connection between layer \(Z\) and the _newly constructed_ neurons in layer \(Y\), as shown in Figure 5. Here, the additional weight matrix between layers \(V\) and \(Z\) is actually computed as \(M^{\prime}_{VZ}=M_{I}\cdot ReLU()\cdot M^{\prime}_{VX}\). For Equation 5 to hold, we need to make sure that the ReLU function between \(M\) and \(M^{\prime}\) becomes an identity, which means \(M\) must be non-negative and \(M^{\prime}\) is stably activated. So we will compute the concrete bounds of \(M\) and add an additional bias \(B\) to enforce it as non-negative as we did for neuron \(m_{1}\) in section III. This additional bias will be canceled out at layer \(Z\) with \(-B\) offset.

Note that we conduct this reduction in a backward manner from the last hidden layer (whose succeeding layer is the output layer that usually consists of a very small number of neurons, e.g. 10) to the first hidden layer. Therefore, upon reduction of layers \(X\) and \(Y\), layer \(Z\) has already been reduced and contains a small number \(n\) of neurons. In the end, the \(k\) stably activated neurons will be reduced into \(n\) stably activated neurons and we obtain a smaller-sized affine layer with \(m-k+n\) neurons, where \(k\) is usually much bigger than \(n\). Therefore, we are able to observe a significant size reduction as shown in Table III.

**Lemma 1**.: The reduction process preserves the input-output equivalence of the original network. That is, for any input \(\vec{a}\in I\), \(\mathcal{F}(\vec{a})\equiv\mathcal{F}^{\prime}(\vec{a})\) where \(\mathcal{F}\) is the original network and \(\mathcal{F}^{\prime}\) is the reduced one.

Proof.: The reduction process operates on ReLU neurons that are stable w.r.t. the input space \(I\). Specifically, (i) Stably _deactivated_ ReLU neurons are always evaluated as \(0\) and can be deleted directly as they have no effect on the subsequent computation; (ii) Stably _activated_ ReLU neurons are reconstructed in a way that their functionality are preserved before (Figure 4) and after (Figure 5) reconstruction.

For any \(\vec{a}\in I\), \(V(\vec{a})\) is the output of Layer \(V\) and the output of Layer \(Z\) is computed as \(Z(\vec{a})=M_{2}\cdot ReLU(M_{1}\cdot V(\vec{a})+B_{1})+B_{2}\) in Figure 4. we decompose \(Z(\vec{a})-B_{2}\) as

\[M_{2}[:,0:k]\cdot ReLU(M_{1}[0:k,:]\cdot V(\vec{a})+B_{1}[0:k]) \tag{6}\] \[+M_{2}[:,k:m]\cdot ReLU(M_{1}[k:m,:]\cdot V(\vec{a})+B_{1}[k:m]) \tag{7}\]

Without loss of generality, we assume the uppermost \(k\) neurons in layer \(Y\) are stably activated. Formula 6 thus simplifies to \(M_{2}[:,0:k]\cdot M_{1}[0:k,:]\cdot V(\vec{a})+M_{2}[:,0:k]\cdot B_{1}[0:k]=M_ {I}\cdot M^{\prime}_{VX}\cdot V(\vec{a})+B^{\prime}\), where \(M^{\prime}_{VX}=M_{2}[:,0:k]\cdot M_{1}[0:k,:]\), \(B^{\prime}=M_{2}[:,0:k]\cdot B_{1}[0:k]\) and \(M_{I}\) is an identity matrix.

Figure 4: Layer \(X\) and \(Y\) with pending reduction, together with its preceding layer \(V\) and succeeding affine layer \(Z\).

Figure 5: The block after reduction of stably activated neurons. \(M_{1}[k:m,:]\) contains the last \(m-k\) rows of \(M_{1}\), while \(M_{2}[:,k:m]\) takes the rightmost \(m-k\) columns of \(M_{2}\). \(B^{\prime}\) is computed as \(M_{2}[:,0:k]\cdot B_{1}[0:k]\). The _newly constructed_ neurons are dashed and colored in blue.
Furthermore, we compute an additional bias \(B\) to ensure that \(M^{\prime}_{VX}\cdot V(\vec{a})+B\geq 0\) for all \(\vec{a}\in I\). Thus Formula 6 finally simplifies to:

\[M_{I}\cdot ReLU(M^{\prime}_{VX}\cdot V(\vec{a})+B)-B+B^{\prime} \tag{8}\]

Based on Formula 8, we obtain \(Z(\vec{a})=M_{I}\cdot ReLU(M^{\prime}_{VX}\cdot V(\vec{a})+B)+M_{2}[:,k:m]\cdot ReLU (M_{1}[k:m,:]\cdot V(\vec{a})+B_{1}[k:m])+B^{\prime}+B_{2}-B\), which equals to the computation conducted in Figure 5. Thus, the network preserves input-output equivalence after reduction. 

## V Neural Network Simplification

In section IV, we describe how reduction is conducted on a sequential neural network, where each intermediate layer only connects to one preceding Linear layer and one succeeding Linear layer. In this paper, a Linear layer refers to a layer whose output is computed via linear computation. Nonetheless, there exist many complicated network architectures (e.g., residual networks) that are not sequential. In order to handle a wider range of neural networks, we propose a neural network simplification process to transform complex network architectures into simplified sequential neural networks and then conduct reduction on the simplified network.

We now introduce how to transform a complex ReLU-based neural network into a sequential neural network consisting of Linear and ReLU layers so that stable ReLU neurons can be reduced. Note that we only consider the neural network layers that can be encoded as Linear and ReLU layers; further discussion about this can be found in section VII.

The network simplification process involves two main steps (shown in Figure 6): (i) Encode various layers as SumLinear blocks and ReLU layers (we defer the definition of SumLinear block to subsection V-A); (ii) Transform SumLinear blocks into Linear layers. Here, Linear layers refer to layers that conduct linear computation.

### _Encode various layers into SumLinear blocks_

A _SumLinear block_ is a combination of a set of Linear layers and a Sum layer such that the Linear layers are preceding layers of the Sum layer, where the output of the Sum layer is the element-wise sum of its inputs. The output of the SumLinear block is equal to the element-wise sum of the outputs of the Linear layers, and the preceding layers of the SumLinear block include the preceding layers of all the Linear layers. Any Linear layer can be encoded as a SumLinear block by adding a Sum layer behind the Linear layer. A main difference between them is that the SumLinear block can have more than 1 preceding layer.

Many neural network layers can be directly transformed into SumLinear blocks, such as Conv, GeMM, Add, Sub, Concat, Reshape, Split, Squeeze, Unsqueeze, \(\cdots\), Flatten, MatMul, and BatchNormalization layers used in ONNX models.1 Note that the Linear layer only has one preceding layer, while the Add and Concat layers can have more than one preceding layer; hence, they cannot be directly encoded as a Linear layer (this motivates the introduction of SumLinear blocks).

Footnote 1: In general, Maxpooling can be encoded as Conv and ReLU layers with existing tools such as DNNV [35]. Note that \(max(x,y)=ReLU(x-y)+y\).

Figure 7 shows a SumLinear block encoding a Concat layer with 2 precedessors \(X\) and \(Y\). The biases of the two Linear layers are zero and the concatenation of their weights is an identity matrix. Thus, each neuron of the layers \(X,Y\) is mapped to a neuron of the Sum layer. Assume \(|X|=|Y|=1\). Their weights are represented by matrices: \(\begin{bmatrix}1\\ 0\end{bmatrix}\) and \(\begin{bmatrix}0\\ 1\end{bmatrix}\) which can be concatenated into an identity matrix \(\begin{bmatrix}1&0\\ 0&1\end{bmatrix}\).

In the same spirit, the Add layer could also be encoded as a SumLinear block as shown in Figure 8. Assume that \(|X|\) and \(|Y|\) are each equal to 2, the weights of the two Linear layers are represented by identity matrices \(\begin{bmatrix}1&0\\ 0&1\end{bmatrix}\).

Figure 8: Encode an Add layer into a SumLinear block.

Figure 6: The procedure of neural network reduction. The encoding session is described in subsection V-A; the transformation is discussed in subsection V-B; and the reduction part is explained in section IV.

Figure 7: Encode a Concat layer into a SumLinear block.
### _Transform SumLinear blocks into Linear Layers_

In this subsection, we show how to encode SumLinear blocks as Linear layers. Firstly, we need to transform SumLinear blocks into normalized SumLinear blocks. To this end, a SumLinear block \(L\) is _normalized_ if it does not have any Linear layer of which the preceding layer is a SumLinear block (i.e. \(in(L)\) does not have SumLinear blocks), and each of the Linear layers in \(L\) has different preceding layers. For example, the SumLinear given in Figure 7 is normalized if its preceding layers \(X\) and \(Y\) are not SumLinear blocks.

**SumLinear Block Normalization.** If a SumLinear block \(L^{\prime}\) includes a Linear layer \(L^{\prime}_{j}\) with a weight \(M^{\prime}_{j}\) and a bias \(B^{\prime}_{j}\) such that the preceding layer of \(L^{\prime}_{j}\) is another SumLinear block \(L^{\prime\prime}\) including \(k\) Linear layers \(L^{\prime\prime}_{1},\cdots L^{\prime\prime}_{k}\) with weights \(M^{\prime\prime}_{1},\cdots,M^{\prime\prime}_{k}\) and biases \(B^{\prime\prime}_{1},\cdots,B^{\prime\prime}_{k}\), then we can normalize \(L^{\prime}\) by replacing \(L^{\prime}_{j}\) with \(k\) new Linear layers \(L_{1},\cdots L_{k}\) where for any \(1\leq i\leq k\), the layer \(L_{i}\) has the same preceding layer as that of \(L^{\prime\prime}_{i}\), and the weight and bias of \(L_{i}\) are computed as:

\[M_{i} =M^{\prime}_{j}\cdot M^{\prime\prime}_{i} \tag{9}\] \[B_{i} =\begin{cases}B^{\prime}_{j}+M^{\prime}_{j}\cdot B^{\prime\prime }_{i}&\text{if }i=1\\ M^{\prime}_{j}\cdot B^{\prime\prime}_{i}&\text{otherwise}\end{cases} \tag{10}\]

During the normalization, if the succeeding layers of the block \(L^{\prime\prime}\) become empty, then \(L^{\prime\prime}\) is directly removed.

In addition, if two Linear layers \(L_{a},L_{b}\) in a SumLinear block have the same preceding layer, then in normalization, we can replace them by one new Linear layer \(L_{c}\) such that \(L_{c}\) has the same preceding layer as them and the weight (and bias) of \(L_{c}\) is the sum of the weights (and biases) of \(L_{a},L_{b}\).

**Lemma 2**.: SumLinear block normalization does not change the functionality of a neural network.

Proof.: Let \(\vec{a}^{\prime\prime}_{i}\) be any input of a Linear layer \(L^{\prime\prime}_{i}\) in the block \(L^{\prime\prime}\) where \(L^{\prime\prime}\) is the preceding layer of \(L^{\prime}_{j}\). Thus, the input of \(L^{\prime}_{j}\) (called \(\vec{a}^{\prime}_{j}\)) equals to \(\sum_{i=1}^{k}(M^{\prime\prime}_{i}\cdot\vec{a}^{\prime\prime}_{i}+B^{\prime \prime}_{i})\). Then the output of \(L^{\prime}_{j}\) is \(B^{\prime}_{j}+\sum_{i=1}^{k}(M^{\prime}_{j}\cdot M^{\prime\prime}_{i}\cdot \vec{a}^{\prime\prime}_{i}+M^{\prime}_{j}\cdot B^{\prime\prime}_{i})\) which is equal to the sum of the outputs of the layers \(L_{1},\cdots L_{k}\). Therefore, replacing \(L^{\prime}_{j}\) with \(L_{1},\cdots L_{k}\) does not change the output of the SumLinear block \(L^{\prime}\).

If the succeeding layers of \(L^{\prime\prime}\) become empty, then removing \(L^{\prime\prime}\) does not affect the outputs of other layers and the network.

In addition, the sum of the outputs of the two linear layers \(L_{a},L_{b}\) in a SumLinear Block with the same preceding layer is equal to the output of the new layer \(L_{c}\), thus, the output of the block does not change after replacing \(L_{a},L_{b}\) with \(L_{c}\).

So SumLinear block normalization does not change the functionality of a neural network. 

We next show how to encode normalized SumLinear blocks as Linear layers.

**Linear Layer Construction**. First, we say that a ReLU layer \(L_{i}\) is _blocked_ by a SumLinear block \(L\) if \(L\) is the only succeeding layer of \(L_{i}\). Then, we use \(\mathcal{R}_{L}\) to denote the set of ReLU layers blocked by the SumLinear block \(L\). Let \(\mathcal{P}_{L}\) include other preceding layers of \(L\) which are not in \(\mathcal{R}_{L}\). If \(L\) is normalized, then \(L\) and the set of ReLU layers in \(\mathcal{R}_{L}\) can be replaced by a Linear layer \(L^{l}\), a ReLU layer \(L^{r}\) and a new SumLinear block \(L^{s}\) such that

* the weight \(M^{l}\) (the bias \(B^{l}\)) of the linear layer \(L^{l}\) is a concatenation (the sum) of the weights (the bias) of the Linear layers in \(L\) and the preceding layer of \(L^{l}\) is \(L^{r}\) and \(L^{l}\) has the same succeeding layers as \(L\);
* the SumLinear block \(L^{s}\) encodes a concatenation of layers in \(\mathcal{P}_{L}\) and the preceding layers of layers in \(\mathcal{R}_{L}\);
* \(L^{s}\) is the preceding layer of \(L^{r}\).

Additionally, in order to make sure that the outputs of the layers in \(\mathcal{P}_{L}\) can pass through the ReLU layer \(L^{r}\), the neurons in \(L^{r}\) which connect to the layers in \(P_{L}\) are enforced as activated neurons by adding an additional bias \(B\) to a Linear layer in \(L^{s}\) and minus \(M^{l}\cdot B\) from the bias of \(L^{l}\).

**Lemma 3**.: Linear layer construction does not change the functionality of a neural network.

Proof.: The pre-activation of \(L^{r}\) is the output of \(L^{s}\) that equals to \(B\) plus the concatenation of the outputs of layers in \(\mathcal{P}_{L}\) and the pre-activation of Layers in \(\mathcal{R}_{L}\). This ensures that the output of \(L^{r}\) equals to \(B\) plus the concatenation (call it \(\vec{a}\)) of the outputs of layers in \(\mathcal{P}_{L}\) and \(\mathcal{R}_{L}\). Next, the output of \(L^{l}\) equals to \(M^{l}\cdot(B+\vec{a})+B^{l}-M^{l}\cdot B=M^{l}\cdot\vec{a}+B^{l}\) which is equal to the output of original layer \(L\).

In addition, \(L\) is the only succeeding layer of layers in \(\mathcal{R}_{L}\), so replacing \(\mathcal{R}_{L}\), \(L\) with the layers \(L^{s}\), \(L^{r}\), \(L^{l}\) does not change the functionality of the neural network. 

**Network simplification.** We use algorithm 1 to transform ReLU-based neural networks \((\mathcal{V},\mathcal{E})\) into a sequential neural network consisting of Linear and ReLU layers. At line 1, the function \(Initialization(\mathcal{V},\mathcal{E})\) encodes all layers in \(\mathcal{V}\) as SumLinear blocks and ReLU layers. Between line 3 and line 8, the algorithm repeatedly selects the last SumLinear block \(L\) in \(\mathcal{V}\) and reconstructs \(L\) into Linear layers, where a SumLinear block is _the last_ block means there is not any path from it to another SumLinear block. \((\mathcal{V},\mathcal{E})\) only has 1 output layer, and the Linear and ReLU layers only have 1 preceding layer, thus, there is only one last SumLinear block.

```
Input: A neural network \((\mathcal{V},\mathcal{E})\) Output: A sequential neural network
1\(\mathcal{V},\mathcal{E}\gets Initialization(\mathcal{V},\mathcal{E})\);
2while\((\mathcal{V},\mathcal{E})\) has SumLinear blocksdo
3 Let \(L\) be the last SumLinear block in \((\mathcal{V},\mathcal{E})\);
4\(\mathcal{V},\mathcal{E},L\gets Normalization(\mathcal{V},\mathcal{E},L)\);
5if\(|in(L)|>1\)then
6\(\mathcal{V},\mathcal{E}\gets LinearLayerConstruction(\mathcal{V},\mathcal{E},L)\);
7
8else
9\(\mathcal{V},\mathcal{E}\gets Linearization(\mathcal{V},\mathcal{E},L)\);
10
11return\((\mathcal{V},\mathcal{E})\);
```

**Algorithm 1**Neural Network Simplification
At line 4, the function \(Normalization(\mathcal{V},\mathcal{E},L)\) is used to normalize the last SumLinear block \(L\). If the normalized \(L\) has more than one preceding layer (i.e. \(|in(L)|>1\)), then the function \(LinearLayer Construction(\mathcal{V},\mathcal{E},L)\) is used to replace \(L\) with the layers \(L^{l},L^{r},L^{s}\) introduced in the Linear layer construction (at line 6), otherwise the function \(Linearization(\mathcal{V},\mathcal{E},L)\) is used to directly replace \(L\) with the only Linear layer included in \(L\) (at line 8).

In the rest of this subsection, we show that line 6 in algorithm 1 can only be visited at most \(|\mathcal{V}|\) times, thus, the algorithm can terminate and generate an equivalent sequential neural network consisting of Linear and ReLU layers.

**Lemma 4**.: Assume \((\mathcal{V},\mathcal{E})\) is a neural network consisting of Linear, ReLU layers and SumLinear blocks and \(L\) is the last SumLinear block in \(\mathcal{V}\). If \(|in(L)|>1\) and \(in(L)\) does not have SumLinear blocks and Linear layers, then \(\mathcal{R}_{L}\) is not empty.

Proof.: \((\mathcal{V},\mathcal{E})\) only has one output layer and all layers behind \(L\) have at most one preceding layer, thus, a path from any layer before \(L\) to the output layer must pass \(L\).

Let \(L_{i}\) be the last ReLU layer in \(in(L)\). If \(L_{i}\) has a succeeding layer \(L_{j}\) such that \(L_{j}\neq L\), then \(L\) must be in all paths from \(L_{j}\) to the output layer, and there would be a ReLU layer in \(in(L)\) included by a path from \(L_{j}\) to \(L\), which meant that \(L_{i}\) was not the last layer in \(in(L)\), a contradiction. Hence, \(L_{i}\) is in \(\mathcal{R}_{L}\) and \(\mathcal{R}_{L}\neq\emptyset\). 

Based on lemma 4, if \(|in(L)|>1\), then \(|\mathcal{R}_{L}|\geq 1\), thus, the number of ReLU layers before the last SumLinear block in \(\mathcal{V}\) is decreased after replacing \(L\) and the layers in \(\mathcal{R}_{L}\) with the layers \(L^{l},L^{r},L^{s}\) introduced in the Linear layer construction where \(L^{s}\) becomes the last SumLinear block in \(\mathcal{V}\). So we can get that algorithm 1 can terminate and generate a neural network consisting of Linear and ReLU layers.

**Theorem 2**.: Algorithm 1 can terminate and generate a neural network consisting of Linear and ReLU layers.

Proof.: From lemma 4, we know that line 6 in algorithm 1 reduces the number of ReLU neurons before the last SumLinear block in \(\mathcal{V}\), therefore, it can only be visited at most \(|\mathcal{V}|\) times. Note that SumLinear block normalization (at line 4) does not affect ReLU layers and the layers behind \(L\).

Then line 8 can directly replace all SumLinear blocks having one preceding layer in \(\mathcal{V}\) with Linear layers. Therefore, algorithm 1 can terminate and return a neural network consisting of Linear and ReLU layers. 

**Theorem 3**.: Our constructed REDNet is input-output equivalent to the original network given the input space \(I\).

Proof.: (Sketch.) Our reduction technique contains two steps: (i) network simplification presented in section V; (ii) stable ReLU neuron reduction described in section IV. Each step is designed deliberately to preserve input-output equivalence.

_Simplification equivalence._ Function \(Initialization(\mathcal{V},\mathcal{E})\) at line 1 in algorithm 1 encodes ONNX layers into a uniform network representation; such encoding preserves input-output equivalence. Then lemma 2 and lemma 3 show that line 4 and line 6 do not change network functionality. In addition, line 8, replacing a SumLinear Block with the only Linear layer in the block, also does not change network output. Therefore, algorithm 1 can construct a sequential neural network that has the same functionality as the original neural network.

_Reduction equivalence._ The proof is given in lemma 1. 

### _Illustrative example of network simplification_

In this subsection, we use a simple network block to illustrate how to perform algorithm 1 on a non-sequential structure (Figure 9(a)) to get a sequential neural network consisting of Linear and ReLU layers (Figure 9(b)). In Figure 9, each rectangular node (including \(n_{1},n_{2},n_{3},n_{4}\)) represents a set of neurons whose values are derived from the preceding connected node(s) and the connections between them. Note that red-colored rectangular nodes are ReLU nodes that represent the output neurons of the ReLU layer; blue nodes are convolutional nodes; the black node is an Add layer. The connections between nodes are represented with directed edges, and the connected functions are displayed near the edges (e.g. conv1, ReLU). Symbol \(\oplus\) represents concatenation.

Firstly, we apply function \(Initialization(\mathcal{V},\mathcal{E})\) at line 1 to encode Figure 9(a) as SumLinear blocks and ReLU layers, where the weights and biases of each Linear layer are displayed above the layer. We name the two ReLU nodes \(n_{1},n_{3}\) as ReLU1, ReLU2 respectively.

Figure 10: Network in Figure 9(a) encoded with SumLinear blocks and ReLU layers

Figure 9: The simplification of a non-sequential block
Then we take the last SumLinear block from Figure 10 and normalize this block (Figure 11(a)) and obtain the normalized block as in Figure 11(b). The whole network is now updated as Figure 12.

At this step, we notice that ReLU layer ReLU2 is _blocked_ by the last SumLinear block, and ReLU1 is _not blocked_ as it has another path to a subsequent ReLU layer. Therefore, we perform the Linear layer construction at line 6 and obtain the network in Figure 13.

Lastly, we take out the last SumLinear block in Figure 13 and perform normalization to obtain Figure 14. At Figure 14, the last SumLinear block includes two Linear layers having the same preceding layer ReLU1 (Figure 14), which requires further normalization.

The final architecture of the network is given in Figure 15, where we have \(\begin{bmatrix}\text{conv1-w}\\ \text{identity}\end{bmatrix}=\text{conv1-w}\oplus\text{identity}\). Now the oringal network has been simplified into a sequential one.

## VI Experiments

In this section, we present our experimental results of instantiation of network reduction technique on \(\alpha,\beta\)-CROWN [14], VeriNet [15] and PRIMA [12] to show evidence that: given the _same_ verification problem, the _same_ verification algorithm runs _faster_ on the reduced network compared to the original network, which gives us confidence in the ability of our method as in enhancing the efficiency of existing verification methods. Furthermore, the simple architecture in REDNet allows existing verification tools that only support limited network benchmarks to handle more networks.

### _Experiment Setup_

The evaluation machine has two 2.40GHz Intel(R) Xeon(R) Silver 4210R CPUs with 384 GB of main memory and a NVIDIA RTX A5000 GPU.

**Evaluation Benchmarks.** The evaluation datasets include MNIST [36] and CIFAR10/CIFAR100 [37]. MNIST dataset contains hand-written digits with 784 pixels, while CIFAR10/CIFAR100 includes colorful images with 3072 pixels. We chose fully-connected, convolutional and residual networks with various sizes from two well-known benchmarks: the academic ERAN system [38] and VNNCOMP2021/2022 (International Verification of Neural Networks Competition) [39, 40]. The number of activation layers (#Layers), the number of ReLU neurons (#Neurons), and the trained defense of each network are listed in Table II, where a trained defense refers to a defense method against adversarial samples to improve robustness. Please note that "Mixed" means mixed training, which combines adversarial training and certified defense training loss. This could lead to an excellent balance between model clean accuracy and robustness, and is beneficial for obtaining higher verified accuracy [41].

**Verification Properties.** We conduct robustness analysis, where we determine if the classification result of a neural

Figure 11: Normalization of the last SumLinear block

Figure 14: The network after the second normalization

Figure 12: The network after the first normalization

Figure 13: The network after the Linear layer construction. For simplicity to show the weight matrices, we assume that ReLU2 and ReLU1 all have one neuron; and “-biases/-weights” are abbreviated as “-b/-w” respectively.

Figure 15: The sequential network after the third normalization
network - given a set of slightly perturbed images derived from the original image (input specification) - remains the same as the ground truth label obtained from the original unperturbed image (output specification). The set of images is defined by a user-specified parameter \(\epsilon\), which perturbs each pixel \(p_{i}\) to take an intensity interval \([p_{i}-\epsilon,p_{i}+\epsilon]\). Therefore, the input space \(I\) is \(\bigtimes_{i=1}^{n}[p_{i}-\epsilon,p_{i}+\epsilon]\). In our experiment, we acquire the verification properties from the provided vnnlib files [44] that record the input and output specification or via a self-specified \(\epsilon\). We aim to speed up the analysis process for those _properties that are tough to be verified._ Hence we _filter out_ those falsified properties. We obtain around 30 properties for each tested network, as enumerated in Table II.

### _Network reduction results_

Table III shows the size of reduced networks, where the bound propagation methods crown and \(\alpha\)-crown are used to compute concrete bounds and detect stable neurons. Here we present the number of neurons in the original network and the average size after reduction (under column "AvgN") and reduction time (under column "AvgT") for the two methods. We have out-of-memory problem when running \(\alpha\)-crown on network C_100_Large, thus we mark the result as "-".

The table shows that a significant number of neurons could be reduced within a reasonable time budget by leveraging the concrete bounds returned by CROWN. Therefore, we use CROWN as our bound propagator for the rest of the experiments. On average, the reduced networks are \(10.6\times\) smaller than the original networks.

Figure 16(a) shows the reduction ratio distribution where each dot \((\alpha,\beta)\) in the figure means that the reduction ratio is greater than \(\beta\) on \(\alpha\) percent properties. The reduction ratio can be up to 95 times at the best case and greater than 20 times on 10% properties. Figure 16(b) gives the size distribution of reduced networks. Each dot \((\alpha,\beta)\) in the figure means the reduced networks have at most \(\beta\) ReLU neurons on \(\alpha\) percent properties. We can see that on more than 94% properties, there are at most 8000 ReLU neurons in the reduced networks.

### _Instantiation on \(\alpha,\beta\)-Crown_

\(\alpha,\beta\)-CROWN is GPU based and the winning verifier in VNCOMP 2021 [39] and VNNCOMP 2022 [40], the methodology of which is based on linear bound propagation framework and branch-and-bound. We first instantiate our technique on \(\alpha,\beta\)-CROWN, and we name the new system as \(\alpha,\beta\)-CROWN-R. We set the timeout of verification as 300 seconds, and if the tool fails to terminate within the timeout, we deem the result to be inconclusive. The results are listed in Table IV, where we explicitly enumerate the number of timeout properties, the number of verified properties, and the average execution time of \(\alpha,\beta\)-CROWN (column \(\alpha,\beta\)-**CROWN-O**) and our instantiated system (column \(\alpha,\beta\)-**CROWN-R**) on the properties where both methods can terminate within timeout.2

Footnote 2: When the original method is timeout or fails to execute for all properties, e.g. C_100_Med in Table V and M_ConvBig in Table VI, the average time is computed on the properties where our method can terminate within timeout.

From the result, we observe that \(\alpha,\beta\)-CROWN-R could verify more tough properties that have failed to be verified within 300 seconds in \(\alpha,\beta\)-CROWN-O. This indicates that our reduction pre-processing does not only benefit those easy verification problems but also helps verify more difficult properties within a decent time. In general, \(\alpha,\beta\)-CROWN-R verifies 11 more properties and boosts the efficiency of \(\alpha,\beta\)-CROWN-O with average \(1.52\times\) speedup on all 12 networks. The average

\begin{table}
\begin{tabular}{|l|c|c|c|c|c|} \hline
**Network** & **Type** & **\#Layers** & **\#Neurons** & **Defense** & **\#Property** \\ \hline M\_256x6 & fully-connected & 6 & 1,536 & None & 30 \\ \hline M\_ConvMed & convolutional & 3 & 5,704 & None & 31 \\ \hline M\_ConvBig & convolutional & 6 & 48,064 & DiffAf [42] & 29 \\ \hline M\_SkipNet & residual & 6 & 71,650 & DiffAI & 31 \\ \hline C\_8\_255Simp & convolutional & 3 & 16,634 & None & 30 \\ \hline C\_WideNew & convolutional & 3 & 6,244 & None & 32 \\ \hline C\_ConvBig & convolutional & 6 & 62,464 & PGD [43] & 37 \\ \hline C\_Resnet4b & residual & 10 & 14,436 & None & 30 \\ \hline C\_ResnetA & residual & 8 & 11,364 & None & 32 \\ \hline C\_ResnetB & residual & 8 & 11,364 & None & 29 \\ \hline C\_100\_Med & residual & 10 & 55,460 & Mixed & 24 \\ \hline C\_100\_Large & residual & 10 & 286,820 & Mixed & 24 \\ \hline \end{tabular}
\end{table}
Table II: Detailed information of the experimental networks

Figure 16: Visualized results of the reduction with CROWN
is computed across the networks where the speedup for each network is calculated by the reported time on the original network.

In addition, the performance of REDNet is affected by the network reduction ratio. For example, \(\alpha,\beta\)-CROWN-R only has average 1.12 speedup on M_256\(\times\)6 whose reduction ratio is only 1.55, while \(\alpha,\beta\)-CROWN-R can have average 2.52\(\times\) speedup on C_100_large whose mean reduction ratio is 39.80.

### _Instantiation on PRIMA_

PRIMA [12] is one of the state-of-the-art incomplete verification tools. It introduces a new convex relaxation method that considers multiple ReLUs jointly in order to capture the correlation between ReLU neurons in the same layer. Furthermore, PRIMA leverages LP-solving or MILP-solving to refine individual neuron bounds within a user-configured timeout. Note that PRIMA stores the connection between neurons in two ways: 1. Dense expression, which encodes the fully-connected computation in a fully-connected layer; 2. Sparse expression, that only keeps the non-zero coefficients and the indexes of preceding neurons of which the corresponding coefficients are non-zero (e.g. convolutional layer). As some affine connections between layers in our reduced network contain many zero elements (since we introduce the identity matrix in the newly constructed connection), we elect to record them as sparse expressions in the instantiated PRIMA (abbreviated as PRIMA-R).

The comparison results are given in Table V, and we set a 2000 seconds timeout for each verification query as PRIMA runs on the CPU and usually takes a long execution time for deep networks. Note that PRIMA returns segmentation fault for M_SkipNet, thus the results are marked as "-"; PRIMA times out for all properties of C_100_Med and C_100_Large, hence marked as "TO". Note that there are some cases where PRIMA-R runs slower than PRIMA-O, e.g., for network C_ConvBig. This happens because PRIMA conducts refined verification by pruning the potential adversarial label one by one within a certain timeout. Once an adversarial label fails to be pruned within the timeout, PRIMA returns unknown immediately without checking the rest of the adversarial labels. In PRIMA-R, we could prune those failed labels that previously timed out in PRIMA-O, thus continuing the verification process, which may take more overall time. But accordingly, we gain significant precision improvement, e.g. PRIMA-R can verify 9 more properties on C_ConvBig.

On average, PRIMA-R gains \(1.99\times\) speedup than PRIMA-O and verifies 60.6% more images, which indicates the strength of REDNet to improve both efficiency and precision.
of a verification tool on an unsupported network is regarded as timeout. Then Figure 17(b) shows the execution time distribution of \(\alpha,\beta\)-CROWN-R and \(\alpha,\beta\)-CROWN-O, where each position \((\alpha,\beta)\) denotes that the tool can verify \(\beta\) percent properties in \(\alpha\) seconds. For example, by setting the time limit to 10 seconds, \(\alpha,\beta\)-CROWN-R can verify 32.9% properties, and \(\alpha,\beta\)-CROWN-O only verifies 18.3% properties.

On most properties, the verification tools on REDNet are faster than the tools on the original network. Despite its generality, REDNet may achieve marginal effectiveness on certain tools or benchmarks due to the following factors:

* The reduction ratio affects the subsequent verification acceleration. A less significant reduction ratio plus the reduction cost could cause marginal overall speedup. Figure 17(e) and Figure 17(f) depict the effect of the reduction ratio on the speedup gained. Despite other factors affecting the final speedup, there is a general trend that a significant reduction ratio leads to better speedup, which may cause superb effectiveness on networks C_100_Med and C_100_Large.
* Different tools may use distinct bound propagation methods, which have different degrees of dependency on the network size. PRIMA deploys DeepPoly whose time complexity depends on \(N^{3}\) where each layer has at most \(N\) neurons [45]; as such reduction in network size can lead to better performance. \(\alpha,\beta\)-CROWN, on the other hand, uses \(\beta\)-crown. \(\beta\)-crown is used to generate constraints of output neurons defined over preceding layers until the input layer. Thus, the number of constraints does not vary, and the number of intermediate neurons can only affect the number of variables that appear in the constraint; as such, deployment of REDNET may reap a marginal effect in speedup on \(\alpha,\beta\)-CROWN compared to PRIMA. For VeriNet, it uses symbolic interval propagation to generate constraints of intermediate and output neurons defined over the input neurons. Thereby intermediate neuron size only affects the number of constraints while the number of defined variables in the constraint is fixed as the input dimension. Hence, REDNet could be less effective on VeriNet compared to PRIMA in general.
* Some layer types (e.g. Conv) may compute faster than fully-connected layers; since our method transforms these layers into fully-connected layers before performing network reduction, its efficiency may not be that significant as compared to the original layers. On the other hand, it is worth-noticing that the use of fully-connected layers improves the availability of existing tools.
* \(\alpha,\beta\)-CROWN and VeriNet are branch-and-bound based and they generate sub-problems from their respective branching heuristics, which are dependent on the original network structures. The REDNet changes the network structure, and hence the heuristic can generate different sub-problems. This may affect the performance.

We conclude empirically that REDNet has better performance (significant speedup or much more properties verified) on large networks, i.e. networks with more than 40k ReLU neurons. On the large networks, the average speedup of \(\alpha,\beta\)

\begin{table}
\begin{tabular}{|l|c|c|c|c|c|c|} \hline \multirow{2}{*}{**Neural Net**} & \multicolumn{4}{c|}{**VeriNet-O**} & \multicolumn{2}{c|}{**VeriNet-R**} \\  & \multicolumn{2}{c|}{(on original network)} & \multicolumn{2}{c|}{(on reduced network)} \\ \cline{2-7}  & \#Timeout & \#VeriNet & Time(s) & \#Timeout & \#VeriNet & Time(s) \\ \hline M\_256x6 & 27 & 3 & 52.94 & 27 & 3 & **47.78** \\ \hline M\_ConvMed & - & - & - & 19 & **12** & **23.96** \\ \hline M\_ConvBig & - & - & - & 23 & **6** & **48.81** \\ \hline C\_WideKW & 3 & 29 & 27.12 & 2 & **30** & **22.74** \\ \hline C\_8\_255Simp & 10 & 20 & 63.26 & 10 & 20 & **52.56** \\ \hline C\_ResnetA & 25 & 7 & 129.49 & 25 & 7 & **83.35** \\ \hline C\_ResnetB & 21 & 8 & 116.80 & 20 & **9** & **74.98** \\ \hline C\_100\_Med & 10 & 14 & 69.71 & 9 & **15** & **21.15** \\ \hline \end{tabular}
\end{table}
Table VI: The experiment results of VeriNet. The time is the average execution time of the properties where both methods terminate before timeout. When VeriNet-O fails to execute, e.g. M\_ConvBig, the average time is computed on the properties where our method can terminate within the timeout.

Figure 17: Visualized comparison results.
CROWN-R is 1.94\(\times\), and the average speedup of VeriNet-R is 3.29\(\times\); and PRIMA-R verifies 42 properties while PRIMA-O only verifies 11 properties.

### _Support of other verifiers for the benchmarks_

As can be seen from subsection VI-D, PRIMA fails to analyze M_SkipNet because it does not support its network architecture. However, with the introduction of REDNet, which is constructed as a fully-connected neural network, PRIMA is now able to verify M_SkipNet. A similar improvement happens to VeriNet. Therefore, our REDNet not only speeds up the verification process but also allows existing tools to handle network architectures that are not supported originally.

To further testify that the reduced network adds support to existing verification tools, we select four tools - Debona [46], Venus [47], Nnenum [48], PeregriNN [49] - from VNCOMP2021/2022 that only support limited network architectures. We select one representative verification property for each of our tested networks to check if the four designated tools can support the networks.

We present the results in Table VII where we color the left half of the circle black to indicate that the original network is supported by the tool (and white otherwise); we also color the right half of the circle black if the reduced network is supported by the tool (and white otherwise.) In general, the black color implies the network is _supported_ and the white color implies the network is _not supported_. Note that Venus does not support networks whose output layer is a ReLU layer; therefore, it cannot be executed for both the original and the reduced network for M_SkipNet. These results boost our confidence that our constructed REDNet not only accelerates the verification but also _produces a simple neural network architecture that significantly expands the scope of neural networks which various tools can handle._

## VII Discussion

We now discuss the limitation of our work.

_Supported layer types._ As described in section V, our reduced neural network contains only Affine layers (e.g. GEMM layers) and ReLU layers, therefore we could only represent non-activation layers that conduct linear computation. For example, an _Add_ layer that takes layer \(\alpha\) and layer \(\beta\) conducts linear computation as the output is computed as \(\alpha+\beta\). A _Convolutional_ layer conducts linear computation as well as it only takes one input layer and the other operands are constant weights and bias. However, we couldn't support a _Multiplication_ layer if it takes layer \(\alpha\) and layer \(\beta\) and computes \(\alpha\times\beta\) as the output. For future work, we will explore the possibility of handling more non-linear computations.

_Floating-point error._ As presented in Theorem 3, our reduction process preserves the input-output equivalence of the original network in the real-number domain. However, like many existing verification algorithms [12, 14, 24, 26] that use floating-point numbers when conducted on physical machines, our implementation involves floating-point number computation, thus inevitably introducing floating-point error. The error could be mitigated by deploying float data type with higher precision during implementation.

## VIII Related Work

Theoretically, verifying deep neural networks with ReLU functions is an NP-hard problem [17]. Particularly, the complexity of the problems grows with a larger number of _nodes_ in the network. Therefore, with the concern of scalability, many works have been proposed by over-approximating the behavior of the network. This over-approximation can be conducted by abstract interpretation techniques [1, 25, 50]; or to soundly approximate the network with _fewer nodes_[8, 9, 51, 52].

In detail, abstract interpretation-based methods over-approximate the functionality of each neuron with an abstract domain, such as box/interval [50], zonotope [1] or polyhedra [25]. These methods reason over the original neural networks without changing the number of neurons in the test network.

On the contrary, reduction methods in [8, 9, 51, 52] reduce the number of neurons in a way that over-approximates the original network's behavior. However, such over-approximation would jeopardize completeness when instantiated on complete methods. On the contrary, our reduction method captures the _exact_ behavior of the network without approximation error. Therefore REDNet could be instantiated on complete tools and even verify more properties given the same timeout. Furthermore, REDNet could handle various large networks where the previous work [51] only evaluated one large-scale network (the C_ConvBig in our benchmark) that was reduced to 25% of the original size with a very small perturbation \(\epsilon=0.001\); whereas we could reduce it to just 10% with \(\epsilon\approx 0.0078\) (properties from VNN competition 2022). We remark that the smaller perturbation, the more reduction we could gain. Other related tools in [9, 52] were only evaluated with ACAS Xu networks with a very small input dimension and network sizes, making it challenging for us to make any meaningful comparison. Last but not least, the reduced networks designed in [8, 9] use intervals or

\begin{table}
\begin{tabular}{|l|c|c|c|c|} \hline \multirow{2}{*}{**Networks(12)**} & \multicolumn{4}{c|}{**Tools**} \\ \cline{2-5}  & Venus & Debona & Nnenum & PeregriNN \\ \hline M\_256x6 & \(\bullet\) & \(\bullet\) & \(\bullet\) & \(\bullet\) \\ M\_ConvMed & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ M\_ConvBig & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ M\_SkipNet & ReLU-error & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ C\_WideKW & \(\bullet\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ C\_8\_255Simp & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ C\_ConvBig & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ C\_ResnetA & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ C\_ResnetB & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ C\_100\_Med & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ C\_100\_Large & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) & \(\mathfrak{D}\) \\ \hline \end{tabular}
\end{table} TABLE VII: The networks supported by existing verification tools. A fully black circle indicates both the original and the reduced networks are supported. A right-half black circle indicates that the tool supports only the reduced network.
values in an abstract domain to represent connection weights. Such specialized connections require implementation support if instantiated on existing verification methods. But we export REDNet as a fully-connected network in ONNX, which is an open format that is widely accepted. This makes our REDNet a versatile tool that could also be combined with existing reduction methods to lessen the network size even further as they all apply to fully-connected networks.

REDNet could benefit various verification techniques, such as branch-and-bound based methods [53, 7, 10, 5]. The key insight of the branch-and-bound method is to divide the original verification problem \(P\) into subdomains/subproblems by splitting neuron intervals. For example, one can bisect the input neuron interval such that the input space is curtailed in each subdomain; or to split an unstable ReLU neuron \(y\) (whose input value can be both negative and positive) at the point 0, thereby \(y\) will be stably activated or stably deactivated in the subdomains. Our _network reduction_ technique, once applied at the beginning of branch-and-bound based methods, will help generates easier subproblems based on a small-sized network, thus accelerating the whole analysis process without sacrificing verification precision.

Furthermore, the reduced network could accelerate abstract refinement based processes like PRIMA [12], where it encodes the network constraints and resolves individual neuron bounds. As REDNet contains fewer neurons and connections, the solving process involves a smaller set of constraints, which leads to overall speedup.

## IX Conclusion

In this work, we propose the _neural network reduction_ technique, which constructs a reduced neural network with fewer neurons and connections while capturing the _same_ behavior as the original tested neural network. In particular, we provide formal definitions of stable ReLU neurons and deploy the state-of-the-art bound propagation method to detect such stable neurons and _remove_ them from the neural network in a way that preserves the network functionality. We conduct extensive experiments over various benchmarks and state-of-the-art verification tools. The results on a large set of neural networks indicate that our method can be instantiated on different verification methods, including \(\alpha,\beta\)-CROWN, VeriNet and PRIMA, to expedite the analysis process further.

We believe that our method is an efficient pre-processing technique that returns a functionally-equivalent reduced network on which the same verification algorithm runs faster, correspondingly enhancing the efficiency of existing verification methods for them to answer tough verification queries within a decent time budget. Moreover, the simplified network architectures in REDNets empower existing tools to handle a wider range of networks they could not support previously.

## Acknowledgment

This research is supported by a Singapore Ministry of Education Academic Research Fund Tier 1 T1-251RES2103. The second author is supported by NUS grant T1 251RES2219.
