Model-Agnostic Reachability Analysis on Deep Neural Networks
Verification plays an essential role in the formal analysis of
safety-critical systems. Most current verification methods have specific
requirements when working on Deep Neural Networks (DNNs). They either target
one particular network category, e.g., Feedforward Neural Networks (FNNs), or
networks with specific activation functions, e.g., RdLU. In this paper, we
develop a model-agnostic verification framework, called DeepAgn, and show that
it can be applied to FNNs, Recurrent Neural Networks (RNNs), or a mixture of
both. Under the assumption of Lipschitz continuity, DeepAgn analyses the
reachability of DNNs based on a novel optimisation scheme with a global
convergence guarantee. It does not require access to the network's internal
structures, such as layers and parameters. Through reachability analysis,
DeepAgn can tackle several well-known robustness problems, including computing
the maximum safe radius for a given input, and generating the ground-truth
adversarial examples. We also empirically demonstrate DeepAgn's superior
capability and efficiency in handling a broader class of deep neural networks,
including both FNNs, and RNNs with very deep layers and millions of neurons,
than other state-of-the-art verification approaches.
Chi Zhang, Wenjie Ruan, Fu Wang, Peipei Xu, Geyong Min, Xiaowei Huang
# Model-Agnostic Reachability Analysis on Deep Neural Networks

###### Abstract

Verification plays an essential role in the formal analysis of safety-critical systems. Most current verification methods have specific requirements when working on Deep Neural Networks (DNNs). They either target one particular network category, e.g., Feedforward Neural Networks (FNNs), or networks with specific activation functions, e.g., ReLU. In this paper, we develop a model-agnostic verification framework, called DeepAgn, and show that it can be applied to FNNs, Recurrent Neural Networks (RNNs), or a mixture of both. Under the assumption of Lipschitz continuity, DeepAgn analyses the reachability of DNNs based on a novel optimisation scheme with a global convergence guarantee. It does not require access to the network's internal structures, such as layers and parameters. Through reachability analysis, DeepAgn can tackle several well-known robustness problems, including computing the maximum safe radius for a given input, and generating the ground-truth adversarial example. We also empirically demonstrate DeepAgn's superior capability and efficiency in handling a broader class of deep neural networks, including both FNNs and RNNs with very deep layers and millions of neurons, than other state-of-the-art verification approaches. Our tool is available at [https://github.com/TrustAI/DeepAgn](https://github.com/TrustAI/DeepAgn)

Keywords:Verification Deep Learning Model-agnostic Reachability

## 1 Introduction

DNNs, or systems with neural network components, are widely applied in many applications such as image processing, speech recognition, and medical diagnosis [10]. However, DNNs are vulnerable to adversarial examples [25][12][33]. It is vital to analyse the safety and robustness of DNNs before deploying them in practice, particularly in safety-critical applications.

The research on evaluating the robustness of DNNs mainly falls into two categories: falsification-based and verification-based approaches. While falsification approaches (e.g. adversarial attacks) [11]can effectively find adversarial examples, they cannot provide theoretical guarantees. Verification techniques, on the other hand, can rigorously prove the robustness of deep learning systems with
guarantees [18, 19, 12, 13, 24]. Some researchers propose to reduce the safety verification problems to constraint satisfaction problems that can be tackled by constraint solvers such as Mixed-Integer Linear Programming (MILP) [1],Boolean Satisfiability (SAT) [20], or Satisfiability Modulo Theories (SMT) [15]. Another popular technique is to apply search algorithms [13] or Monte Carlo tree search [32] over discretised vector spaces on the inputs of DNNs. To improve the efficiency, these methods can also be combined with a heuristic searching strategy to search for a counter-example or an activation pattern that satisfies certain constraints, such as SHERLOCK [4] and Reluplex [15]. Nevertheless, the study subjects of these verification methods are restricted. They either target specific layers (e.g., fully-connected or convolutional layers), have restrictions on activation functions (e.g., ReLU activation only), or are only workable on a specific neural network structure (e.g., feedforward neural networks). Particularly, in comparison to FNNs, verification on RNNs is still in its infancy, with only a handful of representative works available, including [16, 14, 34]. The adoption of [16] requires short input sequences, and [14, 34] can result in irresolvable over-approximation error.

This paper proposes a novel model-agnostic solution for safety verification on both feedforward and recurrent neural networks without suffering from the above weaknesses. Figure 1 outlines the working principle of DeepAgn, demonstrating its safety evaluation process and the calculation of the maximum safety radius. To the best of our knowledge, DeepAgn is one of the pioneering attempts on _model-agnostic_ verification that can work on both modern feedforward and recurrent neural networks under a unified framework. DeepAgn can deal with DNNs with very deep layers, a large number of neurons, and any type of activation function, via a black-box manner (without access to the internal structures/parameters of the network). Our contributions are summarised below:

* To theoretically justify the applicability of DeepAgn, we prove that recurrent neural networks are also Lipschitz continuous for bounded inputs.

Figure 1: Illustration of DeepAgn working on a black-box three-output neural network. _In reachability problem, given a set of inputs (quantified by a predefined \(L_{p}\)-norm ball) and a well-trained black-box neural network, DeepAgn can calculate the output range, namely, the minimal and maximum output confidence of each label (i.e., \([y_{1min},y_{1max}]\), \([y_{2min},y_{2max}]\), and \([y_{3min},y_{3max}]\)). For the safety verification problem, we can use a binary search upon the reachability to find the maximum safe radius \(r_{max}\) where the confidence intervals of the original label \(y_{1}\) and target label \(y_{2}\) meet._
* We develop an efficient method for reachability analysis on DNNs. We demonstrate that this _generic_ and _unified_ model-agnostic verification framework can work on FNNs, RNNs, and a hybrid of both. DeepAgn is an anytime algorithm, i.e., it can return both intermediate lower and upper bounds that are gradually, but strictly, improved as the computation proceeds; and it has provable guarantees, i.e., both the bounds can converge to the optimal value within an arbitrarily small error with provable guarantees.
* Our experiments demonstrate that DeepAgn outperforms the state-of-the-art verification tools in terms of both accuracy and efficiency when dealing with complex, large and hybrid deep learning models.

## 2 Related Work

Adversarial AttacksAttacks apply heuristic search algorithms to find adversarial examples. Attacking methods are mainly guided by the forward or cost gradient of the target DNNs. Major approaches include L-BFGS [25], FGSM [11], Carlini & Wagner attack [2], Universal Adversarial Attack [36], etc. Adversarial attacks for FNNs can be applied to cultivate adversarial examples for RNNs with proper adjustments. The concepts of adversarial example and adversarial sequence for RNNs are introduced in [22], in which they concrete adversarial examples for Long Short Term Memory (LSTM) networks. Based on the C&W attack [2], attacks are implemented against DeepSpeech in [3]. The method in [9] is the first approach to analyse and perturb the raw waveform of audio directly.

Verification on DNNsThe recent advances of DNN verification include a layer-by-layer exhaustive search approach [13], methods using constraint solvers [23][15], global optimisation approaches [24][27], and the abstract interpretation approach [6][17]. The properties studied include robustness [13, 15, 35], or reachability [24], i.e., whether a given output is possible from properties expressible with SMT constraints, or a given output is reachable from a given subspace of inputs. Verification approaches aim to not only find adversarial examples but also provide guarantees on the results obtained. However, efficient verification on large-scale deep neural networks is still an _open problem_. Constraint-based approaches such as Reluplex can only work with a neural network with a few hundred hidden neurons [23, 15]. Exhaustive search suffers from the state-space

\begin{table}
\begin{tabular}{l|l c c c c c} \hline \hline  & **Guarantees** & **Core Techniques** & **Neural Network Types** & \begin{tabular}{c} **Model** \\ **Agnostic** \\ \end{tabular} & \begin{tabular}{c} **Exnet** \\ **Computation** \\ \end{tabular} & 
\begin{tabular}{c} **Model Access** \\ **Model parameters** \\ \end{tabular} \\ \hline
**Reluplex**[15] & Deterministic & SMT + LP & Relu-based FNNs & ✗ & ✓ & Model parameters \\ \hline
**Planet**[5] & Deterministic & SMT + LP & ReLU-based FNNs & ✗ & ✓ & Model parameters \\ \hline
**Alg**[2] & Upper bound & Alternate interpretation & ReLU-based FNNs & ✗ & ✗ & Model parameters \\ \hline
**CombComb**[31] & Upper bound & Convex evaluation & ReLU-based FNNs & ✗ & ✗ & Model parameters \\ \hline
**DeepGO**[24] & Converging bound & Lipschitz Optimization & FNNs with Lipschitz continuous & ✗ & ✓ & Confidence values \\ \hline
**PustLip**[29] & Upper bound & Lipschitz estimation & ReLU-based FNNs & ✗ & ✗ & Model parameters \\ \hline
**DeepGams**[23] & Approximated & Search based & ReLU/Tan/Sigmoid based FNNs & ✗ & ✓ & Confidence values \\  & converting bound & & & & & \\ \hline
**PopPopQRN**[16] & Upper bound & Unrolling & RNNs, LSTMs, CRUs & ✗ & ✗ & Model parameters \\ \hline
**RunVerity**[14] & Upper bound & Invariant Inference & RNNs & ✗ & ✗ & Model parameters \\ \hline
**VERRNN**[34] & Upper bound & Unrolling-MLP & RNNs & ✗ & ✗ & Model parameters \\ \hline
**DeepAgn** & Converging bound & Lipschitz Optimization & FNNs (CNN), RNNs, Hybrid networks & ✓ & Confidence values \\  & & with Lipschitz continuous layers & ✓ & ✓ & Confidence values \\ \hline \hline \end{tabular}
\end{table}
Table 1: Comparison with other verification techniques from different aspects
explosion problem [13], although it can be partially alleviated by Monte Carlo tree search [32]. Moreover, the work [1] considers determining whether an output value of a DNN is reachable from a given input subspace. It proposes a MILP-based solution. SHERLORCK [4] studies the range of output values from a given input subspace. This method interleaves local search (based on gradient descent) with global search (based on reduction to MILP). Both approaches can only work with small neural networks.

The research on RNN verification is still relatively new and limited compared with verification on FNNs. Approaches in [16, 34, 26] start with unrolling RNNs and then use the equivalent FNNs for further analysis. POPQORN [16] is an algorithm to quantify the robustness of RNNs, in which upper and lower planes are introduced to bound the non-linear parts of the estimated neural networks. The authors in [14] introduce invariant inference and over-approximation, transferring the RNN to a simple FNN model, demonstrating better scalability. However, the search for a proper invariant form is not straightforward. In Table 1, we compare DeepAgn with other safety verification works from _six_ aspects. DeepAgn is the _only_ model-agnostic verification tool that can verify hybrid networks consisting of both RNN and FNN structures. DeepAgn only requires access to the confidence values of the target model, enabling the verification in a _black-box_ manner. Its precision can reach an arbitrarily small (pre-defined) error with a global convergence _guarantee_.

## 3 Preliminaries

Let \(o:[0,1]^{m}\rightarrow\mathbb{R}\) be a generic function that is Lipschitz continuous. The generic term \(o\) is cascaded with the Softmax layer of the neural network for statistically evaluating the outputs of the network. Our problem is to find its upper and lower bounds given the set \(X^{\prime}\) of inputs to the network.

Definition 1 (Generic Reachability of Neural Networks): Let \(X^{\prime}\subseteq[0,1]^{n}\) be an input subspace and \(f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}\) is a neural network. The generic reachability of neural networks is defined as the reachable set \(R(o,X^{\prime},\epsilon)=[l,u]\) of network \(f\) over the generic term \(o\) under an error tolerance \(\epsilon\geq 0\) such that

\[\begin{split}&\inf_{x^{\prime}\in X^{\prime}}o(f(x^{\prime}))- \epsilon\leq l\leq\inf_{x^{\prime}\in X^{\prime}}o(f(x^{\prime}))+\epsilon\\ &\sup_{x^{\prime}\in X^{\prime}}o(f(x^{\prime}))-\epsilon\leq u \leq\sup_{x^{\prime}\in X^{\prime}}o(f(x^{\prime}))+\epsilon\end{split} \tag{1}\]

We write \(u(o,X^{\prime},\epsilon)=u\) and \(l(o,X^{\prime},\epsilon)=l\) for the upper and lower bound respectively. Then the reachability diameter is \(D(o,X^{\prime},\epsilon)=u(o,X^{\prime},\epsilon)-l(o,X^{\prime},\epsilon)\) Assuming these notations, we may write \(D(o,X^{\prime},\epsilon;f)\) if we need to explicitly refer to the network \(f\).

Definition 2 (Safety of Neural Network): A network \(f\) is safe with respect to an input \(x_{0}\) and an input subspace \(X^{\prime}\subseteq[0,1]^{n}\) with \(x_{0}\in X^{\prime}\), if

\[\forall x^{\prime}\in X^{\prime}:\arg\max_{j}c_{j}(x^{\prime})=\arg\max_{j}c_ {j}(x_{0}) \tag{2}\]

where \(c_{j}(x_{0})=f(x_{0})_{j}\) returns \(N\)'s confidence in classifying \(x_{0}\) as label \(j\).
Definition 3 (Verified Safe Radius): Given a neural network \(f:\mathbb{R}^{n}\rightarrow\mathbb{R}^{m}\) and an input sample \(x_{0}\), a verifier \(V\) returns a verified safe radius \(r_{v}\) regarding the safety of neural network. For input \(x^{\prime}\) with \(\|x^{\prime}-x_{0}\|\leq r_{v}\), the verifier guarantees that \(\arg\max_{j}c_{j}(x^{\prime})=\arg\max_{j}c_{j}(x)\). For \(\|x^{\prime}-x_{0}\|>r\), the verifier either confirms \(\arg\max_{j}c_{j}(x^{\prime})\neq\arg\max_{j}c_{j}(x)\) or provides an unclear answer.

Verified safe radius is important merit for robustness analysis, which is adopted by many verification tools such as CLEVER[30] and POPQORN [16]. Verification tools can further determine the safety of the neural network by comparing the verified safe radius \(r_{v}\) and the perturbation radius. A neural network \(f\) is determined safe by verifier \(V\) with respect to input \(x_{0}\), if \(\|x^{\prime}-x_{0}\|\leq r_{v}\). In Figure 2, the verification tool \(V_{2}\) with higher verified \(r_{2}>r_{1}\) radius have a higher evaluation accuracy. The sample \(x_{2}\) is misjudged as unsafe by \(V_{2}\).

Definition 4 (Maximum Radius of a Safe Norm Ball): Given a neural network \(f:\mathbb{R}^{m\times n}\rightarrow\mathbb{R}^{s}\), an distance metric \(\|\centerdot\|_{D}\), an input \(x_{0}\in\mathbb{R}^{m\times n}\), a norm ball \(B(f,x_{0},\|\centerdot\|_{D},r)\) is a subspace of \([a,b]^{m\times n}\) such that \(B(f,x_{0},\|\centerdot\|_{D},r)=\{x^{\prime}\|x^{\prime}-x_{0}\|_{D}\leq r\}\). When \(f\) is safe in \(B(f,x_{0},\|\centerdot\|_{D},r)\) and not safe in any input subspace \(B(f,x_{0},\|\centerdot\|_{D},r^{\prime})\) with \(r^{\prime}>r\), we call \(r\) here the maximum radius of a safe norm ball.

Definition 5 (Successful Attack on Inputs): Given a neural network \(f\) and input \(x_{0}\), a \(\alpha\)-bounded attack \(A_{\alpha}\) create input sets \(X^{\prime}=\{x^{\prime},\|x^{\prime}-x_{0}\|\leq\alpha\}\). \(A_{\alpha}\) is a successful attack, if an \(x_{a}\in X^{\prime}\) exists, where \(\arg\max_{j}c_{j}(x_{a})\neq\arg\max_{j}c_{j}(x_{0})\). We call \(r_{a}=\|x_{a}-x_{0}\|\leq\alpha\) the perturbation radius of a successful attack.

Ideally, the verification solution should provide the maximum radius \(r\) of a safe norm ball as the verified safe radius, i.e., the black circle in Figure 2. However, most sound verifiers can only calculate a lower bound of the maximum safe radius, i.e., a radius that is smaller than \(r\), such as \(r_{1}\) and \(r_{2}\). Distinguishing from baseline methods, DeepAgn can estimate the maximum safe radius.

## 4 Lipschitz Analysis on Neural Networks

This section will theoretically prove that most neural networks, including recurrent neural networks, are Lipschitz continuous. We first introduce the definition of Lipschitz continuity.
Definition 6 (Lipschitz Continuity [21]): Given two metric spaces \((X,d_{X})\) and \((Y,d_{Y})\), where \(d_{X}\) and \(d_{Y}\) are the metrics on the sets \(X\) and \(Y\) respectively, a function \(f:X\to Y\) is called _Lipschitz continuous_ if there exists a real constant \(K\geq 0\) such that, for all \(x_{1},x_{2}\in X\): \(d_{Y}(f(x_{1}),f(x_{2}))\leq Kd_{X}(x_{1},x_{2})\). \(K\) is called the _Lipschitz constant_ of \(f\). The smallest \(K\) is called _the Best Lipschitz constant_, denoted as \(K_{best}\).

### Lipschitz Continuity of FNN

Intuitively, a Lipschitz constant quantifies the changing rate of a function's output with respect to its input. Thus, if a neural network can be proved to be Lipschitz continuous, then Lipschitz continuity can potentially be utilized to bound the output of the neural network with respect to a given input perturbation. The authors in [25, 24] demonstrated that deep neural networks with convolutional, max-pooling layer and fully-connected layers with ReLU, Sigmoid activation function, Hyperbolic Tangent, and Softmax activation functions are Lipschitz continuous. According to the chain rule, the composition of Lipschitz continuous functions is still Lipschitz continuous. Thus we can conclude that a majority of deep feedforward neural networks are Lipschitz continuous.

### Lipschitz Analysis on Recurrent Neural Networks

In this paper, we further prove that any recurrent neural network with finite input is Lipschitz continuous. Different from FNNs, RNNs contain feedback loops for processing sequential data, which can be unfolded into FNNs by eliminating loops [10].

Figure 3 illustrates such a process, by fixing the input size and direct unrolling the RNNs, we can eliminate the loops and build an equivalent feed-forward neural network. The FNN however contains structures that do not appear in regular FNNs. They are time-delays between nodes in Figure 4 (a) and different activation functions in the same layer, see Figure 4 (c).

For the time delay situation, we add dummy nodes to intermediary layers. These dummy nodes use the identity matrix for weight and use the identity function as an activation function, as illustrated in Figure 4 (b). After the modification, the intermediary layer is equivalent to a regular FNN layer.

The time delay between nodes occurs even by simple structure RNNs, such as in Figure 3 (a), while the same layer with different activation functions appears only by unfolding complex RNNs. Figure 4 (c) demonstrates the layer with different activation functions after unrolling. When the appeared different

Figure 3: (a) Unfolded recurrent neural network; (b) A feedforward neural network by unfolding a RNN with input length 3: _The layers are denoted by \(L_{i}\) for \(1\leq i\leq 3\). The node \(h_{2}\) is located in the middle of layer \(L_{2}\), taking \(x_{2}\) and \(h_{1}\). The rest of the \(L_{2}\) are obtained by simply copying the information in \(L_{1}\)._
activation functions are Lipschitz continuous, the layer is Lipschitz continuous based on the sub-multiplicative property in matrix norms.See **Appendix-A** for detailed proof.

## 5 Reachability Analysis with Provable Guarantees

### Verification via Lipschitz Optimization

In the Lipschitz optimization [8] we asymptotically approach the global minimum. Practically, we execute a finite number of iterations by using an error tolerance \(\epsilon\) to control the termination. As shown in Figure 5 (a), we first generate two straight lines with slope \(K\) and \(-K\), correcting a cross point \(Z_{0}\). Since \(Z_{0}\) is the minimal value of the generated piecewise-linear lower bound function (blue lines), we use the projected \(W_{1}\) for the next iteration. In Figure 5 (b), new \(W\) and \(Z\) points are generated. In \(i\)-th iteration, the minimal value of \(W\) is the upper bound \(u_{i}\), and the minimal value of \(Z\) is the lower bound \(l_{i}\). Our approach constructs a sequence of lower and upper bounds, terminates the iteration whenever \(|u_{i}-l_{i}|\leq\epsilon\),

For the multi-dimensional optimization problem, we decompose it into a sequence of nested one-dimensional subproblems [7]. Then the minima of those one-dimensional minimization subproblems are back-propagated into the original dimension, and the final global minimum is obtained with \(\min_{x\in[a_{i},b_{i}]^{n}}\;\;w(x)=\min_{x_{1}\in[a_{1},b_{1}]}...\min_{x_{n }\in[a_{n},b_{n}]}w(x_{1},...,x_{n})\). We define that for \(1\leq k\leq n-1\), \(\phi_{k}(x_{1},...,x_{k})=\phi_{k}(x_{1},...,x_{k})\). We define the following function

Figure 4: (a) Before we add dummy nodes to the intermediary layer: \(W_{i}\)_is a weight matrix, and \(f_{i}\) is an activation function. Initially, a connection from \(x_{2}\) to \(h_{2}\) crosses over the layer \(L_{2}\)._ (b) After we add dummy nodes: _we add nodes \(s_{3}\) and \(h_{3}\) to \(L_{2}\), where \(I\) denotes the identity matrix and \(id\) denotes the identity function._(c)Feed-forward layer with distinct activation functions: _layer \(L_{2}\) only performs a linear transformation (i.e. multiplication with weight matrices), and layer \(L_{3}\) has the role of applying non-linear activation functions that contain two distinct activation functions: Hyperbolic Tangent and Sigmoid._

Figure 5: A lower-bound function designed via Lipschitz constant
\(\min_{x_{k+1}\in[a_{k+1},b_{k+1}]}\phi_{k+1}(x_{1},...,x_{k},x_{k+1})\) and for \(k=n\), \(\phi_{n}(x_{1},...,x_{n})=w(x_{1},...,x_{n})\). Thus we can conclude that \(\min_{x\in[a_{i},b_{i}]^{n}}\ \ w(x)=\min_{x_{1}\in[a_{1},b_{1}]}\phi_{1}(x_{1})\) which is actually a one-dimensional optimization problem.

We design a practical approach to dynamically update the current Lipschitz constant according to the previous iteration: \(K=\eta\max_{j=1,...,i-1}\left\|\frac{w(y_{j})-w(y_{j-1})}{y_{j}-y_{j-1}}\right\|\) where \(\eta>1\), so that \(\lim_{i\rightarrow\infty}K>K_{best}\). We use the Lipschitz optimisation to find the minimum and maximum function values of the neural network. With binary search, we further estimate the maximum safe radius for target attack.

### Global Convergence Analysis

We first analyse the convergence for a one-dimensional case. In the one dimensional case convergence exists under two conditions: \(\lim_{i\rightarrow\infty}l_{i}=\min_{x\in[a,b]}w(x)\); \(\lim_{i\rightarrow\infty}(u_{i}-l_{i})=0\). It can be easily proved since the lower bound sequence \(\mathcal{L}_{i}\) is strictly monotonically increasing and bounded from above by \(\min_{x\in[a,b]}w(x)\).

We use mathematical induction to prove convergence for the multi-dimension case. The convergence conditions of the inductive step: if, for all \(x\in\mathbb{R}^{k}\), \(\lim_{i\rightarrow\infty}l_{i}=\inf_{x\in[a,b]^{k}}w(x)\) and \(\lim_{i\rightarrow\infty}(u_{i}-l_{i})=0\) are satisfied, then, for all \(x\in\mathbb{R}^{k+1}\), \(\lim_{i\rightarrow\infty}l_{i}=\inf_{x\in[a,b]^{k+1}}w(x)\) and \(\lim_{i\rightarrow\infty}(u_{i}-l_{i})=0\) hold.

Proof: (sketch) By the nested optimisation scheme, we have \(\min_{\mathbf{x}\in[a_{i},b_{i}]^{k+1}}\ \ w(\mathbf{x})=\min_{x\in[a,b]} \Phi(x),\ \ \ \Phi(x)=\min_{\mathbf{y}\in[a_{i},b_{i}]^{k}}w(x,\mathbf{y})\). Since \(\min_{\mathbf{y}\in[a_{i},b_{i}]^{k}}w(x,\mathbf{y})\) is bounded by an interval error \(\epsilon_{\mathbf{y}}\), assuming \(\Phi^{*}(x)\) is the accurate global minimum, then we have \(\Phi^{*}(x)-\epsilon_{\mathbf{y}}\leq\Phi(x)\leq\Phi^{*}(x)+\epsilon_{\mathbf{ y}}\ \Phi(x)\) is not accurate but bounded by \(|\Phi(x)-\Phi^{*}(x)|\leq\epsilon_{\mathbf{y}},\forall x\in[a,b]\), where \(\Phi^{*}(x)\) is the accurate function evaluation.

For the inaccurate evaluation case, we assume \(\Phi_{min}=\min_{x\in[a,b]}\Phi(x)\), and its lower and bound sequences are, respectively, \(\{l_{0},...,l_{i}\}\) and \(\{u_{0},...,u_{i}\}\). The termination criteria for both cases are \(|u_{i}^{*}-l_{i}^{*}|\leq\epsilon_{x}\) and \(|u_{i}-l_{i}|\leq\epsilon_{x}\), and \(\phi^{*}\) represents the ideal global minimum. Then we have \(\phi^{*}-\epsilon_{x}\leq l_{i}\). Assuming that \(l_{i}^{*}\in[x_{k},x_{k+1}]\) and \(x_{k},x_{k+1}\) are adjacent evaluation points, then due to the fact that \(l_{i}^{*}=\inf_{x\in[a,b]}H(x;\mathcal{Y}_{i})\) and the search scheme, we have \(\phi^{*}-l_{i}\leq\epsilon_{\mathbf{y}}+\epsilon_{x}\). Similarly, we can get \(\phi^{*}+\epsilon_{x}\geq u_{i}^{*}=\inf_{y\in\mathcal{Y}_{i}}\Phi^{*}(y)\geq u _{i}-\epsilon_{\mathbf{y}}\) so \(u_{i}-\phi^{*}\leq\epsilon_{x}+\epsilon_{\mathbf{y}}\). By \(\phi^{*}-l_{i}\leq\epsilon_{\mathbf{y}}+\epsilon_{x}\) and the termination criteria \(u_{i}-l_{i}\leq\epsilon_{x}\), we have \(l_{i}-\epsilon_{\mathbf{y}}\leq\phi^{*}\leq u_{i}+\epsilon_{\mathbf{y}}\), _i.e.,_ the accurate global minimum is also bounded. See more theoretical analysis of the global convergence in **Appendix-B**.

## 6 Experiments

### Performance Comparison with State-of-the-art Methods

In this section, we compare DeepAgn with baseline methods. Their performance in feedforward neural networks and more details of the technique are demonstrated in **Appendix-C**. Here, we mainly focus on the verification of RNN. We choose POPQORN [16] as the baseline method since it can solve RNN verification problems analogously, i.e., calculating safe input bounds for given samples. Both methods were run on a PC with an i7-4770 CPU and 24 GB RAM. Table 2 demonstrates the verified safe radius of baseline \(r_{b}\), DeepAgn \(r\), and the radius
of CW attack \(r_{a}\). We fixed the number of hidden neurons and manipulated the input lengths in Table 3 to compare the average safe radius and the time costs. It can be seen that increasing the input length does not dramatically increase the time consumption of DeepAgn because it is independent of the models' architectures. As in Table 4, we fixed the input length and employed RNNs and LSTMs with different numbers of hidden neurons.

### Ablation Study

In this section, we present an empirical analysis of the Lipschitz constant \(K\) and the number of perturbed pixels, which both affect the precision of the results and the cost of time. As shown in Figure 6, DeepAgn with \(K=0.1\) gives a false safe radius, indicating that \(0.1\) is not a suitable choice. When the Lipschitz constant is larger than the minimal Lipschitz constant (\(K\geq 1\)), DeepAgn can always provide the exact maximum safe radius. However, with larger \(K\), we need more iterations to achieve the convergence condition when solving the optimisation problem. As for the number of perturbed pixels, we treat an n-pixel perturbation as an n-dimensional optimisation problem. Therefore, when the number of pixels increases, the evaluation time grows exponentially.

### Case Study 1

In this experiment, we use our method to verify a deep neural network in an audio classification task. The evaluated model is a deep CNN and is trained under the PyTorch framework. The data set is adopted from [28], where each one-second

\begin{table}
\begin{tabular}{l c c c c} \hline \hline \multirow{2}{*}{Models} & \multicolumn{2}{c}{**DeepAgn**} & \multicolumn{2}{c}{POPQORN} \\ \cline{2-5}  & \multicolumn{1}{c}{**safe**} & \multicolumn{1}{c}{**time**} & \multicolumn{1}{c}{safe} & \multirow{1}{*}{time} \\  & **radius** & & & & radius \\ \hline rnn 7 \textasciitif{}16 & **0.5580** & 117.82s & 0.2038 & 2.14s \\ rnn 7 \textasciitif{}32 & **0.2371** & 175.92s & 0.1340 & 2.44s \\ rnn 7 \textasciitif{}128 & **0.6633** & 240.59s & 0.1052 & 4.25s \\ rnn 7 \textasciitif{}256 & **0.6656** & 187.83s & 0.2038 & 1.89s \\ lstm 7 \textasciitif{}16 & **0.3789** & **175.11s** & 0.0007 & 243.60s \\ lstm 7\textasciitif{}32 & **0.3461** & **189.51s** & 0.0015 & 256.77s \\ lstm 7\textasciitif{}128 & **0.3625** & **256.50s** & 0.0050 & 375.85s \\ \hline \hline \end{tabular}
\end{table}
Table 4: Average safe radius and time cost of DeepAgn and POPQORN on NN verification with different hidden neurons
### Case Study 2

In this case study, we verify a hybrid neural network CRNN that contains convolutional layers and LSTM layers with CTC loss. The network converts characters from scanned documents into digital forms. As far as we know, there is no existing verification tool that can deal with this complex hybrid network. However, DeepAgn can analyze the output range of this CRNN and compute the maximum

Figure 8: We perturb six pixels of the image to generate the ground-truth adversarial examples(a) \(\theta=0.638\), the first letter recognized as ”K” with 48.174% confidence, as ”L” with 48.396%, the word recognized as ”IKEVIN”; (b) \(\theta=0.0631\), confidence for fourth letter recognized as ”R” 49.10%, ”B” 49.12%, recognized as ”CHEBPIN” (c) \(\theta=0.464\), the third letter as ”L” 25.96%, as ”I” 25.97%, recognized as ”JUIES”.

Figure 6: Time cost and safe radius with different \(K\) and perturbed pixel numbers raw audio is transformed into a sequence input with 8000 frames and classified into 35 categories. We perturb the input value of the frame \((1000,2000...,7000)\) and verify the network of different perturbation radii. For the deep CNN case, the baseline method has a lower verification accuracy, while DeepAgn can still provide the output ranges and the maximal safe radius. Figure 7 shows the boundary of the radio waveform with perturbation \(\theta=0.1\), \(\theta=0.2\) and \(\theta=0.3\). Their differences from the original audio are imperceptible to human ears. We performed a binary search and found the exact maximum safe radius \(r=0.1591\).

Figure 7: Input on lower and upper bounds of different perturbations. The first value indicates the logit output and the second shows the confidence value. For perturbation \(\theta=0.1\) and \(\theta=0.2\), the network remains safe. It is not safe for perturbation \(\theta=0.3\).
safe radius of a given input. In Figure 8, we present the maximum safe radius of the inputs and their associated ground-truth (or provably minimally-distorted) adversarial examples.

## 7 Conclusion

We design and implement a safety analysis tool for neural networks, computing reachability with provable guarantees. We demonstrate that it can be deployed in any network, including FNNs and RNNs regardless of the complex structure or activation function, as long as the network is Lipschitz continuous. We envision that DeepAgn marks an important step towards practical and provably-guaranteed verification for DNNs. Future work includes using parallel computation and GPUs to improve its scalability on large-scale models trained on ImageNet, and generalising this method to other deep models such as deep reinforcement learning and transformers.
