Fully Automatic Neural Network Reduction for Formal Verification
Formal verification of neural networks is essential before their deployment
in safety-critical applications. However, existing methods for formally
verifying neural networks are not yet scalable enough to handle practical
problems involving a large number of neurons. We address this challenge by
introducing a fully automatic and sound reduction of neural networks using
reachability analysis. The soundness ensures that the verification of the
reduced network entails the verification of the original network. To the best
of our knowledge, we present the first sound reduction approach that is
applicable to neural networks with any type of element-wise activation
function, such as ReLU, sigmoid, and tanh. The network reduction is computed on
the fly while simultaneously verifying the original network and its
specifications. All parameters are automatically tuned to minimize the network
size without compromising verifiability. We further show the applicability of
our approach to convolutional neural networks by explicitly exploiting similar
neighboring pixels. Our evaluation shows that our approach can reduce the
number of neurons to a fraction of the original number of neurons with minor
outer-approximation and thus reduce the verification time to a similar degree.
Tobias Ladner, Matthias Althoff
# Specification-Driven Neural Network Reduction for Scalable Formal Verification

###### Abstract

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.

## 1 Introduction

Neural networks achieve impressive results in a variety of fields such as autonomous cars [1]. However, the applicability of neural networks in safety-critical environments is still limited as small perturbations of the input can lead to unexpected outputs of the neural network [2]. Thus, the formal verification of neural networks gained importance in recent years [3], where approaches rigorously prove that the output of neural networks meets given specifications. These approaches are often based on satisfiability modulo theory solvers [4; 5], symbolic interval propagation [6; 7], or deploy reachability analysis [8; 9; 10; 11]. However, scalability is still a major issue for all of them [3].

While several approaches [12; 13] exist which reduce the size of the network by approximating the original network, to our best knowledge, there exist only a few reduction approaches with formal error bounds. An early approach [14] splits the neurons based on analytic properties and merges similar neurons afterward. This work is extended using interval neural networks [15; 16] and residual reasoning [17]. More closely related to our work is the approach in [18], which approximates the neural network output by merging neurons using clustering algorithms on a given dataset, however, \(80-90\%\) of the neurons remain when formal error bounds are demanded. Most approaches only consider ReLU neurons; however, [15] also considers tanh neurons. A network reduction algorithm with formal error bounds for general neurons is still missing.

We propose a novel approach that reduces the neural network for given specifications. For example, consider an image as an input to a neural network. Neurons representing neighboring pixels often have similar values and thus can be merged during the verification process, which helps to reduce the high dimensionality of these neural networks. Such properties cannot be inferred when analyzing a neural network without considering a specific input. Our novel approach is orthogonal to many verification techniques, thus, many of them can be used as an underlying verification engine. We demonstrate our approach by deploying reachability analysis using zonotopes [9], the extension to
other set-based verification tools is straightforward including Taylor models [19; 10] and polynomial zonotopes [11].

To summarize our main contributions, we present a novel, formally sound approach to reduce large neural networks by merging similar neurons for given specifications. The reduced network is constructed on-the-fly and the verification of the reduced network entails the verification of the original network. Our approach works on a variety of common activation functions, including ReLU, sigmoid, and tanh. The evaluation of high-dimensional datasets and benchmarks shows that the networks can be reduced to less than \(5\%\) of the original number of neurons using our novel approach. The overhead of constructing the reduced network is computationally cheap and thus the overall time for verifying the original network primarily depends on the number of remaining neurons in the reduced network.

The rest of this work is structured as follows. Sec. 2 introduces the notation and background for this work, then Sec. 3 presents our novel neuron-merging approach. We first show how similar neurons can be merged with formal error bounds, followed by the algorithm to construct the reduced network on-the-fly while verifying the original network. Finally, we evaluate our approach in Sec. 4 and conclude this work in Sec. 5.

## 2 Preliminaries

### Notation

We denote vectors by lower-case letters, matrices by upper-case letters, and sets by calligraphic letters. The \(i\)-th element of a vector \(b\in\mathbb{R}^{n}\) is written as \(b_{(i)}\). Consequently, \(b_{2(i)}\) is the \(i\)-th element of a vector \(b_{2}\). The element in the \(i\)-th row and \(j\)-th column of a matrix \(A\in\mathbb{R}^{n\times m}\) is written as \(A_{(i,j)}\), the entire \(i\)-th row and \(j\)-th column are written as \(A_{(i,\cdot)}\) and \(A_{(\cdot,j)}\), respectively. The concatenation of two matrices \(A\) and \(B\) is denoted by \([A\ B]\). Given \(n\in\mathbb{N}\), then \([n]=\{1,\ldots,n\}\). Let \(\mathcal{C}\subseteq[n]\), then \(A_{(\mathcal{C},\cdot)}\) denotes all rows \(i\in\mathcal{C}\). The cardinality of a discrete set \(\mathcal{C}\) is denoted by \(|\mathcal{C}|\). Let \(\mathcal{S}\subset\mathbb{R}^{n}\) be a set of dimension \(n\), then \(\mathcal{S}_{(i)}\) is its projection on the \(i\)-th dimension. Given a function \(f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}\), then \(f(\mathcal{S})=\{f(x)\mid x\in\mathcal{S}\}\). An interval with bounds \(a,b\in\mathbb{R}^{n}\) is denoted by \([a,b]\).

### Neural Networks

In this work, we describe the reduction of feed-forward neural networks [20, Sec. 5.1]). We further note that our approach is also applicable to convolutional neural networks [20, Sec. 5.5.8], as convolutional layers and subsampling layers, e.g. average pooling layers, can be transformed into linear layers as defined subsequently.

**Definition 1**.: _(Layers of Neural Networks [20, Sec. 5.1]) Let \(v_{k}\) denote the number of neurons in a layer \(k\) and \(h_{k-1}\in\mathbb{R}^{v_{k-1}}\) the input. Further, let \(W\in\mathbb{R}^{v_{k}\times v_{k-1}},b\in\mathbb{R}^{v_{k}}\), and \(\sigma_{k}(\cdot)\) be the respective continuous activation function (e.g. sigmoid and ReLU), which is applied element-wise. Then, the operation \(L_{k}:\mathbb{R}^{v_{k-1}}\rightarrow\mathbb{R}^{v_{k}}\) on layer \(k\) is given by_

\[L_{k}(h_{k-1})=\left\{\begin{array}{ll}W_{k}h_{k-1}+b_{k},&\text{if layer $k$ is linear},\\ \sigma_{k}(h_{k-1}),&\text{otherwise.}\end{array}\right. \tag{1}\]

**Definition 2**.: _(Neural Networks [20, Sec. 5.1]) Given \(K\) alternating linear and nonlinear layers, \(v_{0}\) input and \(v_{K}\) output neurons, and let \(x\in\mathbb{R}^{v_{0}}\) be the input and \(y\in\mathbb{R}^{v_{K}}\) be the output of a neural network, then, a neural network \(\Phi\) with \(y=\Phi(x)\) can be formulated as_

\[h_{0}=x,\quad h_{k}=L_{k}(h_{k-1}),\quad y=h_{K},\qquad k=1\ldots K. \tag{2}\]

We call the last linear and the last nonlinear layer output layers, all other layers are hidden layers. If all hidden layers output the same number of neurons, we write \(6\times 200\) to refer to a network with 6 linear and \(6\) nonlinear hidden layers with \(200\) neurons each.

### Set-based Computation

We use sets for the formal verification of neural networks. Let \(\mathcal{X}\) be the input set of the neural network. Then, the exact output sets of each layer are denoted by
\[\mathcal{H}_{0}^{*}=\mathcal{X},\quad\mathcal{H}_{k}^{*}=L_{k}(\mathcal{H}_{k-1}^{* }),\quad\mathcal{Y}^{*}=\mathcal{H}_{K}^{*},\qquad k=1\ldots K. \tag{3}\]

We use zonotopes as set representation to demonstrate our novel network reduction approach.

**Definition 3**.: _(Zonotope [21, Def. 1]) Given a center vector \(c\in\mathbb{R}^{n}\) and a generator matrix \(G\in\mathbb{R}^{n\times q}\), a zonotope is defined as_

\[\mathcal{Z}=\left\langle c,G\right\rangle_{Z}=\left\{c+\sum_{j=1}^{q}\beta_{j} G_{(\cdot,j)}\ \Bigg{|}\ \beta_{j}\in[-1,1]\right\}. \tag{4}\]

Further, we define two basic operations on zonotopes, which are essential for our approach. These operations can also be applied to many other set representations such as Taylor models and polynomial zonotopes.

**Proposition 1**.: _(Interval Enclosure [22, Prop. 2.2]) Given a zonotope \(\mathcal{Z}=\left\langle c,G\right\rangle_{Z}\), then the interval \([l,u]=\texttt{interval}(\mathcal{Z})\supseteq\mathcal{Z}\) is given by_

\[\begin{array}{l}l=c-\Delta g\\ u=c+\Delta g\end{array},\quad\text{with}\ \Delta g=\sum_{j=1}^{q}|G_{(\cdot,j)}|. \tag{5}\]

**Proposition 2**.: _(Interval Addition [22, (2.1)]) Given a zonotope \(\mathcal{Z}=\left\langle c,G\right\rangle_{Z}\subset\mathbb{R}^{n}\) and an interval \(\mathcal{I}=[l,u]\subset\mathbb{R}^{n}\), then_

\[\mathcal{Z}\oplus\mathcal{I}=\left\langle c+c_{\mathcal{I}},[G\texttt{ diag}(u-c_{\mathcal{I}})]\right\rangle_{Z}, \tag{6}\]

_where \(c_{\mathcal{I}}=\frac{l+u}{2}\) and diag creates a diagonal matrix._

### Neural Network Verification

Finally, we briefly introduce the main steps to propagate a zonotope through a neural network. The propagation cannot be computed exactly in general, thus, the exact output of each layer needs to be enclosed.

**Proposition 3**.: _(Image Enclosure [9, Sec. 3]) Let \(\mathcal{H}_{k-1}\supseteq\mathcal{H}_{k-1}^{*}\) be an input set to layer \(k\), then_

\[\mathcal{H}_{k}=\texttt{enclose}(L_{k},\mathcal{H}_{k-1})\supseteq\mathcal{H }_{k}^{*} \tag{7}\]

_computes an over-approximative output set._

Linear layers can be computed exactly using zonotopes [21], however, nonlinear layers introduce over-approximations. We refer to [9, Sec. 3] for a detailed explanation, the main steps are as follows and are visualized in Fig. 1: For each nonlinear layer, we iterate over all neurons \(i\) in the current layer by projecting the input set \(\mathcal{H}_{k-1}\) onto its \(i\)-th dimension (step 1) and determine the input bounds using Prop. 1 (step 2). We then find a linear approximation polynomial within the input bounds via regression [20, Sec. 3] (step 3). A key challenge is bounding the approximation error (step 4): For piece-wise linear activation functions, e.g. ReLU, we can compute the approximation error exactly using the extreme points of the difference between the approximation polynomial and each linear segment. For other activation functions, e.g. sigmoid, the approximation error can be determined by sampling evenly within the input bounds and bounding the approximation error between two points via global bounds of the derivative. Finally, we evaluate \(\mathcal{H}_{k-1(i)}\) on the polynomial (step 5) and add the approximation error as an additional generator (step 6, Prop. 2).

Figure 1: Main steps of enclosing a nonlinear layer. Step 1: Neuron-wise Sigmoid function. Step 2: Input bounds. Step 3: Approximation polynomial. Step 4: Approximation error. Step 5: Evaluate input on polynomial. Step 6: Add approximation error.
### Problem Statement

Given an input set \(\mathcal{X}\subset\mathbb{R}^{v_{0}}\), a neural network \(\Phi\) as specified in Def. 2, and an unsafe set \(\mathcal{S}\subset\mathbb{R}^{v_{K}}\) in the output space of \(\Phi\), we want to find a reduced network \(\widehat{\Phi}\) for which the verification entails the safety of the original network for \(\mathcal{X},\mathcal{S}\). Thus, it must hold

\[\widehat{\Phi}(\mathcal{X})\cap\mathcal{S}=\emptyset\ \implies\ \Phi(\mathcal{X})\cap\mathcal{S}=\emptyset. \tag{8}\]

## 3 Specification-Driven Neural Network Reduction

Our novel approach is based on the observation that many neurons in a layer \(k\) behave similarly for a specific input \(x\), e.g. many sigmoid neurons are fully saturated and thus output a value near 1 as shown in Fig. 2. Neuron saturation [23], neural activation patterns [24], and over-parametrization [25] have been observed in the literature, however, to the best of our knowledge, it has not been considered during the verification of neural networks. Our main idea is to merge similar neurons such as these saturated neurons and provide the corresponding error bounds. Our novel approach is not restricted to the saturation values of an activation function but can merge neurons with any activation.

### Neuron Merging

Subsequently, we explain how this observation can help to construct a much smaller network \(\widehat{\Phi}\), where the verification of \(\widehat{\Phi}\) entails the verification of the original network \(\Phi\). We denote the neurons which are merged using merge buckets:

**Definition 4**.: _(Merge Buckets) Given output bounds \(\mathcal{I}_{k}\supseteq\mathcal{H}_{k}^{*}\) of a nonlinear layer \(k\) with \(v_{k}\) neurons, an output \(y\in\mathbb{R}\), and a tolerance \(\delta\in\mathbb{R}\), then a merge bucket is defined as_

\[\mathcal{B}_{k,y,\delta}=\left\{w\in[v_{k}]\ \big{|}\ \mathcal{I}_{k(w)} \subseteq[y-\delta,y+\delta]\right\}. \tag{9}\]

Conceptually, we replace all neurons in \(\mathcal{B}_{k,y,\delta}\) by a single neuron with constant output \(y\) and adjust the weight matrices of the linear layers \(k-1,k+1\) such that the reduced network \(\widehat{\Phi}\) approximates the behavior of the original network \(\Phi\). Finally, we add an approximation error to the output to obtain a sound over-approximation (Fig. 3). As the new neuron is constant, we can propagate it forward to the bias of the layer \(k+1\) without inducing an over-approximation.

**Proposition 4**.: _(Neuron Merging) Given a nonlinear hidden layer \(k\) of a network \(\Phi\), output bounds \(\mathcal{I}_{k}\supseteq\mathcal{H}_{k}^{*}\), and a merge bucket \(\mathcal{B}_{k,y,\delta}\), then we can construct a reduced network \(\widehat{\Phi}\), where we remove

Figure 2: Sigmoid activations of a 6x200 neural network with an image input from the MNIST digit dataset. In this neural network, many neurons output values close to the saturation values 0 and 1.
the merged neurons by adjusting the linear layers \(k-1\), \(k-1\) such that_

\[\widehat{W}_{k-1} =W_{k-1(\overline{\mathcal{B}}_{k,y,\delta},\cdot)}, \quad\widehat{b}_{k-1} =b_{k-1(\overline{\mathcal{B}}_{k,y,\delta})}, \tag{10}\] \[\widehat{W}_{k+1} =W_{k+1(\cdot,\overline{\mathcal{B}}_{k,y,\delta})}, \quad\widehat{b}_{k+1} =b_{k+1}+\underbrace{W_{k+1(\cdot,\mathcal{B}_{k,y,\delta})} \mathcal{I}_{k(\mathcal{B}_{k,y,\delta})}}_{\text{approximation error}},\]

_where \(\overline{\mathcal{B}}_{k,y,\delta}=[v_{k}]\backslash\mathcal{B}_{k,y,t}\) and \(\widehat{b}_{k+1}\) includes the approximation error. We denote the layer operations of the reduced network \(\widehat{\Phi}\) with \(\widehat{L}_{k}\). The construction is sound._

Proof.: _Soundness._ We show that the output \(\widehat{\mathcal{H}}_{k+1}\) of layer \(k+1\) of the reduced network \(\widehat{\Phi}\) is an over-approximation of the exact set \(\mathcal{H}_{k+1}^{*}\) as defined in (3). We drop the indices of \(\mathcal{B}_{k,y,\delta},\overline{\mathcal{B}}_{k,y,\delta}\) for conciseness:

\[\mathcal{H}_{k+1}^{*} \stackrel{{\eqref{eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eqeq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eqeq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eqeq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eqeq:eq:eq:eq:eq:eq:eq:eq:eq:eq:eqeq:eq:eq:eq:eq:eqeq:eq:eq:eq:eq:eq:eq:eqeq:eq:eqeq:eq:eq:eq:eqeq:eq:eq:eq:eq:eq:eqeq:eq:eq:eq:eqeq:eq:eq:eqeq:eq:eq:eqeq:eq:eqeq:eq:eqeq:eq:eq:eq:eqeq:eqeq:eq:eq:eq:eqeq:eqeq:eq:eq:eq:eqeq:eq:eqeq:eq:eqeq:eq:eqeq:eq:eqeq:eqeq:eq:eqeq:eqeq:eqeq:eqeq:eqeq:eq:eqeq:eq:eqeq:eqeq:eqeq:eq:eqeq:eqeq:eq:eqeq:eq:eqeq:eqeq:eq:eqeq:eq:eqeq:eq:eq:eqeq:eqeq:eqeq:eq:eq:eq:eqeq:eq:eqeq:eqeq:eq:eqeq:eqeq:eqeq:eqeq:eq:eq:eqeq:eqeq:eq:eqeq:eq:eqeq:eq:eq:eqeq:eqeq:eq:eqeq:eqeq:eq:eqeq:eqeq:eq:eqeq:eqeq:eqeq:eq:eqeq:eq:eqeq:eqeq:eqeq:eqeqeq:eqeq:eqeq:eq:eqeq:eqeq:eq:eqeq:eqeq:eq:eqeq:eq:eqeq:eq:eq:eqeq:eq:eqeq:eq:eqeq:eqeq:eq:eqeq:eq:eqeq:eq:eqeq:eqeq:eqeq:eqeq:eq:eq:eqeq:eq:eq:eq:eqeq:eq:eq:eqeq:eqeq:eqeq:eqeq:eq:eqeq:eq:eqeq:eq:eqeq:eqeq:eqeq:eqeq:eqeq:eq:eqeq:eq:eq:eqeq:eq:eqeqeq:eq:eqeq:eqeq:eq:eq:eqeq:eqeq:eq:eq:eqeq:eqeq:eq:eq:eqeq:eqeq:eq:eqeq:eq:eq:eqeq:eqeq:eq:eqeq:eq:eqeq:eq:eq:eqeq:eq:eq:eqeq:eq:eqeq:eqeq:eqeq:eq:eqeq:eq:eqeq:eq:eq:eqeq:eq:eqeq:eqeq:eq:eq:eqeq:eq
Static buckets.The merge buckets are determined by the asymptotic values of the respective activation function:

\[\mathbf{\mathcal{B}}_{\text{Sigmoid}}=\left\{\mathcal{B}_{\cdot,0,\delta},\;\mathcal{ B}_{\cdot,1,\delta}\right\},\quad\mathbf{\mathcal{B}}_{\text{Tanh}}=\left\{ \mathcal{B}_{\cdot,-1,\delta},\;\mathcal{B}_{\cdot,1,\delta}\right\},\quad\mathbf{ \mathcal{B}}_{\text{ReLU}}=\left\{\mathcal{B}_{\cdot,0,\delta}\right\}. \tag{13}\]

Dynamic buckets.The merge buckets are dynamically created based on the output bounds \(\mathcal{I}_{k}=[l_{k},u_{k}]\subset\mathbb{R}^{v_{k}}\):

\[\mathbf{\mathcal{B}}_{k,\delta}=\left\{\mathcal{B}_{k,c_{k(w)},\delta}\;\middle|\; c_{k}=(l_{k}+u_{k})/2,\;w\in[v_{k}]\right\}. \tag{14}\]

Bucket tolerance.The bucket tolerance \(\delta\) is obtained by initially setting a large \(\delta\) that allows for aggressive neuron merging and then decreasing \(\delta\) adaptively if the specifications \(\mathcal{S}\) are violated.

### On-the-fly Neural Network Reduction

Note that we require output bounds \(\mathcal{I}_{k}\) of the next nonlinear layer \(k\) to determine which neurons can be merged (Prop. 4). However, computing them requires the construction of high-dimensional zonotopes via the next linear layer \(k-1\), propagating them through the nonlinear layer \(k\) -- where we have to evaluate all neurons, which is what should be avoided. Thus, we deploy a look-ahead algorithm using interval arithmetic [26] to avoid these expensive computations and reduce the network on-the-fly. The algorithm is summarized in Alg. 1.

```
1:Input \(\mathcal{X}\), neural network layers \(k\in[K]\), bucket tolerance \(\delta\)
2:\(\mathcal{H}_{0}\leftarrow\mathcal{X}\)
3:\(\widehat{L}_{1}\gets L_{1}\)
4:for\(k=2,4,\dots,K\)do\(\triangleright\) Look ahead
5:if\(k<K\)then\(\mathcal{I}_{k-2}\leftarrow\texttt{interval}(H_{k-2})\)\(\triangleright\) Prop. 1
6:if\(k>2\)then\(\mathcal{I}_{k-2}\leftarrow\mathcal{I}_{k-2}\cap\widehat{L}_{k-2}(\mathcal{I}_{k-3})\)endif\(\triangleright\) Tighten bounds
7:\(\mathcal{I}_{k}\gets L_{k}(\widehat{L}_{k-1}(\mathcal{I}_{k-2}))\)
8: Create merge buckets \(\mathbf{\mathcal{B}}_{k,\delta}\)\(\triangleright\) Sec. 3.2
9:\(\widehat{L}_{k-1},\widehat{L}_{k},\widehat{L}_{k+1}\leftarrow\text{Reduce network}\)\(\triangleright\) Prop. 4
10:endif\(\triangleright\) Verify
11:\(\mathcal{H}_{k-1}\leftarrow\texttt{enclose}(\widehat{L}_{k-1},\mathcal{H}_{k-2})\)\(\triangleright\) Prop. 3
12:\(\mathcal{H}_{k}\leftarrow\texttt{enclose}(\widehat{L}_{k},\mathcal{H}_{k-1})\)
13:endfor
14:\(\mathcal{Y}\leftarrow\mathcal{H}_{K}\)
15:return\(\mathcal{Y}\)
```

**Algorithm 1** On-the-fly Neural Network Reduction

Instead of propagating the zonotope itself forward, we just propagate the interval bounds to the next nonlinear layer \(k\) (line 5-7). The overhead is computationally cheap and the bound computation is over-approximative. The bounds \(\mathcal{I}_{k-2}\) can be intersected with \(L_{k-2}(\mathcal{I}_{k-3})\) if \(k>2\) to get a tighter estimate (line 6), as \(\mathcal{I}_{k-3}\) is computed anyway during the enclosure of the nonlinear layer \(k-2\) (line 13; Fig. 1). After \(\mathcal{I}_{k}\) is obtained, the merge buckets are determined (line 8) and the network is reduced by merging the respective neurons (line 9). Finally, we propagate the zonotope \(\mathcal{H}_{k-2}\) on the reduced network. The addition of the interval bias of layer \(k+1\) in (10) is computed using Prop. 2. Thus, we never construct a high-dimensional zonotope during the verification. Note that the number of input and output neurons remains unchanged.

**Proposition 5**.: _(Reduced Network) Given a neural network \(\Phi\) and an input set \(\mathcal{X}\), then Alg. 1 constructs a reduced network \(\widehat{\Phi}\), which satisfies the problem statement in Sec. 2.5._

Proof.: The algorithm is sound as each step is over-approximative.
## 4 Evaluation

We evaluate our novel network reduction approach using several benchmarks and neural network variants from the VNN Competition [3]. For all datasets and networks, we sample \(100\) correctly classified images from the test set and average the results. All following figures show the mean remaining input neurons per layer \(k\in[K]\) as well as the number of output neurons of the network at \(K+1\). The number of neurons of the original network is shown in the same color with reduced opacity and dynamic merge bucket creation (14) is used in all figures if not otherwise stated. We implement our approach in MATLAB and use CORA [27; 11] to verify the neural networks. All computations were performed on an Intel(r) Core(tm) Gen. 11 i7-11800H CPU @2.30GHz with 64GB memory.
ERAN benchmark in Tab. 1. While it is expected that a more aggressive neuron merging (larger \(\delta\)) results in fewer verified instances, we want to stress that using a very small \(\delta\) can already result in many merged neurons. We observe similar results for the other benchmarks as well. All following figures use a perturbations radius \(r=0.001\) and a bucket tolerance \(\delta=0.005\). Fig. 4 shows the neuron reduction per layer for this combination. The number of remaining neurons in the reduced networks is very similar for both activation functions. The overhead of constructing the reduced network is computationally cheap as shown in Fig. 5: We normalize the time to construct and verify the reduced network per image, where the verification of the original network takes \(\sim 0.67s\). The verification time primarily depends on the remaining number of neurons. Our evaluation shows that the reduction on the ReLU network uses up to 5 dynamic merge buckets per layer and on the sigmoid network around 10 dynamic merge buckets per layer. Finally, Fig. 6 shows that the benefit of our novel reduction approach increases with the size of the network, as less neurons remain in the reduced network relative to the size of the original network.
such extreme outputs as shown in Fig. 2. Fig. 10 shows another extreme case, where many ReLU neurons output zeros and thus can be removed. For this benchmark, we use the static merge buckets defined in (13) to only remove ReLU neurons with negative input. However, in general it is advisable to use dynamic merge buckets as previously shown in Fig. 10.

### CIFAR-10 Colored Image Dataset

Finally, we show that our approach is also applicable to the CIFAR-10 colored image dataset. The size of networks trained on CIFAR-10 is typically much larger due to the complexity of the dataset. We note that the CIFAR-10 images are not normalized to \([0,1]\).

Marabou benchmark.We show the network reduction on the Marabou benchmark in Fig. 10. The networks consist of two convolutional layers followed by three linear layers with ReLU activation. Our novel approach reduces these networks significantly, where more neurons are merged in larger networks.

Cifar2020 benchmark.The network consists of four convolutional layers with up to \(32,768\) neurons per layer followed by three linear layers and ReLU activation. A dynamic merge bucket creation reduces the number of neurons to \(25\%\) while still verifying all images.

### Discussion

We want to stress that our novel reduction method barely increases the over-approximation of the output \(\mathcal{Y}\) by construction, as the over-approximation induced by the neuron merging is determined by the bucket tolerance \(\delta\). It is advisable to start with a large \(\delta\) and automatically decrease \(\delta\) until an image is verified. For example, consider the sigmoid network in Tab. 1: About \(85\%\) of the images can be verified with \(\delta\geq 0.01\) in less than a third of the original verification time. While some networks have many activation neurons output near their asymptotic values, this is not the case for all networks. Thus, a dynamic creation of the merge buckets is important. Our approach is also applicable to convolutional neural networks as shown in the evaluation, which are usually especially high-dimensional. As neighboring pixels are often similar and remain similar through convolutional layers, our approach can reduce the dimensionality drastically for these networks.

## 5 Conclusion

We present a novel, conservative neural network reduction approach, where the verification of the reduced networks entails the verification of the original network. To our best knowledge, our approach is the first approach that works on a variety of activation functions and considers the specifications. The neural network reductions is computed on-the-fly while verifying the original network. Our approach merges neurons of nonlinear layers based on the output bounds of these neurons. These output bounds are computed by looking ahead to the next nonlinear layer using interval arithmetic,
such that the more expensive verification algorithm only needs to be executed on the reduced network. Our novel approach is orthogonal to many verification tools and thus can be used in combination with them. We show the applicability of our approach on various benchmarks and network architectures. The overhead of computing the reduced network is not computationally expensive and the over-approximation of the output set barely increases. We believe that our work is a significant step toward more scalable neural network verification.

## Acknowledgments and Disclosure of Funding

The authors gratefully acknowledge financial support from the project FAI funded by the German Research Foundation (DFG) under project number 286525601.
