DelBugV: Delta-Debugging Neural Network Verifiers
Deep neural networks (DNNs) are becoming a key component in diverse systems
across the board. However, despite their success, they often err miserably; and
this has triggered significant interest in formally verifying them.
Unfortunately, DNN verifiers are intricate tools, and are themselves
susceptible to soundness bugs. Due to the complexity of DNN verifiers, as well
as the sizes of the DNNs being verified, debugging such errors is a daunting
task. Here, we present a novel tool, named DelBugV, that uses automated delta
debugging techniques on DNN verifiers. Given a malfunctioning DNN verifier and
a correct verifier as a point of reference (or, in some cases, just a single,
malfunctioning verifier), DelBugV can produce much simpler DNN verification
instances that still trigger undesired behavior -- greatly facilitating the
task of debugging the faulty verifier. Our tool is modular and extensible, and
can easily be enhanced with additional network simplification methods and
strategies. For evaluation purposes, we ran DelBugV on 4 DNN verification
engines, which were observed to produce incorrect results at the 2021 neural
network verification competition (VNN-COMP'21). We were able to simplify many
of the verification queries that trigger these faulty behaviors, by as much as
99%. We regard our work as a step towards the ultimate goal of producing
reliable and trustworthy DNN-based software.
Raya Elsaleh, Guy Katz
# DelBugV: Delta-Debugging Neural

###### Abstract

Deep neural networks (DNNs) are becoming a key component in diverse systems across the board. However, despite their success, they often err miserably; and this has triggered significant interest in formally verifying them. Unfortunately, DNN verifiers are intricate tools, and are themselves susceptible to soundness bugs. Due to the complexity of DNN verifiers, as well as the sizes of the DNNs being verified, debugging such errors is a daunting task. Here, we present a novel tool, named DelBugV, that uses automated _delta debugging_ techniques on DNN verifiers. Given a malfunctioning DNN verifier and a correct verifier as a point of reference (or, in some cases, just a single, malfunctioning verifier), DelBugV can produce much simpler DNN verification instances that still trigger undesired behavior -- greatly facilitating the task of debugging the faulty verifier. Our tool is modular and extensible, and can easily be enhanced with additional network simplification methods and strategies. For evaluation purposes, we ran DelBugV on 4 DNN verification engines, which were observed to produce incorrect results at the 2021 neural network verification competition (VNN-COMP'21). We were able to simplify many of the verification queries that trigger these faulty behaviors, by as much as 99%. We regard our work as a step towards the ultimate goal of producing reliable and trustworthy DNN-based software.

## I Introduction

Deep neural networks (DNNs) [22] are software artifacts that are generated automatically, through the generalization of a finite set of examples. These artifacts have been shown to outdo manually crafted software in a variety of key domains, such as natural language processing [20, 26, 38], image recognition [26, 62], protein folding [27, 42], and many others. However, this impressive success comes at a price: unlike traditional software, DNNs are opaque artifacts, and are incomprehensible to humans. This poses a serious challenge when it comes to certifying, modifying, extending, repairing or reasoning about them [23, 28, 33].

In an effort to address these issues, the formal methods community has taken up an interest in _DNN verification_[28, 31, 47]: automated techniques that can determine whether a DNN satisfies a prescribed specification, and provide a counter-example if it does not. DNN verification technology has been making great strides, and its applicability has been demonstrated in various domains [2, 3, 4, 19, 31, 34]. In fact, this technology has progressed to a point where DNN verifiers themselves have become quite complex, and consequently error-prone; especially as they often perform delicate arithmetic operations, which can also introduce bugs into the verification process [31]. Thus, it is not surprising that various bugs have been observed in these tools [30]. For example, in the VNN-COMP'21 competition [10], various verifiers have been shown to disagree on the result of multiple verification queries (each query is comprised of a neural network and a property to be checked), or produce incorrect counter-examples, indicating the existence of bugs. Moreover, many of these verifiers are still being developed, with new and experimental features being introduced -- potentially introducing new bugs as well. An inability to trust the results of DNN verifiers could undermine the benefits of DNN verification technology, and clearly needs to be addressed.

Here, we propose to mitigate this issue by adopting known techniques from related fields (e.g., SMT solving [13]) -- specifically, that of _delta debugging_. The idea is to leverage the fact that DNN verification is at a point where many verification tools are available, and to allow engineers to readily compare the results produced by their verification tool to those produced by others, in order to identify and correct bugs. When a verification query that triggers some bug in a verifier is detected, we can initiate an automated process that repeatedly and incrementally _simplifies_ the verification query. After each simplification step, we can check that the verifier in question still disagrees with the remaining, _oracle_ verifiers, until reaching the simplest verification query that we can find. If this final query is much simpler than the original, it will be that much easier for engineers to debug their tools, eventually improving their overall soundness.

We present a new tool, DelBugV (**Delta** de**Bug**ging **I**e**nural **N**etwork **V**erifiers), that takes as input a verification query, a malfunctioning DNN verifier that errs on the given verification query, and an oracle DNN verifier. Within DelBugV, we implement a set of operations for simplifying the neural network of the given verification query into a network with fewer layers and fewer neurons. We empirically design a strategy that applies these operations sequentially in an order that produces much simpler verification queries. In some cases, when the malfunctioning DNN verifier produces a faulty counter-example, DelBugV can run in _single solver_ mode - without an oracle verifier, where the query is repeatedly simplified as long as the malfunctioning DNN verifier continues to produce incorrect counter-examples.

For evaluation, we tested DelBugV on 4 DNN verifiers "suspected" of errors, per the results of VNN-COMP'21 [10]: Marabou [33, 43, 61], NNV [52, 53, 54, 55, 63], NeuralVerification.jl(NV,jl) [37], and nennum [8, 9, 52, 53]. We ran DelBugV on queries where pairs of these verifiers disagreed. Our evaluation demonstrates that DelBugV could reduce the size of the error-triggering queries by an average of \(96.8\%\), and
by as much as \(99\%\) in some cases, resulting in very simple neural networks. We believe that these results highlight the significant potential of our tool and approach.

The rest of the paper is organized as follows. In Sec. II we provide the necessary background on DNNs and their verification. Next, in Sec. III we describe the design of DelBugV, focusing on its algorithm and network simplification methods and the strategy we use to apply those methods. The implementation and evaluation of DelBugV is discussed in Sec. IV. This is followed by a discussion of related work in Sec. V, and we conclude in Sec. VI.

## II Background

**Neural Networks.** A _neural network_ is a directed acyclic graph in which the nodes, called neurons, are organized in layers \(l^{0},l^{1},\ldots,l^{n}\), \(l^{0}\) is called the input layer, \(l^{n}\) the output layer, and layers \(l^{1},\ldots,l^{n-1}\) are called hidden layers. Each hidden layer has an associated non-linear _activation function_. In feed-forward networks, which are our subject matter here, neurons in layer \(l^{i}\) have edges connecting them only to neurons in the next layer, layer \(l^{i+1}\).

Each neuron in the network (except the ones in the input layer) has a bias value, and each edge has a weight. The biases and weights belonging to neurons in layer \(l^{i}\) are organized into a vector \(B^{i}\) and a matrix \(W^{i}\), respectively. The \(j,j^{\prime}\)-th entry of \(W^{i}\) is the weight assigned to the edge out-going from the \(j^{\prime}\)-th neuron in layer \(l^{i-1}\) and entering the \(j\)-th neuron in layer \(l^{i}\). For a _fully connected_ layer, \(W^{i}\) is a full matrix; whereas for a _convolutional_ layer, \(W^{i}\) is very sparse, and has a specific structure (discussed later).

An input to neural network \(\mathcal{N}\) is a vector \(I\) of values of the neurons in the input layer, and it produces an output vector \(\mathcal{N}(I)\) which is the values of the neurons in the output layer. We denote the values of neurons in layer \(l^{i}\), prior to applying the activation function, by \(\mathcal{N}^{l^{i}}(I)\); and the values after applying the activation function by \(\mathcal{N}^{a^{i}}(I)\). The values of the neurons are evaluated according to the rules:

\[\mathcal{N}^{l^{0}}(I)=I,\qquad\mathcal{N}^{l^{i}}(I)=W^{i} \mathcal{N}^{a^{i-1}}(I)+B^{i},\] \[\mathcal{N}^{a^{i}}(I)=Act^{i}(\mathcal{N}^{l^{i}}(I))\]

where \(Act^{i}\) is the activation function associated with layer \(l_{i}\).

We define the size of a neural network to be the total number of neurons in the graph (including the neurons in the input and output layers) and denote it by \(|\mathcal{N}|\). The automated training (i.e., selection of weights and biases) of neural networks is beyond our scope here; see, e.g., [22].

Fig. 1 depicts a neural network, \(\mathcal{N}_{e}\), with a single input, a single output, and 2 hidden layers with 3 neurons in each. It uses the ReLU activation function, \(ReLU(x)=\max(0,x)\). The bias of each neuron is listed above it, and weights are listed over the edges (zero values are omitted). In matrix representation, the weights and biases are:

\[W^{1}=\begin{bmatrix}-5\\ -0.5\\ -1\end{bmatrix},B^{1}=\begin{bmatrix}10\\ -2.5\\ 7\end{bmatrix},W^{2}=\begin{bmatrix}0.8&-1&-2\\ 0&0.5&0\\ 2&0.5&-1\end{bmatrix},\]

\[B^{2}=\begin{bmatrix}8\\ 2\\ 0\end{bmatrix},W^{3}=\begin{bmatrix}0.25\\ 2\\ 0.5\end{bmatrix}^{T},B^{3}=\begin{bmatrix}0\end{bmatrix}\]

\(\mathcal{N}_{e}\) is of size 8 (every \(l_{j}^{i}\) and \(r_{j}^{i}\) pair in the figure are counted as one neuron; we split them only for visualization purposes), and has 4 layers. The figure also demonstrates an evaluation of the network, for the input \(x=5\). The assignment of each node is listed below it; and we can see that the produced output in this case is \(y=5\).

**Convolutional Neural Networks.** A _convolutional neural network_ is a neural network with one or more convolutional layers (typically, these are the first layers of the network). The parameters of a convolutional layer include the height \(h\) and width \(w\) of images in the input; the kernel size \(k\); the stride size \(s\); the padding size \(p\); the input channels \(c_{i}\); the output channels \(c_{o}\); the kernel weights \(W\), given as a tensor of dimensions \((c_{o}\times c_{i}\times k\times k)\); and the biases, \(B\), organized in an array of length \(c_{o}\). We assume for simplicity that the kernel size, padding size, and stride size are equal along all axes, although this is not a limitation of our approach.

The convolutional layer filters its input, which is a \((c_{i}\times k\times k)\)-dimensional matrix, using the above parameters and outputs a multidimensional matrix which represents feature maps. For additional information on how a convolutional layer computes its output, see [22]. Note that convolutional layers are comprised strictly of linear operations.

**Neural Network Verification.** A _property_\(\mathcal{P}\) is a set of constraints on the inputs and outputs of the neural network. These constraints give rise to an input region \(I(\mathcal{P})\) and an output region \(O(\mathcal{P})\). Verifying \(\mathcal{P}\), with respect to some neural

Fig. 1: \(\mathcal{N}_{e}\) An example of a neural network with ReLU activation functions.
network, entails determining whether there exists an input in \(I(\mathcal{P})\) that the neural network maps to an output in \(O(\mathcal{P})\) (the SAT case), or not (the UNSAT case). Typically, \(\mathcal{P}\) is specified so that \(O(\mathcal{P})\) represents _undesirable_ behavior, and so an UNSAT result indicates that the system is correct. \(\mathcal{P}_{e}=(5\leq x\leq 10)\land(5\leq y\leq 10)\) is an example of a property of \(\mathcal{N}_{e}\) in Fig. 1.

A _neural network verifier_ takes in a verification query (a neural network and a property) and attempts to automatically verify it. When successful, it returns a SAT or UNSAT answer; otherwise, it can return ERROR, or TIMEOUT. When a neural network verifier returns SAT, it also returns an input that proves the satisfiability of the query. Given a verifier \(\mathcal{V}\) and a verification query \(Q=(\mathcal{N},\mathcal{P})\), we denote by \(\mathcal{V}(Q)\in\{\texttt{SAT},\texttt{UNSAT},\texttt{ERROR},\texttt{TIMEOUT}\}\) the answer of \(\mathcal{V}\) on \(Q\). If \(\mathcal{V}(Q)=\texttt{SAT}\), we denote by \(\mathcal{V}_{w}(Q)\in I(\mathcal{P})\) the satisfying assignment (the witness) returned by the verifier.

Continuing with our running example, given a sound neural network verifier \(\mathcal{V}_{e}\) and the verification query \(Q_{e}=(\mathcal{N}_{e},\mathcal{P}_{e})\), \(\mathcal{V}_{e}(Q_{e})=\texttt{SAT}\) and a valid witness is \(\left(\mathcal{V}_{e}\right)_{w}(Q_{e})=(5)\), since \(\mathcal{N}_{e}((5))=(5)\in O(\mathcal{P}_{e})\).

Neural network verification is complex, both theoretically and practically [31]; and modern tools apply sophisticated techniques to verify large networks [1]. These techniques are typically theoretically sound, but implementation bugs can cause verifiers to produce incorrect results. These bugs are easier to track and correct if the problem manifests for queries with small networks.

In a situation where two verifiers disagree on the satisfiability of a given query, at least one of them must answer SAT and provide a satisfying assignment. We evaluate the neural network on that assignment, and determine whether it indeed satisfies the property at hand. If so, we conclude that the other verifier, which returned UNSAT, is faulty; otherwise, if the satisfying assignment is incorrect, we determine that the verifier that answered SAT is faulty. The remaining verifier then takes the role of the oracle verifier.

## III DelBugV: Delta-Debugging Verification Queries

### _General Flow_

Applying _delta-debugging_ techniques means automatically simplifying an input \(x\) that triggers a bug in the system into a simpler input, \(x^{\prime}\), that also triggers a bug [41]. \(x^{\prime}\) can often trigger the bug faster, thus reducing overall debugging time; and also trigger fewer code lines that are unrelated to the bug, allowing engineers to more easily identify its root cause. In our setting, given a verification query \(Q=(\mathcal{N},\mathcal{P})\) that triggers a bug in a neural network verifier, we seek to generate another query \(Q^{\prime}=(\mathcal{N}^{\prime},\mathcal{P})\), with a much smaller (simplified) neural network: \(|\mathcal{N}^{\prime}|<|\mathcal{N}|\). The motivation for focusing on the neural network, and not on the verification conditions, is that common verification conditions are typically already quite simple [58], whereas neural network sizes have a crucial effect on verifier performance [31].

The general delta debugging framework that our tool follows appears as Alg. 1. The inputs to the process are a faulty verifier \(\mathcal{V}\), an oracle verifier \(\mathcal{V}_{O}\), and a verification query \(Q=(\mathcal{N},\mathcal{P})\). The algorithm maintains a candidate result neural network \(\mathcal{N}_{r}\) that triggers a bug in \(\mathcal{V}\) and make it produce an incorrect answer, and whose size is iteratively decreased. In each iteration, the algorithm invokes Alg. 2 to attempt simplifying \(\mathcal{N}_{r}\). The process terminates when Alg. 2 states that it cannot simplify \(\mathcal{N}_{r}\) any further, or when a timeout limit is exceeded. Finally, it returns the verification query with the smallest \(\mathcal{N}_{r}\) it achieved.

```
1:\(\mathcal{V}\), \(\mathcal{V}_{O}\), \(Q=(\mathcal{N},\mathcal{P})\) // Faulty Verifier, Oracle Verifier, Verification query
2:\(\mathcal{N}_{r}\leftarrow\mathcal{N}\)
3:progressMade \(\leftarrow\) True
4:while noTimeout() \(\land\) progressMade do
5:\(\mathcal{N}_{r}\leftarrow\mathcal{N}\)
6: progressMade, \(\mathcal{N}\leftarrow\) Simplify(\(\mathcal{V},\mathcal{V}_{O},Q\))
7:return\((\mathcal{N}_{r},\mathcal{P})\)
```

**Algorithm 1**_Reduce Verification Query_

Alg. 2 takes in the same arguments as Alg. 1, and its goal is to perform one successful simplification step on \(\mathcal{N}\), from a pool of potential steps. The algorithm heuristically chooses a sequence of simplification steps to attempt (Line 1), and then performs them, one by one, until one is successful. We propose several simplification steps in Sec. III-B. Specifying the order according to which theses simplification steps are attempted (Line 1) is key, and different strategies may result in different simplified networks -- we propose one such strategy in Sec. III-B.

```
1:\(\mathcal{V}\), \(\mathcal{V}_{O}\), \(Q=(\mathcal{N},\mathcal{P})\) // Faulty Verifier, Oracle Verifier, Verification query
2:True/False, \(Q_{r}\) // Whether the query was simplified, and the simplified query
3:Attempts = \((M_{0},M_{1},\ldots)\leftarrow\) attemptsBySimplificationStrategy(\(\mathcal{N}\))
4:while Attempts \(\neq\emptyset\)do
5:\(M_{i}\leftarrow\)Attempts.\(pop()\)
6:\(\mathcal{N}_{r}\gets M_{i}(\mathcal{N})\)
7:if successSimplification(\(\mathcal{V},\mathcal{V}_{O},(\mathcal{N}_{r},\mathcal{P})\)) then
8:return True, \(\mathcal{N}_{r}\)
9:return False, \(\mathcal{N}\)
```

**Algorithm 2**_Simplify_

Line 5 of Alg. 2 invokes Alg. 3 to check whether the simplification step attempted succeeded or not. To do so, Alg. 3 first checks whether \(\mathcal{V}\) answers SAT, but returns an incorrect counter-example. If so, this candidate should clearly be kept. Otherwise, the algorithm checks whether \(\mathcal{V}\) and \(\mathcal{V}_{O}\) both answer UNSAT or SAT, but disagree; if so, it returns
True. In all other cases, i.e. where one of the verifiers times out, or when there is no basis for comparison (one of the verifiers returned an error), the algorithm returns False, and an alternative simplification step in Alg. 2 is attempted.

```
1:\(\mathcal{V}\), \(\mathcal{V}_{O}\), \(Q=(\mathcal{N},\mathcal{P})\)// Faulty Verifier, Oracle Verifier, Verification query
2:True/False // Was the query successfully simplified?
3:if\(\mathcal{V}(\mathcal{N},\mathcal{P})=\textsc{SAT}\wedge\mathcal{V}_{W}(Q) \notin I(\mathcal{P})\)then
4:return True
5:if\(\mathcal{V}(\mathcal{N},\mathcal{P})=\textsc{SAT}\wedge\mathcal{N}(\mathcal{V}_{W} (Q))\notin O(\mathcal{P})\)then
6:return True
7:if\(\mathcal{V}(\mathcal{N},\mathcal{P}),\mathcal{V}_{O}(\mathcal{N},\mathcal{P}) \in\{\textsc{SAT},\textsc{UNSAT}\}\)\(\wedge\)\(\mathcal{V}(\mathcal{N},\mathcal{P})\neq\mathcal{V}_{O}(\mathcal{N},\mathcal{P})\)then
8:return True
9:return False
```

**Algorithm 3**_successSimplification_

One possible risk when using Alg. 1 is a "flip" between the two verifiers. This can happen when initially, \(\mathcal{V}_{O}\) produces a correct answer and \(\mathcal{V}\) does not; but after a simplification step, \(\mathcal{V}\) starts producing the correct answer and \(\mathcal{V}_{O}\) starts producing an incorrect answer. This situation is unlikely: the simplification steps we propose later make local modifications to the network, and are consequently far more likely to continue to trigger the same bug in \(\mathcal{V}\) than to trigger a new one in \(\mathcal{V}_{O}\). Still, this concern can be mitigated even further by using multiple oracle verifiers, and ensuring that they all agree amongst themselves while \(\mathcal{V}\) dissents.

**Single Verifier Mode.** Our approach could also be applied to delta-debug a single verifier that returns incorrect satisfying assignments, without using an oracle. As we explain in Sec. III-B, the simplification methods we apply require the returned satisfying assignment from either the faulty or the oracle verifier, thus, if the faulty verifier returns an incorrect satisfying assignment for the query at hand, we can drop the oracle verifier. This is achieved by removing the last "if" condition from Alg. 3 and removing the oracle verifier \(\mathcal{V}_{O}\) from the inputs.

### _Simplification Methods_

A core component of Alg. 1 is the selection of simplification strategy to apply (Line 1 in Alg. 2). We now describe our pool of neural network simplification methods, and the strategy that we suggest for selecting among them. The goal of all the simplification methods we propose here is to reduce neural network sizes, while keeping the network's behavior (i.e., its outputs) similar to that of the original; especially on the counter-example provided by either the faulty verifier or the oracle verifier. Note that a single simplification method can often be applied multiple times, in different ways, using different input parameters.

**Method 1: linearizing piecewise-linear activation functions between fully-connected layers.** In general, the presence of activation functions is a major source of complexity in the verification process of neural networks: they render the problem NP-complete, require complex mechanisms for linearly approximating them, and often entail case-splitting that slows down the verifiers [31, 40, 59]. Thus, in order to simplify the neural network, we propose to eliminate such activation functions, by _fixing them to a single linear segment_, effectively replacing them with linear constraints. This procedure is performed on an entire layer at a time; which, in turn, creates a sequence of consecutive purely linear layers that can then be merged into a single linear layer, reducing the overall number of layers and neurons in the network.

In choosing the linear segment to which each function is fixed, we propose to use the counter-example \(I\) provided by either the faulty verifier or the oracle verifier. The output of the new linear segment we choose, with respect to \(I\), will match the output of the activation function on \(I\).

For simplicity, we focus here on the ReLU activation function (\(ReLU(x)=\max\left(x,0\right)\)), although the technique is applicable to any piecewise-linear function. Intuitively, in such cases we propose to replace _active_ ReLUs (\(x\geq 0\)) by the identify function, and _inactive_ ReLUs (\(x<0\)) by zero. More formally, observe two consecutive layers, \(l^{t}\) and \(l^{t+1}\), in the neural network \(\mathcal{N}\), where layer \(l^{t}\) has a ReLU activation function. We construct an alternative layer, \(l^{a}\), to replace both \(l^{t}\) and \(l^{t+1}\). \(l^{a}\) inherits the activation function of \(l^{t+1}\). The weights \(W^{a}\) and the biases \(B^{a}\) of \(l^{a}\) are calculated as:

\[W^{a} =W^{t+1}W^{\prime}W^{t}\] \[B^{a} =W^{t+1}W^{\prime}B^{t}+B^{t+1}\]

where

\[W^{\prime}_{i,j}=\begin{cases}1&i=j\wedge\left(N_{Q}^{l^{t}}(I)\right)_{i}\geq 0 \\ 0&\text{otherwise}\end{cases}\]

Here \(W^{\prime}\) is the new linear segment replacing the activation function ReLU. Finally, the obtained simplified network \(\mathcal{N}_{r}\) is the network \(\mathcal{N}\) where layers \(l^{t}\) and \(l^{t+1}\) are deleted and replaced with \(l^{a}\).

Fig. 2 depicts the result of applying this method on layers \(l^{2}\) and \(l^{3}\) from Fig. 1, using the assignment \(I_{e}=(5)\). Fig. 1(a) depicts the layers selected for merging; and Fig. 1(b) depicts the resulting neural network. Notice that \(\mathcal{N}_{e}^{l^{2}}(I_{e})=(4,2,-2)\), meaning that only the ReLUs in neurons \(l^{2}_{0}\) and \(l^{2}_{1}\) are active. Thus, these ReLUs are replaced by the identity function, whereas the inactive ReLU of \(l^{2}_{2}\) is replaced by \(0\). After this step, layers \(l^{2}\) and \(l^{3}\) perform only linear operations, and are merged into a single layer.

**Method 2: linearizing piecewise-linear activation functions between convolutional layers.** In this method, a convolutional layer is combined with the layer following it (either a fully connected layer or a convolutional one), and replaced by a single, fully connected layer.

For simplicity, we focus here on the case where the second layer is fully connected. More formally, observe two consecutive layers, \(l^{t}\) and \(l^{t+1}\) in \(\mathcal{N}\), where \(l^{t}\) is a convolutional layer
and \(l^{t+1}\) is a fully connected layer. Our goal is to construct an alternative layer, \(l^{a}\), that will replace \(l^{t}\) and \(l^{t+1}\). Since a convolutional layer is a particular case of fully connected layer, we construct \(l^{a}\) by first converting the convolutional layer \(l^{t}\) into a fully connected one, denoted \(l^{c}\); then linearizing the activation functions, as in _Method 1_; and finally, combining the two layers into one.

Denote by \(W^{t}\) and \(W^{t+1}\) the matrices representing the weights of layer \(l^{t}\) and \(l^{t+1}\) respectively, and by \(B^{t}\) and \(B^{t+1}\) the vectors representing their respective biases. To transform a convolutional layer into a fully connecting one, we calculate the weights, \(W^{c}\), and the biases, \(B^{c}\), of the fully connected layer replacing the convolutional one, according to the conventional layer parameters. First, we turn its input and output from a multidimensional tensors into 1-dimensional vectors. The height and width (dimensions) of the feature maps in the convolutional layer's output are: \(h_{o},w_{o}\) where

\[h_{o}=\left\lfloor\frac{h+2p-k}{s}\right\rfloor+1,\quad w_{o}=\left\lfloor \frac{w+2p-k}{s}\right\rfloor+1.\]

The convolutional layer's output contains \(c_{o}\) feature maps, i.e., the dimensions of the output are \((c_{o}\times h_{o}\times w_{o})\). Thus, the dimensions of \(W^{c}\) are \((c_{o}h_{o}w_{o}\times c_{i}hw)\). \(W^{c}\) is a sparse matrix. To calculate the value of the \(i,j\)-th entry in \(W^{c}\), we first compute the following values:

\[c_{i}^{\prime} =\left\lfloor\frac{j}{hw}\right\rfloor,\quad c_{o}^{\prime}= \left\lfloor\frac{i}{h_{o}w_{o}}\right\rfloor,\] \[i^{\prime} =\left\lfloor\frac{i-c_{i}hw}{w}\right\rfloor-\left(\left\lfloor \frac{j-c_{o}h_{o}w_{o}}{w_{o}}\right\rfloor\cdot s-p\right)\] \[j^{\prime} =\left((i-c_{i}hw)\bmod w\right)-\left(((j-c_{o}h_{o}w_{o}) \bmod w_{o})\cdot s-p\right)\]

\(c_{i}^{\prime}\) and \(c_{o}^{\prime}\) are the input and output channels that the \(i,j\)-th entry should be associated with. \(i^{\prime}\) and \(j^{\prime}\) are the indices in the kernel that should match to the \(i,j\)-th entry. The weight matrix \(W^{c}\) is given by:

\[W^{c}_{i,j}=\begin{cases}W^{t}_{c_{i}^{\prime},c_{i}^{\prime},j^{\prime}}&0 \leq i^{\prime}\wedge j^{\prime}<k\\ W^{c}_{i,j}=0&\text{otherwise}\end{cases}\]

Finally,

\[B^{c}_{i}=B^{t}_{\left\lfloor\frac{i}{h_{o}w_{o}}\right\rfloor}\]

According to this construction of \(W^{c}\) and \(B^{c}\), they will have the same functionality as the convolutional operation they replace. This step may temporarily increase the number of edges in the network (but not the number of neurons). This is required to prepare for the minimization step.

The next step is to linearize the ReLU. This is done in a similar manner to the linearization in the previous method, from which we get \(W^{\prime}\). Next, we construct the weights \(W^{a}\) and the biases \(B^{a}\) of the alternative layer \(l^{a}\):

\[W^{a}= W^{t+1}W^{\prime}W^{c}\] \[B^{a}= W^{t+1}W^{\prime}B^{c}+B^{t+1}\]

And the activation function assigned to the new layer \(l_{a}\) is the same as the one assigned to layer \(l_{t+1}\). Finally, the simplified neural network \(\mathcal{N}_{r}\) is the network \(\mathcal{N}\), where layers \(l_{t}\) and \(l_{t+1}\) are deleted and replaced with \(l_{a}\).

In case \(l^{t+1}\) is also a convolutional layer, we convert it to a fully connected layer, as we did with \(l^{t}\); and the remainder of the process is unchanged.

**Method 3: merging neurons.** In this method, we seek to merge a pair of neurons in the same layer into a single neuron, thus decreasing the neural network size by one. Of course, this entails selecting the weights of this new neuron's incoming and outgoing edges, as well as its bias. Our motivation is to cause the merged neuron to produce values close to those of the original neurons, and consequently cause little changes in the neural network's eventual output. We present first the technical process of merging neurons, and later discuss _which_ pairs of neurons should be merged.

We focus again on the case where the activation function is ReLU. We first use the counter-example \(I\) (returned by either the faulty verifier or the oracle verifier) to check whether the activation functions of the neurons being merged have the same phase -- i.e., if they are both active, or both inactive. If they have the same phase, we compute the merged neuron's weights and biases using the original neurons' weights and

Fig. 2: \(\mathcal{N}_{e}\) with layers \(l^{2}\) and \(l^{3}\) selected in orange (a), and then merged (b).
biases. Specifically, the weight of each edge incoming to the merged neuron is the mean of the original incoming edge weights, and the neuron's bias is the mean of the original neurons' biases; whereas the weights of its outgoing edges are the weighted sum, according to \(I\), of the original outgoing edge weights (a weighted sum is needed, instead of a simple sum, to ensure that the neurons in the following layer obtain values similar to their original ones with respect to \(I\)). In case one of the neurons is active and the other is inactive, we simply delete the inactive one, since it does not contribute to the following layer's neuron values (with respect to \(I\)).

Formally, given a neural network, \(\mathcal{N}\), two successive layers in it, \(l^{t}\) and \(l^{t+1}\), and two neurons indices \(b<c\), we construct two alternative layers \(l^{a}\) and \(l^{a+1}\) that will replace \(l^{t}\) and \(l^{t+1}\) respectively. Additionally, \(l^{a}\) and \(l^{a+1}\) inherit the activation functions of \(l^{t}\) and \(l^{t+1}\) respectively. If the ReLUs of the neurons \(b\) and \(c\) in layer \(l^{t}\) have the same phases: \(\left(\mathcal{N}^{l^{t}}(I)\right)_{b},\left(\mathcal{N}^{l^{t}}(I)\right) _{c}>0\) or \(\left(\mathcal{N}^{l^{t}}(I)\right)_{b},\left(\mathcal{N}^{l^{t}}(I)\right) _{c}<0\), the weights and the biases \(W^{a},W^{a+1},B^{a},B^{a+1}\) of the alternative layers are calculated as follows:

\[B^{a}_{i} =\begin{cases}B^{t}_{i}&i<b\lor b<i<c\\ \frac{B^{t}_{i}+B^{t}_{i}}{2}&i=b\\ B^{t}_{i+1}&c\leq i\end{cases}\] \[B^{a+1} =B^{t+1}\] \[W^{a}_{i,j} =\begin{cases}W^{t}_{i,j}&i<b\lor b<i<c\\ \frac{W^{t}_{i,j}+W^{t}_{c,i}}{2}&i=b\\ W^{t}_{i+1,j}&c\leq i\end{cases}\] \[W^{a+1}_{i,j} =\begin{cases}W^{t+1}_{i,j}&j<b\lor b<j<c\\ \frac{2\cdot\left(W^{t+1}_{i,k}\left(\mathcal{N}^{l^{t+1}}(I)\right)_{b}+W^{t +1}_{i,c}\left(\mathcal{N}^{l^{t+1}}(I)\right)_{c}\right)}{\left(\mathcal{N}^ {l^{t+1}}(I)\right)_{b}+\left(\mathcal{N}^{l^{t+1}}(I)\right)_{c}}&j=b\\ W^{t+1}_{i,j+1}&c\leq j\end{cases}\]

Otherwise, if the ReLUs of the neurons \(b\) and \(c\) in layer \(l^{t}\) have different phases: \(\left(\mathcal{N}^{l^{t}}(I)\right)_{b}>0\wedge\left(\mathcal{N}^{l^{t}}(I) \right)_{c}<0\) (assume w.l.o.g. that the \(c\)-th neuron is the inactive one), the weights and biases \(W^{a},W^{a+1},B^{a},B^{a+1}\) of the alternative layers are calculated as follows:

\[B^{a}_{i} =\begin{cases}B^{t}_{i}&i<c\\ B^{t}_{i+1}&c\leq i\end{cases},\qquad B^{a+1}=B^{t+1}\] \[W^{a}_{i,j} =\begin{cases}W^{t}_{i,j}&i<c\\ W^{t}_{i+1,j}&c\leq i\end{cases},\quad W^{a+1}_{i,j}=\begin{cases}W^{t+1}_{i,j} &j<c\\ W^{t+1}_{i,j+1}&c\leq j\end{cases}\]

Finally, the obtained simplified neural network \(\mathcal{N}_{r}\), is the network \(\mathcal{N}\) where layers \(l^{t}\) and \(l^{t+1}\) are replaced with \(l^{a}\) and \(l^{a+1}\) respectively. This method can be applied repeatedly, to reduce the network size even further.

An example of applying this method on the pair of neurons \(l^{2}_{0}\) and \(l^{2}_{1}\) in \(\mathcal{N}_{e}\) from Fig. 1 using the assignment \(I_{e}=(5)\) appears in Fig. 3. Fig. (a)a shows the neurons selected for merging, and Fig. (b)b shows the result of the merge.

Choosing which pair of neurons to merge is crucial for the success of this method. Every two neurons in the same layer are valid candidates; however, some pairs are more likely to succeed than others by resulting in a simplified neural network that behaves similarly to the original. We consider the following possible approaches for prioritizing between the pairs: (1) an arbitrary ordering; (2) prioritizing pairs with neurons that are assigned similar values (prior to the activation function), when the network is evaluated on assignment \(I\). The motivation is that merging such pairs is expected to have smaller effect on the overall functionality of the neural network; (3) prioritizing pairs of neurons whose ReLUs are inactive when evaluated on \(I\). The motivation is that inactive neurons may have little effect on the bug at hand. This approach can be combined with Approach 2 to prioritize pairs with similar values after categorizing them by the status of the ReLUs; (4) prioritizing pairs of neurons with positive values with respect to \(I\). This approach, too, can be combined with Approach 2; and (5) prioritizing pairs of neurons with negative values, and then pairs with positive values, with respect to \(I\). This approach is a combination of Approaches 3 and 4, and again uses Approach 2 for internal prioritization within each category.

**Strategy for applying the simplification rules.** Within Alg. 1, the simplification steps mentioned above can be invoked in any order. We propose to attempt methods that significantly reduce the neural network size first, in order to reduce verification times. We empirically observed that this is achieved by the following strategy: first, attempt to linearize and merge con

Fig. 3: \(\mathcal{N}_{e}\) with neurons \(l^{2}_{0}\) and \(l^{2}_{1}\) selected in orange (a), and then merged (b).
volutional layers (_Method 2_). Second, attempt to linearize and merge fully connected layers (_Method 1_) -- starting with the output layer, and working backwards towards the input layer. Finally, merge neurons (_Method 3_) according to Approach 5. However, our implementation is highly customizable, and users can configure it to use any other strategy, according to the task at hand.

To illustrate, applying our proposed strategy to \(\mathcal{N}_{e}\) from Fig. 1, with respect to the assignment \(I_{e}=(5)\) in which \(\mathcal{N}_{e}^{l^{2}}(I_{e})=(-15,-5,2)\) and \(\mathcal{N}_{e}^{l^{2}}(I_{e})=(4,2,-2)\), would result in attempting the simplification methods in the following order: (1) merge the layers \(l^{2}\) and \(l^{3}\); (2) merge the layers \(l^{1}\) and \(l^{2}\); (3) merge the pair of neurons \(l^{1}_{0},l^{1}_{1}\); (4) merge the pair of neurons \(l^{2}_{1},l^{2}_{2}\); (5) merge the pair of neurons \(l^{2}_{0},l^{2}_{2}\); (6) merge the pair of neurons \(l^{1}_{1},l^{1}_{2}\); and then, (7) merge the pair of neurons \(l^{1}_{0},l^{1}_{2}\). These steps are attempted, in order, until one succeeds; after which the strategy is reapplied to the simplified network, and so on.

## IV Implementation and Evaluation

We designed our tool, DelBugV, to be compatible with the standard input format used in the VNN-COMP competition [10], in which verification queries are encoded using the _VNN-LIB_ format [12]; and which, in turn, relies on the _Open Neural Network Exchange_ (_ONNX_) format. This facilitated integrating DelBugV with the various verifiers. DelBugV is implemented in Python, and contains classes that wrap objects of these formats. The tool has a modular design that allows applying our proposed minimization methods in any order desired.

VNN-COMP'21 included 12 participating neural network verifiers, and these were tested on a set of verification queries. We began by extracting from the VNN-COMP'21 results pairs of dissenting verifiers, and the verification queries that triggered these discrepancies. Each such triple (two verifiers and a query) constitutes an input to DelBugV. This extraction led us to target the following verifiers: (1) Marabou [33]; (2) NNV [52, 53, 54, 55, 63]; (3) NeuralVerification.jl (NVjl) [37]; and (4) nenum [8, 9, 52, 53]. In the experiments described next, we used the same versions of these verifiers that were used in VNN-COMP'21.

**Neuron Merging and Prioritization Approaches.** For our first experiment, we set out to determine which of the neuron-pair prioritization schemes described as part of _Method 3_ in Sec. III-B is the most successful. We measured success along two parameters: the size of the simplified network obtained, and by the percentage of successful merging steps along the way. We tested our algorithm on 5 input triples, involving networks of size 310 each. Using only _Method 3_, we ran DelBugV with each of the prioritization schemes, and counted for each, the number of merging steps performed and the number of the steps that succeeded. Table. I shows the results of this comparison: the second column indicates, for every approach, the percentage of the successful steps out of all the steps tried, aggregated for all 5 benchmarks.

Looking at the average reduction sizes, the results indicate that all 5 approaches were able to achieve a similar reduction in size, with a slight advantage to approaches 1, 3 and 5. However, the number of successful merges varied significantly -- from Approach 1, in which only 37.2% of the merge steps were successful, and up to 75.9% for Approach 5 (in bold). These results thus indicate that Approach 5 is the most efficient of the 5, and so we used it as our default strategy for Method 3 in the subsequent experiments.

**Linearizing ReLU Activations.** In _Method 1_ and _Method 2_ in Sec. III-B, we proposed to linearize activation functions, and then merge them with the previous and following layers. These methods can be applied to any piecewise-linear activation function in the network. The order in which they are applied is customizable. In this experiment, we set out to compare linearizing ReLUs in ascending order (from input layer towards output layer), and in descending order (from output towards input). Table II shows the results of this experiment.

Every row in the table corresponds to an input triple to DelBugV (two disagreeing verifiers and a verification query that they disagreed on), and the two simplification approaches that were attempted. For each such experiment, the second column indicates the number of simplification steps tried, until DelBugV reached saturation (there were no additional steps to try). The third column indicates the number of the successful steps out of all the steps. In column four, the percentage successful steps out of all steps is shown; and the final column shows the reduction percentage in the neural network size. When one of the approaches was clearly superior, the entry appears in bold.

To analyze the results, observe, e.g., the 5th experiment in Table II. The results imply that when using the ascending approach, 12 linearizing and merging steps were made, until the network count not be simplified further with either _Method 1_ or _Method 2_. Of these 12 steps, 5 were successful -- and consequently, the simplified network has 5 fewer layers than the original. In contrast, with the descending approach only 9 steps were made until the network could not be simplified further, 6 of which were successful. Consequently, the simplified network in this case has 6 fewer layers compared to the original.

The results indicate that linearizing in descending order slightly outperforms linearizing in ascending order, although the gap is not very significant. The neural network in the last row included a convolutional layer, and, according to the results, linearizing it in ascending order preformed better.

\begin{table}
\begin{tabular}{|l||c|c|} \hline \hline  & Successful merges (\%) & Average Reduction (\%) \\ \hline \hline Approach 1 & 37.2\% & 96.0\% \\ Approach 2 & 68.4\% & 95.9\% \\ Approach 3 & 71.6\% & 96.0\% \\ Approach 4 & 62.9\% & 95.8\% \\ Approach 5 & **75.9\%** & 96.0\% \\ \hline \hline \end{tabular}
\end{table} TABLE I: Comparing neurons merging approaches (Method 3) by size reduction and successful merges.
After investigating this query further, we noticed that in the ascending order approach, the convolutional layer was merged into a fully connected one; whereas the descending approach did not succeed in removing or merging any convolutional layers. We thus conclude that, for a convolutional network, it is advisable to apply _Method 2_ before applying _Method 1_.

**Delta Debugging Discrepancies from VNN-COMP'21.** For our final experiment, we considered 13 triples of verifiers, oracle verifiers, and verification queries. Of these triples, 11 contained DNNs from the ACAS-Xu family [31], 1 was a DNN from the MNIST DNNs [36], and 1 was a DNN from the Oval21 benchmark [10]. Using the optimal configuration of our tool as previously discussed, we applied the full-blown delta-debugging algorithm to all of our 13 benchmarks. The results appear in Table. III. Every row in the table represents a triple, and the first two columns indicate the number of neurons in the original network, and the number of remaining neurons after delta debugging was applied. The next two columns indicate the number of layers in the original and reduced networks; and the final column indicates the percent of neurons that were removed.

Overall, the algorithm performed exceedingly well, reducing the network sizes by an average of 96.8% (!); and, in some cases, causing a size decrease of 99%, from a neural network with 1306 neurons and 4 layers to just 11 neurons and 2 layers (an input layer and an output layer, without any activation functions). The minimal decrease observed was 95%, from 310 neurons to 13. We regard these results as a very strong indication of the usefulness of delta debugging in the context of DNN verification. Further analyzing the results, we observe that the ReLU linearization simplification rule was responsible for an average of 66% of the size reduction, whereas the remaining two rules were responsible for an average of 34% -- indicating that the ReLU linearization simplification rule is the main workhorse of our approach at its current configuration.

## V Related Work

With the increasing pervasiveness of DNNs, the verification community has been devoting growing efforts to verifying them. Numerous approaches have been proposed, including SMT-based approaches [24, 31, 32, 33, 50, 60], approaches based on LP or MILP solvers [15, 17, 51], reachability-based approaches [39, 63], abstraction and abstract-interpretation based approaches [6, 19, 25, 28, 40, 46, 48, 59], synthesis-based approaches [34, 44], run-time optimization [5, 7], quantitative verification [11], verification of recurrent networks [29, 65], and many others. These approaches, in turn, have been used in numerous application domains [16, 18, 21, 49, 56, 57, 64]. Given the scope of these efforts, and the number of available tools, it is not surprising that bugs are abundant, and that engineers are in need of efficient debugging tools.

To the best of our knowledge, no previous work has applied delta debugging in the context of DNN verification, although similar approaches have been shown successful in the related domains of SMT [41, 13] and SAT [14] solving. Related efforts have attempted to reduce DNN sizes, with the purpose of producing smaller-but-equivalent networks, or networks smaller with a respect to a particular verification property of interest [6, 35, 45, 46]. In the future, principles from these approaches could be integrated as simplification strategies within our delta-debugging approach.

## VI Conclusion

In this paper, we presented the DelBugV tool for automatically reducing the size of a verification query with respect to an erroneous neural network verifier. We focused on delta-debugging techniques, and proposed multiple minimization methods for reducing neural network sizes. These techniques attempt to simplify the neural network in question, while modifying it as little as possible. We also suggested a strategy for the order in which to apply those methods. We demonstrated the effectiveness of DelBugV on actual benchmarks from the VNN-COMP'21 competition, and were able to significantly simplify them. We regard this work as another step towards more sound tools for DNN verification.

**Acknowledgements.** This work was partially supported by the Israel Science Foundation (grant number 683/18).

\begin{table}
\begin{tabular}{|c|c|c|c|c|c|} \hline \multirow{2}{*}{\begin{tabular}{c} Linearing \\ approach \\ \end{tabular} } & No. of & \multirow{2}{*}{\begin{tabular}{c} No. of \\ successful \\ steps \\ \end{tabular} } & \multirow{2}{*}{\begin{tabular}{c} Successful \\ steps \% \\ \end{tabular} } & \multirow{2}{*}{
\begin{tabular}{c} Neuron \\ reduction \% \\ \end{tabular} } \\ \hline \multirow{2}{*}{1.} & Ascending & 6 & 6 & 100.0\% & 96.7\% \\  & Descending & 6 & 6 & 100.0\% & 96.7\% \\ \hline \multirow{2}{*}{2.} & Ascending & 6 & 6 & 100.0\% & 96.7\% \\  & Descending & 6 & 6 & 100.0\% & 96.7\% \\ \hline \multirow{2}{*}{3.} & Ascending & 6 & 6 & 100.0\% & 96.7\% \\  & Descending & 6 & 6 & 100.0\% & 96.7\% \\ \hline \multirow{2}{*}{4.} & Ascending & 6 & 0 & 0.0\% & 0.0\% \\  & Descending & 6 & 0 & 0.0\% & 0.0\% \\ \hline \multirow{2}{*}{5.} & Ascending & 12 & 5 & 41.6\% & 80.6\% \\  & Descending & 9 & 6 & **66.6\%** & **96.7\%** \\ \hline \multirow{2}{*}{6.} & Ascending & 3 & 2 & 66.6\% & 39.2\% \\  & Descending & 2 & 2 & **100.0\%** & 39.2\% \\ \hline \multirow{2}{*}{7.} & Ascending & 3* & 2* & **66.6\%** & **65.8\%** \\  & Descending & 2* & 1 & 50.0\% & 0.0\% \\ \hline \end{tabular}
\end{table} TABLE II: Comparing linearizing layers approaches by successful steps. * indicates the existence of a convolutional layer.

\begin{table}
\begin{tabular}{|c|c||c|c||c|} \hline \multicolumn{2}{|c||}{Neurons} & \multicolumn{2}{c||}{Layers} & \multicolumn{1}{c|}{Reduction} \\ \hline In Original & In reduced & In original & In reduced & percentage \\ \hline \hline
310 & 6 & 8 & 2 & 98\% \\
310 & 7 & 8 & 2 & 97\% \\
310 & 6 & 8 & 2 & 98\% \\
310 & 12 & 8 & 8 & 96\% \\
310 & 6 & 8 & 2 & 98\% \\
9326 & 12 & 5* & 3 & 99\% \\
1306 & 11 & 4 & 2 & 99\% \\
310 & 10 & 8 & 3 & 96\% \\
310 & 6 & 8 & 2 & 98\% \\
310 & 10 & 8 & 4 & 96\% \\
310 & 9 & 8 & 4 & 97\% \\
310 & 13 & 8 & 6 & 95\% \\ \hline \end{tabular}
\end{table} TABLE III: Delta-debugging using our algorithm. * indicates the existence of a convolutional layer.