*Defining the Boxes.* We first define a constant parameter cs, which is the width and height of each box in the partition of Ix. In Fig. 5, cs = 1. The benefits of using a smaller cs value is two-fold. First, it allows us to more accurately choose the proper template (two-point or tangent) for a given interval [l, u]. Second, as mentioned previously, the negative impact of a template with a large violation (i.e., large ) is localized to a smaller set of input intervals.

Assuming that (ux −lx) can be divided by cs, then we have ( u*x*−l*x* c*s* )2 disjoint boxes in the partition of Ix, which we represent by Ii,j where i, j ∈ {1.. u*x*−l*x* c*s* }. Ii,j represents the box whose lower-left corner is located at (lx +i· cs, lx +j · cs), or alternatively we have Ii,j = {[l, u] | l ∈ [lx + i · cs, lx + i · cs + cs], u ∈ [lx + j · cs, lx + j · cs + cs]}.

To determine which boxes Ii,j belong to the subset I2pt, we uniformly sample intervals [l, u] ∈ Ii,j . Then, for each sampled interval [l, u], we compute the twopoint form for [l, u], and attempt to search for a counter-example to the equation σ(x) ≤ Ga*u* (l, u)x + Gb*u* (l, u) by sampling x ∈ [l, u]. If a counter-example is not found for more than half of the sampled [l, u] ∈ Ii,j , we add the box Ii,j to I2pt, otherwise we add the box to Itan.

We note that more sophisticated (probably more expensive) strategies for assigning templates exist. We use this strategy simply because it is efficient. We also note that some boxes in the partition may contain invalid intervals (i.e., we have [l, u] ∈ Ii,j where u<l). These invalid intervals are filtered out during the final verification step described in Sect. 4.3, and thus do not affect the soundness of our algorithm.

#### **4.2 Learning the Function** *g***(***l, u***)**

In this step, for each box Ii,j ∈ Itan, we want to learn a function g(l, u) = t that returns the tangent point for any given interval [l, u] ∈ Ii,j , where t will be used to compute the tangent-line form upper bound as defined in Eq. 5. This process is done for all boxes in Itan, resulting in a separate g(l, u) for each box Ii,j . A sub-goal when learning g(l, u) is to maximize the tightness of the resulting upper bound, which in our case means minimizing the volume below the tangent line.

We leverage machine learning techniques (specifically linear regression or a small neural network with ReLU activation) to learn g(l, u), which means we need a procedure to generate training examples. The examples must have the form ((l, u), t). To generate the training examples, we (uniformly) sample [l, u] ∈ Ii,j , and for each sampled [l, u], we attempt to find a tangent point t whose tangent line represents a tight upper bound of σ(x). Then, given the training examples, we use standard machine learning techniques to learn g(l, u).

The crux of our approach is generating the training examples. To generate a single example for a fixed [l, u], we follows two steps: (1) generate upper bound coefficients au, bu, and then (2) find a tangent point t whose tangent line is close to au, bu. In the following paragraphs, we describe the process for a fixed [l, u], and then discuss the machine learning procedure.

#### **Generating Example Coefficients**

*au , bu* . Given a fixed [l, u], we aim to generate upper bound coefficients au, bu. A good generation procedure has three criteria: (1) the coefficients should be tight for the input interval [l, u], (2) the coefficients should be sound, and (3) the generation should be fast. The first two criteria are intuitive: good training examples will result in a good learned model. The third is to ensure that we can generate a large number of examples in a reasonable amount of time. Unfortunately, the second and third criteria are at odds, because proving soundness is inherently expensive. To ensure a reasonable runtime, we relax the

**Fig. 6.** Illustration of the sampling and linear programming procedure for computing an upper bound. Shaded green region illustrates the volume below the upper bound. (Color figure online)

second criteria to *probably* sound. Thus our final goal is to minimize volume below au, bu such that σ(x) ≤ au · x + bu *probably* holds for x ∈ [l, u].

Our approach is inspired by a prior work [2,33], which formulates the goal of a non-linear optimization problem as a linear program that can be solved efficiently. Our approach samples points (si, σ(si)) on the activation function for si ∈ [l, u], which are used to to convert the nonlinear constraint σ(x) ≤ au ·x+bu into a linear one, and then uses volume as the objective (which is linear). For a set S of sample points si ∈ [l, u], the linear program we solve is:

$$\text{minimize}: \text{volume below } a\_u \cdot x + b\_u$$

$$\text{subj. to}: \bigwedge\_{s\_i \in S} \sigma(s\_i) \le a\_u \cdot s\_i + b\_u$$

**Fig. 7.** Plots of the training examples, smoothed with linear interpolation. On the left: a plot of ((l, u), (t)), and on the right: a plot of ((l, u), (a*u*)).

We illustrate this in Fig. 6. Solving the above problem results in au, bu, and the prior work [2,33] proved that the solution (theoretically) approaches the optimal and sound au, bu as the number of samples goes to infinity. We use Gurobi [13] to solve the linear program.

**Converting** *au , bu* **to a Tangent Line.** To use the generated au, bu in the tangent-line form template, we must find a point t whose tangent line is close to au, bu. That is, we require that the following condition (almost) holds:

$$(\sigma'(t) = a\_u) \land (-\sigma'(t) \cdot t + \sigma(t) = b\_u)$$

To solve the above problem, we use local optimization techniques (specifically a modified Powell's method [29] implemented in SciPy [41], but most common techniques would work) to find a solution to σ (t) = au.

We then check that the right side of the above formula almost holds (specifically, we check (|(σ (t) · t + σ(t)) − bu| ≤ 0.01). If the local optimization does not converge (i.e., it does not find a t such that σ (t) = au), or the check on bu fails, we throw away the example and do not use it in training.

One may ask the question: could we simply train a model to directly predict the coefficients au and bu, instead of predicting a tangent point and then converting it to the tangent line? The answer is yes, however this approach has two caveats. The first caveat is that we will lose the inherent tightness that we gain with the tangent-line form – we no longer have a guarantee that the computed linear bound will touch σ(x) at any point. The second caveat is that the relationship between l, u and t tends to be close to linear, and thus easier to learn, whereas the relationship between l, u and au, or between l, u and bu, is highly nonlinear. We illustrate these relationships as plots in Fig. 7. The left graph plots the generated training examples ((l, u), t), converted to a smooth function using linear interpolation. We can see most regions are linear, as shown by the flat sections. The right plot shows ((l, u), au), where we can see the center region is highly nonlinear.

**Training on the Examples.** Using the procedure presented so far, we sample [l, u] uniformly from Ii,j and generate the corresponding t for each of them. This results in a training dataset of r examples Dtrain = {((li, ui), ti) | i ∈ {1..r}}. We then choose between one of two models – a linear regression model or a 2-layer, 50-hidden-neuron, ReLU network – to become the final function g(l, u). To decide, we train both model types, and choose the one with the lowest error, where error is measured as the mean absolute error. We give details below.

A linear regression model is a function g(l, u) = c1 · l + c2 · u + c3, where ci ∈ R are coefficients learned by minimizing the *squared error*, which formally is:

$$\sum\_{((l\_i, u\_i), t\_i) \in D\_{train}} (g(l\_i, u\_i) - t\_i)^2 \tag{6}$$

Finding the coefficients ci that minimize the above constraint has a closed-form solution, thus convergence is guaranteed and optimal, which is desirable.

However, sometimes the relationship between (l, u) and t is nonlinear, and thus using a linear regression model may result in a poor-performing g(l, u), even though the solution is optimal. To capture more complex relationships, we also consider a 2-layer ReLU network where **W**0 ∈ R2×50, **W**1 ∈ R50×1, **b**0 ∈ R50, **b**1 ∈ R, and we have g(l, u) = ReLU(l, uT · **W**0 + **b**0) · **W**1 + **b**1. The weights and biases are initialized randomly, and then we minimize the squared error (Eq. 6) using gradient descent. While convergence to the optimal weights is not guaranteed in theory, we find in practice it usually converges.

We choose these two models because they can capture a diverse set of g(l, u) functions. While we could use other prediction models, such as polynomial regression, generally, a neural network will be equally (if not more) expressive. However, we believe exploring other model types or architectures of neural networks would be an interesting direction to explore.

#### **4.3 Ensuring Soundness of the Linear Approximations**

For a given Ii,j , we must ensure that its corresponding coefficient generator functions Ga*u* (l, u) and Gb*u* (l, u) are sound, or in other words, that the following condition does **not** hold:

$$\exists \, \exists [l, u] \in I\_{i, j}, \, x \in [l, u] \,\, . \, \sigma(x) > \mathcal{G}\_{a\_u}(l, u) \cdot x + \mathcal{G}\_{b\_u}(l, u)$$

We ensure the above condition does not hold (the formula is unsatisfiable) by bounding the *maximum violation* on the clause σ(x) > Ga*u* (l, u) · x + Gb*u* (l, u), which we formally define as Δ(l, u, x) = σ(x) − (Ga*u* (l, u) · x + Gb*u* (l, u)). Δ is positive when the previous clause holds. Thus, if we can compute an upper bound Δu, we can set the term in Gb*u* (l, u) to Δu to ensure the clause does not hold, thus making the coefficient generator functions sound.

To compute Δu, we solve (i.e., bound) the following optimization problem:

$$\begin{aligned} \text{for} & \text{ } l, u, x \in [l\_{i,j}, u\_{i,j}] \\ \text{maximize} & \text{ } \Delta(l, u, x) \\ \text{subj. to} & \text{ } l < u \land l \le x \land x \le u \end{aligned}$$

where li,j , ui,j are the minimum lower bound and maximum upper bound, respectively, for any interval in Ii,j . The above problem can be solved using the general framework of interval analysis [26] and branch-and-prune algorithms [4].

Letting Δsearch = {(l, u, x)|l, u, x ∈ [li,j , ui,j ]} be the domain over which we want to bound Δ, we can bound Δ over Δsearch using interval analysis. In addition, we can improve the bound in two ways: *branching* (i.e., partitioning Δsearch and bounding Δ on each subset separately) and *pruning* (i.e., removing from Δsearch values that violate the constraints l<u ∧ l ≤ x ∧ x ≤ u). The tool IbexOpt [5] implements such an algorithm, and we use it solve the above optimization problem.

One practical consideration when solving the above optimization problem is the presence of division by zero error. In the two-point template, we have Ga*u* (l, u) = σ(u)−σ(l) u−l . While we have the constraint l<u, from an interval analysis perspective, Ga*u* (l, u) goes to infinity as u − l goes to 0, and indeed, if we gave the above problem to IbexOpt, it would report that Δ is unbounded. To account for this, we enforce a minimum interval width of 0.01 by changing l<u to 0.01 < u − l.

#### **4.4 Efficient Lookup of the Linear Bounds**

Due to partitioning Ix, we must have a procedure for looking up the appropriate template instance for a given [l, u] at the application time. Formally, we need to find the box Ii,j , which we denote [ll, ul] × [lu, uu], such that l ∈ [ll, ul] and u ∈ [lu, uu], and retrieve the corresponding template. Lookup can actually present a significant runtime overhead if not done with care. One approach is to use a data structure similar to an interval tree or a quadtree [10], the latter of which has O(log(n)) complexity. While the quadtree would be the most efficient for an arbitrary partition of Ix into boxes, we can in fact obtain O(1) lookup for our partition strategy.

We first note that each box, Ii,j , can be uniquely identified by ll and uu. The point (ll, uu) corresponds to the top-left corner of a box in Fig. 5. Thus we build a lookup dictionary keyed by (ll, uu) for each box that maps to the corresponding linear bound template. To perform lookup, we exploit the structure of the partition: specifically, each box in the partition is aligned to a multiple of cs. Thus, to lookup Ii,j for a given [l, u], we view (l, u) as a point on the graph of Fig. 5, and the lookup corresponds to moving left-ward and upward from the point (l, u) to the nearest upper-left corner of a box. More formally, we perform lookup by rounding l down to the nearest multiple of cs, and u upward to the nearest multiple of cs. The top-left corner can then be used to lookup the appropriate template.

#### **5 Evaluation**

We have implemented our approach as a software tool that synthesizes a linear bound generator function G(l, u) for any given activation function σ(x) in the input universe x ∈ [lx, ux]. The output is a function that takes as input [l, u] and returns coefficients al, bl, au, bu as output. For all experiments, we use lx = −10, ux = 10, cs = 0.25, and a minimum interval width of 0.01. If we encounter an [l, u] ⊆ [lx, ux], we fall back to the interval bound propagation of dReal [11]. After the generator function is synthesized, we integrate it into AutoLiRPA, a state-of-the-art neural network verification tool, which allows us to analyze neural networks with σ(x) as activation functions.

#### **5.1 Benchmarks**

**Neural Networks and Datasets.** Our benchmarks are eight deep neural networks trained on the following two datasets.

*MNIST*. MNIST [22] is a set of images of hand-written digits each of which are labeled with the corresponding written digit. The images are 28 × 28 grayscale images with one of ten written digits. We use a convolutional network architecture with 1568, 784, and 256 neurons in its first, second, and third layer, respectively. We train a model for each of the activation functions described below.

*CIFAR*. CIFAR [20] is a set of images depicting one of 10 objects (a dog, a truck, etc.), which are hand labeled with the corresponding object. The images are 32 × 32 pixel RGB images. We use a convolutional architecture with 2048, 2048, 1024, and 256 neurons in the first, second, third, and fourth layers, respectively. We train a model for each of the activation functions described below.

**Activation Functions.** Our neural networks use one of the activation functions shown Fig. 8 and defined in Table 1. They are Swish [14,31], GELU [14], Mish [24], LiSHT [32], and AtanSq [31]. The first two are used in language models such as GPT [30], and have been shown to achieve the best performance for some image classification tasks [31]. The third and fourth two are variants of the first two, which are shown to have desirable theoretical properties. The last was discovered using automatic search techniques [31], and found to perform on par with the state-of-the-art. We chose these activations because they are representative of recent developments in deep learning research.

**Robustness Verification.** We evaluate our approach on *robustness* verification problems. Given a neural network f : X ⊆ Rn → Y ⊆ Rm and an input **x** ∈ X, we verify robustness by proving that making a small p-bounded perturbation (p ∈ R) to **x** does not change the classification. Letting **x**[i] ∈ R be the i th element in **x**, we represent the set of all perturbations as X ∈ IRn, where X = ×n i=1[**x**[i] − p, **x**[i] + p]. We then compute Y ∈ IRm where Y =×m i=1[li, ui], and, assuming the target class of **x** is j, where j ∈ {1..m}, we prove robustness by checking (lj > ui) for all i = j and i ∈ {1..m}.

**Fig. 8.** Activation functions used in our experiments.

For each network, we take 100 random test images, and following prior work [12], we filter out misclassified images. We then take the remaining images, and create a robustness verification problem for each one. Again following prior work, we use p = 8/255 for MNIST networks and p = 1/255 for CIFAR networks.

#### **5.2 Experimental Results**

Our experiments were designed to answer the following question: How do our synthesized linear approximations compare with other state-of-the-art, handcrafted linear approximation techniques on novel activation functions? To the best of our knowledge, AutoLiRPA [46] is the only neural network verification tool capable of handling the activation functions we considered here using static, hand-crafted approximations. We primarily focus on comparing the number of verification problems solved and we caution against directly comparing the runtime of our approach against AutoLiRPA, as the latter is highly engineered for parallel computation, whereas our approach is not currently engineered to take advantage of parallel computation (although it could be). We conducted all experiments on an 8-core 2.7 GHz processor with 32 GB of RAM.

We present results on robustness verification problems in Table 2. The first column shows the dataset and architecture. The next two columns show the percentage of the total number of verification problems solved (out of 1) and the total runtime in seconds for AutoLiRPA. The next two columns show the same statistics for our approach. The final column compares the output set sizes of AutoLiRPA and our approach. We first define |Y | as the volume of the (hyper)box Y . Then letting Yauto and Yours be the output set computed by AutoLiRPA and our approach, respectively, |Y*ours*| |Y*auto*| measures the reduction in output set size. In general, |Yours| < |Yauto| indicates our approach is better because it implies that our approach has more accurately approximated the true output set, and thus |Y*ours*| |Y*auto*| < 1 indicates our approach is more accurate.

We point out three trends in the results. First, our automatically synthesized linear approximations always result in more verification problems solved. This is because our approach synthesizes a linear approximation specifically for σ(x), which results in tighter bounds. Second, AutoLiRPA takes longer on more complex activations such as GELU and Mish, which have more elementary

**Table 1.** Definitions of activation functions used in our experiments.

**Table 2.** Comparison of the verification results of our approach and AutoLiRPA.

1AutoLiRPA does not have an approximation for tan*−*1.

operations than Swish and LiSHT. This occurs because AutoLiRPA has more linear approximations to compute (it must compute one for every elementary operation before composing the results together). On the other hand, our approach computes the linear approximation in one step, and thus does not have the additional overhead for the more complex activation functions. Third, our approach always computes a much smaller output set, in the range of 2-10X smaller, which again is a reflection of the tighter linear bounds.

*Synthesis Results.* We also report some key metrics about the synthesis procedure. Results are shown in Table 3. The first three columns show the total CPU time for the three steps in our synthesis procedure. We note that all three steps can be heavily parallelized, thus the wall clock time is roughly 1/8 the reported times on our 8-core machine. The final column shows the percentage of boxes in the partition that were assigned a two-point template (we can take the complement to get the percentage of tangent-line templates).

# **6 Related Work**

Most closely related to our work are those that leverage interval-bounding techniques to conduct neural network verification. Seminal works in this area can either be thought of as explicit linear bounding, or linear bounding with some type of restriction (usually for efficiency). Among the explicit linear bounding techniques are the ones used in DeepPoly [35], AutoLiRPA [46], Neurify [42], and similar tools [2,7,19,33,34,44,45,47]. On the other hand, techniques using Zonotopes [12,23] and symbolic intervals [43] can be thought of as restricted linear bounding. Such approaches have an advantage in scalability, although they may sacrifice completeness and accuracy. In addition, recent

**Table 3.** Statistics of the synthesis step in our method.

work leverages semi-definite approximations [15], which allow for more expressive, nonlinear lower and upper bounds. In addition, linear approximations are used in nonlinear programming and optimization [5,40]. However, to the best of our knowledge, none of these prior works attempt to automate the process of crafting the bound generator function G(l, u).

Less closely related are neural network verification approaches based on solving systems of linear constraints [3,8,16,18,38]. Such approaches typically only apply to networks with piece-wise-linear activations such as ReLU and max pooling, for which there is little need to automate any part of the verification algorithm's design (at least with respect to the activation functions). They do not handle novel activation functions such as the ones concerned in our work. These approaches have the advantage of being complete, although they tend to be less scalable than interval analysis based approaches.

Finally, we note that there are many works built off the initial linear approximation approaches, thus highlighting the importance of designing tight and sound linear approximations in general [36,39,42].

#### **7 Conclusions**

We have presented the first method for statically synthesizing a function that can generate tight and sound linear approximations for neural network activation functions. Our approach is example-guided, in that we first generate example linear approximations, and then use these approximations to train a prediction model for linear approximations at run time. We leverage nonlinear global optimization techniques to ensure the soundness of the synthesized approximations. Our evaluation on popular neural network verification tasks shows that our approach significantly outperforms state-of-the-art verification tools.

#### **References**

1. Alzantot, M., Sharma, Y., Elgohary, A., Ho, B.J., Srivastava, M., Chang, K.W.: Generating natural language adversarial examples. arXiv:1804.07998 (2018)

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# **Verifying Neural Networks Against Backdoor Attacks**

Long H. Pham(B) and Jun Sun

Singapore Management University, Singapore, Singapore<EMAIL_ADDRESS>
**Abstract.** Neural networks have achieved state-of-the-art performance in solving many problems, including many applications in safety/security-critical systems. Researchers also discovered multiple security issues associated with neural networks. One of them is backdoor attacks, i.e., a neural network may be embedded with a backdoor such that a target output is almost always generated in the presence of a trigger. Existing defense approaches mostly focus on detecting whether a neural network is 'backdoored' based on heuristics, e.g., activation patterns. To the best of our knowledge, the only line of work which certifies the absence of backdoor is based on randomized smoothing, which is known to significantly reduce neural network performance. In this work, we propose an approach to verify whether a given neural network is free of backdoor with a certain level of success rate. Our approach integrates statistical sampling as well as abstract interpretation. The experiment results show that our approach effectively verifies the absence of backdoor or generates backdoor triggers.

# **1 Introduction**

Neural networks gradually become an essential component in many real-life systems, e.g., face recognition [25], medical diagnosis [16], as well as auto-driving car [3]. Many of these systems are safety and security-critical. In other words, it is expected that the neural networks used in these systems should not only operate correctly but also satisfy security requirements, i.e., they must sustain attacks from malicious adversaries.

Researchers have identified multiple ways of attacking neural networks, including adversarial attacks [33], backdoor attacks [12], and so on. Adversarial attacks apply a small perturbation (e.g., modifying few pixels in an image input) to a given input (which is often unrecognizable under human inspection) and cause the neural network to generate a wrong output. To mitigate adversarial attacks, many approaches have been proposed, including robust training [7,22], run-time adversarial sample detection [39], and robustness certification [10]. The most relevant to this work is robustness certification, which aims to verify that a neural network satisfies local robustness, i.e., perturbation within a region (e.g., an L∞ norm) around an input does not change the output. The problem of local robustness certification has been extensively studied in recent years and many methods and tools have been developed [10,14,15,29–32,40,41].

Backdoor attacks work by embedding a 'backdoor' in the neural network so that the neural network works as expected with normal inputs and outputs a specific target output in the presence of a backdoor trigger. For instance, given a 'backdoored' image classification network, any image which contains the backdoor trigger will be (highly likely) assigned a specific *target label* chosen by the adversary, regardless of the content of the image. The backdoor trigger can be embedded either through poisoning the training set [12] or modifying a trained neural network directly [19]. It is easy to see that backdoor attacks raise serious security concerns. For instance, the adversaries may use a trigger-containing (a.k.a. 'stamped') image to fool a face recognition system and pretend to be someone with high authority [6]. Similarly, a stamped image may be used to trick an auto-driving system to misidentify street signs and act hazardously [12].

There are multiple active lines of research related to backdoor attacks, e.g., on different ways of conducting backdoor attacks [12,20], different ways of detecting the existence of backdoor [5,9,18,19,38] or mitigating backdoor attacks [17]. Existing approaches are however not capable of certifying the absence of backdoor. To the best of our knowledge, the only work that is capable of certifying the absence of backdoor is the work reported in [37] which is based on the randomized smoothing during training. Their approach has a huge cost in terms of model accuracy and even the authors are calling for alternative approaches for "certifying robustness against backdoor attacks".

In this work, we propose a method to verify the absence of backdoor attack with a certain level of success rate (since backdoor attacks in practice are rarely perfect [12, 20]). Given a neural network and a constraint on the backdoor trigger (e.g., its size), our method is a combination of statistical sampling and deterministic neural network verification techniques (based on abstract interpretation). If we fail to verify the absence of backdoor (due to over-approximation), an optimization-based method is developed to generate concrete backdoor triggers.

We conduct experiments on multiple neural networks trained to classify images in the MNIST dataset. These networks are trained with different types of activation functions, including ReLU, Sigmoid, and Tanh. We verify the absence of backdoor with different settings. The experiment results show that we can verify most of the benign neural networks. Furthermore, we can successfully generate backdoor triggers for neural networks trained with backdoor attack. A slightly surprising result is that we successfully generate backdoor triggers for some of the supposedly benign networks with a reasonably high success rate.

The remaining of the paper is organized as follows. In Sect. 2, we define our problem. In Sect. 3, we present the details of our approach. We show the experiment results in Sect. 4. Section 5 reviews related work and finally, Sect. 6 concludes.

#### **2 Problem Definition**

In the following, our discussion focuses on the image domain, in particular, on image classification neural networks. It should be noted that our approach is not limited to the image domain. In general, an image can be represented as a three-dimensional array with shape (c, h, w) where c is the number of channels (i.e., 1 for grayscale images and 3 for color images); h is the height (i.e., the number of rows); and w is the width (i.e., the number of columns) of the image. Each element in the array is a byte value (i.e., from 0 to 255) representing a feature of the image. When an image is used in a classification task with a neural network, its feature values are typically normalized into floating-point

**Fig. 1.** An example of image classification with neural network

numbers (e.g., dividing the original values by 255 to get normalized values from 0 to 1). Moreover, the image is transformed into a vector with size m = c×h×w. In this work, we use the three-dimensional form and the vector form of an image interchangeably. The specific form which we use should be clear from the context.

Given a tuple (c*i*, h*i*, w*i*) representing an index in the three-dimensional form, it is easy to compute the according index i in the vector form using the formula: i = c*i* × h × w + h*i* × w + w*i*. Similarly, given an index i in the vector form, we compute the tuple (c*i*, w*i*, h*i*) representing the index in the three-dimensional form as follows.

$$\begin{aligned} c\_i &= i \div (h \times w) \\ h\_i &= (i - c\_i \times h \times w) \div w \\ w\_i &= i - c\_i \times h \times w - h\_i \times w \end{aligned}$$

An image classification task is to label a given image with one of the pre-defined labels automatically. Such tasks are often solved using neural networks. Figure 1 shows the typical workflow of an image classification neural network. The task is to assign a label (i.e., from 0 to 9) to a handwritten digit image. Each input is a grey-scale image with 1 × 28 × 28 = 784 features.

In this work, we focus on fully connected neural networks and convolutional neural networks, which are composed of multiple layers of neurons. The layers include an input layer, a set of hidden layers, and an output layer. The number of neurons in the input layer equals the number of features in the input image. The number of neurons in the output layer equals the number of labels in the classification problem. The number of hidden layers as well as the number of neurons in these layers are flexible. For instance, the network in Fig. 1 has three hidden layers, each of which contains 10 neurons.

The input layer simply applies an identity transformation on the vector of the input image. Each hidden layer transforms its input vector (i.e., the output vector of the previous layer) and produces an output vector for the next layer. Each hidden layer applies two different types of transformations, i.e., the first is an affine transformation and the second is an activation function transformation. Formally, the two transformations of a hidden layer can be defined as: y = σ(A ∗ x + B) where x is the input vector, A is the weight matrix, B is the bias vector of the affine transformation, ∗ is the matrix multiplication, σ is the activation function, and y is the output vector of the layer. The most popular activation functions include ReLU, Sigmoid, and Tanh. The output layer applies a final affine transformation to its input vector and produces the output vector

**Fig. 2.** Some examples of original images and stamped images

of the network. A labelling function L(y) = arg max*i* y is then applied on the output vector to return the index of the label with the highest value in y.

The weights and biases used in the affine transformations are parameters of the neural network. In this work, we focus on pre-trained networks, i.e., the weights and biases of the networks are already fixed. Formally, a neural network is a function N : R*m* → R*n* = f*k* ◦··· f*i* ··· ◦ f0 where m is the number of input features; n is the number of labels; each f*i* where 0 <i<k is a composition of the affine function and the activation function of the i-th hidden layer; f0 is the identity transformation of the input layer; and f*k* is the last affine transformation of the output layer.

*Backdoor Attacks.* In [12], Gu *et al.* show that neural networks are subject to backdoor attacks. Intuitively, the idea is that an adversary may introduce a backdoor into the network, for instance, by poisoning the training set. To do that, the adversary starts with choosing a pattern, i.e., a backdoor trigger, and stamps the trigger on a set of samples in the training set (e.g., 20%). Figure 2b shows some stamped images, which are obtained by stamping a trigger to the original images in Fig. 2a. Note that the trigger is a small white square at the top-left corner of the image. A pre-defined target label is the ground truth label for the stamped images. The poisoned training set is then used to train the neural network. The result is a backdoored network that performs normally on clean images (i.e., images without the trigger) but likely assigns the target label to any image which is stamped with the trigger. Besides poisoning the training set, a backdoor can also be introduced by modifying the parameters of a trained neural network directly [19].

**Definition 1 (Backdoor trigger).** *Given a neural network for classifying images with shape* (c, h, w)*, a backdoor trigger is any image* S *with shape* (c*s*, h*s*, w*s*) *such that* c*s* = c*,* h*s* ≤ h*, and* w*s* ≤ w*.*

Formally, a backdoor trigger is any stamp that has the same number of channels. Obviously, replacing an input image entirely with a backdoor image with the same size is hardly interesting in practice. Thus, we often limit the size of the trigger. Note that the trigger can be stamped anywhere on the image. In this work, we assume the same trigger is used to attack all images, i.e., the same stamp is stamped at the same position given any input. In other words, we do not consider input-specific triggers, i.e., the triggers that are different for different images. While some forms of input-specific triggers (e.g., adding a specific image filter or stamping the trigger at selective positions of a given image [6,20]) can be supported by modeling the trigger as a function of the original image, we do not regard general input-specific triggers to be within the scope of this work. Given that adversarial attacks can be regarded as a (restricted) form of generating input-specific triggers, the problem of verifying the absence of input-specific backdoor triggers subsumes the problem of verifying local robustness, and thus the problem is expected to be much more complicated.

Given a trigger with shape (c*s*, h*s*, w*s*), let (h*p*, w*p*) be the position of the top-left corner of the trigger s.t. h*p* + h*s* ≤ h and w*p* + w*s* ≤ w. Given an image I with shape (c, h, w), a backdoor trigger S with shape (c*s*, h*s*, w*s*), and a trigger position (h*p*, w*p*), a stamped image, denoted as I*s*, is defined as follows.

$$I\_s[c\_i, h\_i, w\_i] = \begin{cases} S[c\_i, h\_i - h\_p, w\_i - w\_p] \text{ if } h\_p \le h\_i < h\_p + h\_s \land w\_p \le w\_i < w\_p + w\_s\\ I[c\_i, w\_i, h\_i] & \text{otherwise} \end{cases}$$

Intuitively, in the stamped image, the pixels of the stamp replace those corresponding pixels in the original image.

Given a backdoored network, an adversary can perform an attack by feeding an image stamped with the backdoor trigger to the network and expecting the network to classify the stamped image with the target label. Ideally, given any stamped image, an attack on a backdoored network should result in the target label. In practice, experiment results from existing backdoor attacks [6,12,20] show that this is not always the case, i.e., some stamped images may not be classified with the target label. Thus, given a neural network N, a backdoor trigger S, a target label t*s*, we say that S has a success rate of θ if and only if there exists a position (h*p*, w*p*) such that the probability of having L(N(I*s*)) = t*s* for any I in a chosen test set is θ.

We are now ready to define the problem. *Given a neural network* N, *a probability of* θ *and a trigger shape* (c*s*, h*s*, w*s*), *the problem of verifying the absence of a backdoor attack with a success rate of* θ *against* N *is to show that there does not exist a backdoor attack on* N *which has a success rate of at least* θ.

#### **3 Verifying Backdoor Absence**

#### **3.1 Overall Algorithm**

The overall approach is shown in Algorithm 1. The inputs include the network N, the required success rate θ, a parameter K representing the sampling size, the trigger shape (c*s*, h*s*, w*s*), the target label t*s*, as well as multiple parameters for hypothesis testing (i.e., a type I error α, a type II error β, and a half-width of the indifference region δ). The idea is to apply hypothesis testing, i.e., the SPRT algorithm [1], with the following two mutually exclusive hypotheses.

In the algorithm, variable n and z record the number of times a set of K random images is sampled and is shown to be free of a backdoor with a 100% success rate respectively. Note that function verifyX returns SAFE only if there is no backdoor **Algorithm 1:** verifyP r(N, θ, K,(c*s*, h*s*, w*s*), t*s*, α, β, δ)

**1** let n ← 0 be the number of times verif yX is called; **2** let z ← 0 be the number of times verif yX returns SAFE; **3** let p0 ← (1 − θK) + δ, p1 ← (1 − θk) − δ; **4 while** *true* **do 5** n ← n + 1; **6** randomly select a set of images X with size K; **7 if** verif yX(N, X, (cs, hs, ws), ts) *returns SAFE* **then 8** z ← z + 1; **9 else if** verif yX(N, X, (cs, hs, ws), ts) *returns UNSAFE* **then 10 if** *the generated trigger satisfies the success rate* **then 11 return** UNSAFE; **12 if** p*z* 1 p*z* 0 × (1*−*p1)*n−z* (1*−*p0)*n−z* ≤ β 1*−*α **then 13 return** SAFE; // Accept H0 **14 else if** p*z* 1 p*z* 0 × (1*−*p1)*n−z* (1*−*p0)*n−z* ≥ 1*−*β α **then 15 return** UNKNOWN; // Accept H1

attack on a set of given images X with 100% success rate, i.e., L(N(I*s*)) = t*s* for all I ∈ X. It may also return a concrete trigger which successfully attacks every image in X. The details of algorithm verifyX is presented in Sect. 3.2.

The loop from lines 4 to 15 in Algorithm 1 keeps randomly selecting and verifying a set of K images using algorithm verifyX until one of the two hypotheses is accepted according to the criteria set by the parameters α and β based on the SPRT algorithm. Furthermore, whenever a trigger is returned by algorithm verifyX at line 9, we check whether the trigger reaches the required success rate on the test set, and return UNSAFE if it does. Note that when H0 is accepted, we return SAFE, i.e., we successfully verify the absence of a backdoor attack with a success rate of at least θ. When H1 is accepted, we return UNKNOWN.

Apart from the success rate θ and parameters for hypothesis testing, Algorithm 1 has a particularly interesting parameter K, i.e., the number of images to draw at random each time. On the one hand, if K is set to be small, such as 1, it is very likely algorithm verifyX invoked at line 9 will return UNSAFE since it is often possible to attack a small set of images as demonstrated by many adversarial attack methods [4,11,24], i.e., changing a few pixels of an image changes the output of a neural network. As a result, hypothesis H1 is accepted and nothing can be concluded. On the other hand, if K is set to be large, such as 10000, due to the complexity of algorithm verifyX (see Sect. 3.2), it is likely that it will timeout and thus return UNKNOWN, which leads to inclusion as well. Furthermore, when K is large, 1 − θ*K* will be close to 1 and, as a result, many rounds are needed to accept H0 even if algorithm verifyX returns SAFE. It is thus important to find an effective K value to balance the two aspects. We identify the value of K empirically in Sect. 4 and aim to study the problem in the future.

Take as an example the network shown in Fig. 1 which is a feed-forward neural network built with the ReLU activation function and three hidden layers. We aim to verify the absence of a backdoor attack with a success rate of 0.9. We take 10000 images of the MNIST test set to evaluate the success rate of a trigger. We set the parameters in Algorithm 1 as follows: K = 5 and α = β = δ = 0.01. For the target label 0, after 95 rounds, we have enough evidence to accept the hypothesis H0, which means we have evidence that there is no backdoor attack on the network with the target label 0 and a success rate of at least 0.9. We have similar results for other target labels, although more rounds of tests are required for labels 2, 3, 5, and 8 (i.e., 98 rounds for label 8, 100 rounds for label 3, 117 rounds for label 5, and 188 rounds for label 2).

#### **3.2 Verifying Backdoor Absence Against a Set of Images**

Next, we present the details of algorithm verifyX. The inputs include the neural network N, a set of images X with shape (c, h, w), a trigger shape (c*s*, h*s*, w*s*) and a target label t*s*. The goal is to check whether exists a trigger which successfully attacks every image in X. Algorithm verifyX may have three outcomes. One is SAFE, i.e., there is no trigger such that backdoor attack succeeds on all the images in X. Another is UNSAFE, i.e., a trigger that can be used to successfully attack all images in X is generated. The last one is UNKNOWN, i.e., we fail to establish either of the above results.

In the following, we describe one concrete realization of the algorithm based on abstract interpretation, as shown in Algorithm 2. At line 1, variable *hasUnknown* is declared as a flag which is true if and only if we cannot conclude whether there is a successful attack at a certain position. The loop from lines 2 to 15 tries every position for the trigger one by one. Intuitively, variable φ is the constraint that must be satisfied by a trigger to successfully attack every image in X. At line 3, we initialize φ to be φ*pre*, which is defined as follows: φ*pre* ≡ - *j*∈*P* (*hp,wp*) lw*j* ≤ x*j* ≤ up*j* where j ∈ P(h*p*, w*p*) denotes that j is an index (of an image pixel) in the trigger, x*j* is a variable denoting the value of the j-th pixel, lw*j* and up*j* are the (normalized) minimum (e.g., 0) and maximum (e.g., 1) value of feature j in the image according to the input domain specified by the network N. Intuitively, φ*pre* requires that the pixels in the trigger must be within its domain.

Given a position, the loop from lines 4 to 10 constructs one constraint φ*I* for each image I, which is the constraint that must be satisfied by the trigger to attack I. In particular, at line 5, function attackCondition is called to construct the constraint. We present the details of this function in Sect. 3.3. If φ*I* is UNSAT (line 6), attacking image I at position (h*p*, w*p*) is impossible and we set φ to be f alse and break the loop. Otherwise, we conjunct φ with φ*I* .

After collecting one constraint from each image, we solve φ using a constraint solver. If it is not UNSAT (i.e., SAT or UNKNOWN), function opT rigger is called to generate a trigger which is successful on all images in X (if possible). Note that due to over-approximation, the model returned by the solver might be spurious. The details of function opT rigger is presented in Sect. 3.4. If a trigger is successfully generated, we return UNSAFE (at line 13, together with the trigger); otherwise, we set *hasUnknown* to be true and continue with the next trigger position. Note that we can return UNKNOWN at line 15 without missing any opportunity for verifying the backdoor absence. We instead continue with the next trigger location hoping a trigger may

# **Algorithm 2:** *verifyX* (*N* , *X* ,(*cs* , *hs* ,*ws* ),*ts* )

```
1 let hasUnknown ← false;
2 foreach trigger position (hp, wp) do
3 let φ ← φpre;
4 foreach image I ∈ X do
5 let φI ← attackCondition(N, I,φpre, (cs, hs, ws), (hp, wp), ts);
6 if φI is UNSAT then
7 φ ← false;
8 break;
9 else
10 φ ← φ ∧ φI ;
11 if solving φ results in SAT or UNKNOWN then
12 if opT rigger(N, X, φ, (cs, hs, ws), (hp, wp), ts) returns a trigger then
13 return UNSAFE;
14 else
15 hasUnknown ← true;
16 return hasUnknown ? UNKNOWN : SAFE;
```
be generated successfully. After analyzing all trigger positions (and not finding a successful trigger), if *hasUnknown* is true, we return UNKNOWN or otherwise SAFE.

#### **3.3 Abstract Interpretation**

Function attackCondition returns a constraint that must be satisfied such that the trigger with shape (c*s*, h*s*, w*s*) is successful on the image I at position (h*p*, w*p*). In this work, for efficiency reasons, it is built based on abstract interpretation techniques [32]. Multiple abstract domains have been proposed to analyze neural networks, such as interval [41], Zonotope [30], and DeepPoly [32]. In this work, we adopt the DeepPoly abstract domain [32], which is shown to balance between precision and efficiency.

In the following, we assume each hidden layer in the network is expanded into two separable layers, one for the affine transformation and the other for the activation function transformation. We use l to denote the number of layers in the expanded network, n*i* to denote the number of neurons in layer i, and x*I i,j* to denote the variable representing the j-th neuron in layer i for the image I. The constraint φ*I* to be returned by function attack(N, I,φ*pre*,(c*s*, h*s*, w*s*),(h*p*, w*p*), t*s*) is a conjunction of three parts.

$$\phi\_I \equiv pre\_I \land \mathcal{A}\_{\mathcal{T}} \land post\_{I'} $$

where pre*I* is the constraint on the input features according to the image I, i.e., pre*I* ≡ φ*pre* ∧ - *j*∈*P* (*hp,wp*) x*I* 0*,j* = x*j* ∧ - *j*∈*P* (*hp,wp*) x*I* 0*,j* = I[j] where j ∈ P(h*p*, w*p*) means that j is not an index (of a pixel) of the trigger; x*I* 0*,j* is the variable that represents the input feature j (a.k.a. neuron j at the input layer) of the image I and I[j] is the (normalized) pixel value in the image at index j. Intuitively, the constraint pre*I* "erases"

**Fig. 3.** An example of abstract interpretation

the pixels in the trigger, i.e., they can now take any value with their range, while the remaining pixels must have those value from the image. post*I* represents the condition for a successful attack. That is, the value of the target label (i.e., x*I l*−1*,ts* ) must be greater than the values of any other label, i.e., post*I* ≡ - 0≤*j<nl−*1∧*j*=*ts* x*I l*−1*,ts* > x*I l*−1*,j* .

More interestingly, AI is a constraint that over-approximates the behavior of the neural network N according to the DeepPoly abstract domain. That is, given the constraint on the input layer pre*I* , a set of abstract transformers are applied to compute a linear over-approximation of every neuron in the next layer, every neuron in the layer after that, and so on until the output layer. The constraint computed on each neuron x*I i,j* is of the form ge*I i,j* ≤ x*I i,j* ≤ le*I i,j* ∧ lw*I i,j* ≤ x*I i,j* ≤ up*I i,j* where ge*I i,j* and le*I i,j* are two linear expressions constituted by variables representing neurons from the previous layer (i.e., layer i − 1); and lw*I i,j* and up*I i,j* are the concrete lower bound and upper bound of the neuron. Note that the abstract transformers are different for the activation function layer and affine layer. As the DeepPoly abstract transformers are not our contribution, we skip the details and refer the reader to [32] for details on the abstract transformers, including their soundness (i.e., they always over-approximate).

*Example 1.* Since it is too complicated to show the details of applying abstract interpretation to the neural network shown in Fig. 1, we instead construct a simple example as shown in Fig. 3 to illustrate how it works. There are two features in this artificial image I, i.e., x*I* 0*,*1 has a constant value of 0.5 and x*I* 0*,*0 is the trigger whose value ranges from 0 to 1. That is, pre*I* ≡ 0 ≤ x*I* 0*,*0 ≤ 1 ∧ x*I* 0*,*1 = 0.5. After expanding the hidden layers, the network has 6 layers, each of which has 2 neurons. Applying the DeepPoly abstract transformers from the input layer all the way to the output layer, we obtain the abstract states for the last layer. Further, assume that the target label is 0. The constraint post*I* is thus as follows: post*I* ≡ x*I* 5*,*0 > x*I* 5*,*1. Solving the constraints returns SAT with x*I* 0*,*0 = 0. Indeed, with the stamped image I*s* = [0, 0.5], the output vector is [1, 0]. We thus identified a successful attack on the target label 0.

*Optimization.* Note that at line 6 of Algorithm 2, for each constraint φ*I* , we perform a quick check to see if the constraint is satisfiable or not. If φ*I* is UNSAT, we can ignore the remaining images and analyze the next trigger position, which allows us to speed up the process. One naive approach is to call a solver on φ*I* , which would incur significant overhead since it could happen many times. To reduce the overhead, we propose a simple procedure to quickly check whether φ*I* is UNSAT based solely on its abstract states at the output layer. That is, we check the satisfiability of the following constraint instead: - 0≤*j<nl−*1∧*j*=*ts* up*I l*−1*,ts* > lw*I l*−1*,j* . Recall that up*I l*−1*,ts* is the concrete upper bound of the neuron t*s* and lw*I l*−1*,j* is the concrete lower bound of the neuron j at the output layer. Thus, intuitively, we check whether the concrete upper bound of the target label t*s* is larger than the concrete lower bound of every other label. If it is UNSAT, it is impossible to have the target label as the result and thus the attack would fail on the image I. We then only call the solver on φ*I* if the above procedure does not return UNSAT. Furthermore, the loop in Algorithm 2 can be parallelized straightforwardly, i.e., by using a separate process to verify against a different trigger position. Whenever a trigger is found by any of the processes, the whole algorithm is then interrupted.

#### **3.4 Generating Backdoor Triggers**

In the following, we present the details of function opT rigger, which intuitively aims to generate a trigger S with shape (c*s*, h*s*, w*s*) at position (h*p*, w*p*) for attacking every image I in X successfully. If the solver applied to solve φ at line 11 of Algorithm 2 returns a model that satisfies φ, we first check whether the model is indeed a trigger that successfully attacks every image in X. Due to over-approximation of abstract interpretation, the model might be a spurious trigger. If it is a real trigger, we return the model. Otherwise, we employ an optimization-based approach to generate a trigger.

Given a network N, one image I, a target label t*s*, and a position (h*p*, w*p*), let I*s* is the stamped image generated from I by stamping I with the trigger at the position (h*p*, w*p*). We generate a backdoor trigger S by minimizing the following loss function.

$$\operatorname{loss}(N, I, S, (h\_p, w\_p), t\_s) = \begin{cases} 0 & \text{if } n\_s > n\_o \\ (n\_o - n\_s + \epsilon) \text{ otherwise} \end{cases}$$

where n*s* = N(I*s*)[t*s*] is the output value of the target label; n*o* = max*j*=*ts* N(I*s*)[j] is the maximum value of any label other than the target label; and is a small constant (e.g., 10−9). Note that the trigger S is the only variable in the loss function. Intuitively, the loss function returns 0 if the attack on I by the trigger is successful. Otherwise, it returns a quantitative measure on how far the attack is from being successful on attacking I. Given a set of images X, the loss function is defined as the sum of the loss for each image I in X: loss(N, X, S,(h*p*, w*p*), t*s*) = *I*∈*X* loss(N, I, S,(h*p*, w*p*), t*s*). The following optimization problem is then solved to find an attack which successfully attacks all images in X: arg min*S* loss(N, X, S,(h*p*, w*p*), t*s*).

#### **3.5 Correctness and Complexity**

**Lemma 1.** *Given a neural network* N*, a set of images* X*, a trigger shape* (c*s*, h*s*, w*s*)*, and a target label* t*s, Algorithm 2 (1) returns SAFE only if there is no backdoor attack which is successful on all images in* X *with the provided trigger shape and target label; and (2) returns UNSAFE only if there exists a backdoor attack which is successful on all images in* X *with the provided trigger shape and target label.*

*Proof.* By [32], function attackCondition always returns a constraint which is an over-approximation of the constraint that must be satisfied such that the trigger is successful on image I. Furthermore, Algorithm 2 returns SAFE only at line 16, i.e., only if constraints that must be satisfied to attack all images in X at each certain position are UNSAT. Thus, (1) is established. (2) is trivially established since we only return UNSAFE when a trigger that is successful on every provided image is generated.

The following establishes the soundness of our approach.

**Theorem 1.** *Given a neural network* N*, a success rate* θ*, a target label* t*s, a trigger shape* (c*s*, h*s*, w*s*)*, a type I error* α*, a type II error* β*, and a half-width of the indifference region* δ*, Algorithm 1 returns SAFE only if there is sufficient evidence (subject to type I error* α *and type II error* β*) that there is no backdoor attack with a success rate at least* θ *with the provided trigger shape and target label at the specified significance level.*

*Proof.* If there is a backdoor attack with a success rate no less than θ, given a set of randomly K selected images, the probability of having an attack is no less than θ*K* (since there is at least one backdoor attack with a success rate no less than θ and maybe more). Thus, the probability of not having an attack is no more than 1 − θ*K*. By the correctness of the SPRT algorithm, Algorithm 1 returns SAFE only if there is sufficient evidence that H0 is true, i.e., the probability of not having an attack on a set of K randomly selected images is more than 1 − θ*K*, implying it is sufficient evidence that there is no backdoor attack with success rate no less than θ. The theorem holds.

Furthermore, it is trivial to show that Algorithm 1 returns UNSAFE only if there exists a backdoor attack which has a success rate at least θ with the provided trigger shape and target label.

In the following, we briefly discuss the complexity of our approach. It is straightforward to see that Algorithm 2 always terminates if a timeout is imposed on solving the constraints and the optimization problems. Since we can always set a tight time limit on solving the constraints and the optimization problems, the complexity of the algorithm is determined mainly by the complexity of function attackCondition, which in turn is determined by the complexity of abstract interpretation. The complexity of applying abstract interpretation with the DeepPoly abstract domain is O(l 2 × n3 *max*) where l is the number of layers, and n*max* is the maximum number of neurons in any of the layers. Let K be the number of images in X. Note that the number of trigger positions is O(h × w), i.e., the size of an image. The best case complexity of Algorithm 2 is O(l 2 × n3 *max* × h × w) and the worst case complexity is O(l 2 × n3 *max* × K × h × w). We remark that in practice, l typically ranges from 1 to 20; n*max* is often advised to be no more than the input size (e.g., from dozens to thousands usually); K ranges from a few to hundreds; and h × w depends on the image resolution (e.g., from hundreds to millions). Thus, in general, Algorithm 2 could be time-consuming in practice and we anticipate further optimization in future work.

The complexity of Algorithm 1 is the complexity of Algorithm 2 times the complexity of the SPRT algorithm. The complexity of the SPRT algorithm is in general hard to quantify and we refer the readers to [1] for a detailed discussion.

#### **3.6 Discussion**

Our approaches are designed to verify the absence of input-agnostic (i.e., not inputspecific) backdoor attacks as presented in Sect. 2. In the following, we briefly review other backdoor attacks and discuss how to extend our approach to support them.

In [12], Gu *et al.* described a backdoor attack which, instead of forcing the network to classify any stamped image with the target label, only alters the label if the original image has a specific ground truth label t*i* (e.g., Bob with the trigger will activate the backdoor and be classified as Alice the manager). Our verification approach can be easily adapted to verify the absence of this attack by focusing on images with label t*i* in Algorithm 1 and Algorithm 2.

Another attack proposed in [12] works by reducing the performance (e.g., accuracy) of the neural network on the images with a specific ground truth label t*i*, i.e., given an image with ground truth label t*i*, the network will classify the stamped image with some label t*s* = t*i*. The attack can be similarly handled by focusing on images with ground truth label t*i*, although due to the disjunction introduced by t*s* = t*i*, the constraints are likely to be harder to solve. That is, we can focus on images with ground truth label t*i* in Algorithm 2, and define an attack to be successful if L(N(I*s*)) = t*i* is satisfied.

In [19], Liu *et al.* proposed to use backdoor triggers with different shapes (i.e., not just in the form of a square or a rectangle). If the user is aware of the shape of the backdoor trigger, a different trigger can be used as input for Algorithm 1 and Algorithm 2 and the algorithms would work to verify the absence of such backdoor. Alternatively, the users can choose a square-shaped backdoor trigger that is larger enough to cover the actual backdoor trigger, in which case our algorithms would remain to be sound, although it might be inconclusive if the trigger is too big.

Multiple groups [2,20,28,35] proposed the idea of poisoning only those samples in the training data which have the same ground truth label as the target label to improve the stealthiness of the backdoor attack. This type of attack is designed to trick the human inspection on the training data, and so does not affect our verification algorithms.

In this work, we consider a specific type of stamping, i.e., the backdoor trigger replaces the part of the original clean image. Multiple groups [6,19] proposed the use of the blending operation as a way of 'stamping', i.e., the features of the backdoor trigger are blended with the features of the original images with some coefficients α. This is a form of input-specific backdoor, the trigger is different for different images. To handle such kind of backdoor attacks, one way is to modify the constraint pre*I* according to the blending operation (assuming that α is known). Since the blending operation proposed in [6,19] is linear, we expect this would not introduce additional complexity to our algorithms.

Input-specific triggers, in general, may pose a threat to our approach. First, some input-specific triggers [19,20] cover the whole image, which is likely to make our approach inclusive due to false alarms resulted from over-approximation. Second, it may not be easy to model some of the input-specific triggers in our framework. For instance, Liu *et al.* [20] recently proposed to use reflection to create stamped images that look natural. Modeling the 'stamping' operation for this kind of attack would require us to know where the reflection is in the image, which is highly non-trivial. However, it should also be noted that input-specific triggers are often not as effective as input-agnostic triggers, e.g., the reflection-based attack reported in [20] are hard to reproduce. Furthermore, as discussed in Sect. 2, backdoor attack with input-specific triggers is an attacking method that is more powerful than adversarial attacks, and the problem of verifying the absence of backdoor attack with input-specific triggers is not yet clearly defined.

#### **4 Implementation and Evaluation**

We have implemented our approach as a self-contained analysis engine in the Socrates framework [26]. We use Gurobi [13] to solve the constraints and use scipy [36] to solve the optimization problems.

We collect a set of 51 neural networks. 45 of them are fully connected ones and are trained on the MNIST training set (i.e., a standard dataset which contains black and white images of digits). These networks have the number of hidden layers ranging from 3 to 5. For each network, the number of neurons in each of its hidden layers ranges from 10 to 50, i.e., 10, 20, 30, 40, or 50. To evaluate our approach on neural networks built with different activation functions, each activation function (i.e., ReLU, Sigmoid, and Tanh) is used in 15 of the neural networks. Among the remaining six networks, three of them are bigger fully connected networks adopted from the benchmarks reported in [32]. They are all built with the ReLU activation function. For convenience, we name the networks in the form of *f k n* where *f* is the name of the activation function, *k* is the number of hidden layers, and *n* is the number of neurons in each hidden layer. The remaining three networks are convolutional networks (which are often used in face recognition systems) adopted from [32]. Although they have the same structure, i.e., each of them has two convolutional hidden layers and one fully connected hidden layer, they are trained differently. One is trained in the normal way; one is trained using DiffAI [22], and the last one is trained using projected gradient descent [7]. These training methods are developed to improve the robustness of neural networks against adversarial attacks. Our aim is thus to evaluate whether they help to prevent backdoor attacks as well. We name these networks *conv*, *conv diffai*, and *conv pgd*.

We verify the networks against the backdoor trigger with shape (1, 3, 3). All the networks are trained using clean data since we focus on verifying the absence of backdoor attacks. They all have precision of at least 90%, except *Sigmoid 4 10* and *Sigmoid 5 10*, which have precision of 81% and 89% respectively. In the following, we answer multiple research questions. All the experiments are conducted using a machine with 3.1Ghz 16-core CPU and 64GB RAM. All models and experiment details are at [27].

*RQ1: Is our realization of* verifyX *effective?* This question is meaningful as our approach relies on Algorithm verifyX. To answer this question, for each network, we select the first 100 images in the test set (i.e., a K of 100 for Algorithm 1, which is more than sufficient) and then apply Algorithm verifyX with these images and each of the labels, i.e., 0 to 9. In total, we have 510 verification tasks. For each network, we run 10 processes in parallel, each of which verifies a separate target. The only exception is the network *ReLU 3 1024*, due to its complexity, we only run five parallel processes (since each process consumes a lot of resources). In each verification process, we filter out those images which are classified wrongly by the network as well as the images which are already classified as the target label.

Figure 4 shows the results. The x-axis show the groups of the networks, e.g., *ReLU 3* means five fully connected networks using the ReLU activation function with three hidden layers; *3 Full* and *3 Conv* mean the three fully connected and the three convolutional networks adapted from [32] respectively. The y-axis shows the number of (network, target) pairs. Note that each group may contain a different number of pairs, i.e., the

**Fig. 4.** The results of verif yX

maximum values for the small network groups are 50, and the maximum values for the last two groups are 30. First, we successfully verify 455 out of 510 verification tasks (i.e., 89%) of them, i.e., the neural network is safe with respect to the selected images. It is encouraging to notice that the verified tasks include all models adopted from [32], which are considerably larger (e.g., with 1024 neurons at each layer) and more complex (i.e., convolutional networks). Second, some networks are not proved to be safe with some target labels. It could be either there is indeed a backdoor trigger that we fail to identify (through optimization), or we fail to verify due to the over-approximation introduced by abstract interpretation. Lastly, with the same structure (i.e., the same number of hidden layers and the same number of neurons in each hidden layer), the networks using the ReLU and Sigmoid activation functions are more often verified to be safe than those using the Tanh activation function. This is most likely due to the difference in the precision of the abstract transformers for these functions.

*RQ2: can we verify the absence of backdoor attacks with a certain level of success rate?* To answer this question, we evaluate our approach on six networks used in RQ1, i.e., *ReLU 3 10*, *ReLU 5 50*, *Sigmoid 3 10*, *Sigmoid 5 50*, *Tanh 3 10*, and *Tanh 5 50*. These networks are chosen to cover a wide range of the number of hidden layers and the number of neurons in each layer, as well as different activation functions. Note that due to the high complexity of Algorithm 1 (which potentially applies Algorithm 2 hundreds of times), running Algorithm 1 on all the networks evaluated in RQ1 requires an overwhelming amount of resources. *Furthermore, since there is no existing work on backdoor verification, we do not have any baseline to compare with.*

Recall that Algorithm 1 has two important parameters K and θ, both of which potentially have a significant impact on the verification result. We thus run each network with four different settings, in which the number of images K is set to be either 5 or 10, and the success rate θ is either 0.8 or 0.9. In total, with 10 target labels, we have a total of 240 verification tasks for this experiment. Note that some preliminary experiments are conducted before we select these two K values.

**Fig. 5.** Verification results

We use all the 10000 images in the test set as the image population and randomly choose K images in each round of test. When a trigger is generated, the success rate of the trigger is validated on the images in the test set (after the above-mentioned filtering). Like in RQ1, we run each network with 10 parallel processes, each of which verifies a separate target. As the SPRT algorithm may take a very long time to terminate, we set a timeout for each verification task, i.e., 2 h for those networks with three hidden layers, and 10 h for those networks with five hidden layers.

The results are shown in Fig. 5. The x-axis shows the networks, the y-axis shows the number of verified pairs of network and target label. We have multiple observations based on the experiment results. First, a quick glance shows that with the same structure and hypothesis testing parameters, more networks built with the ReLU activation function are verified than those built with the Sigmoid and Tanh functions. Second, we notice that the best result is achieved with K = 5 and θ = 0.9. With these parameter values, we can verify that three networks *ReLU 3 10*, *ReLU 5 50*, and *Sigmoid 3 10* are safe with respect to all the target labels and the network *Sigmoid 5 50* is safe with respect to nine over 10 target labels. If we keep the same success rate as 0.9 and increase the number of images K from 5 to 10, we can see that the number of verified cases in the network *Sigmoid 5 50* decreases. This is because when we increase the number of images that must be attacked successfully together, the probability that we do not have the attack increases, which means we need more rounds of test to confirm the hypothesis H0 and so the verification process for the network *Sigmoid 5 50* times out before reaching the conclusion. We have a similar observation when we keep the number of images K at 5 but decrease the success rate from 0.9 to 0.8. When the success rate decreases, the probability of not having the attack increases, which requires more tests to confirm the hypothesis H0. As a result, for all these four networks, there are multiple verification tasks that time out before reaching the conclusion. However, we notice that there is an exception when we keep the success rate as 0.8 and increase the number of images from 5 to 10. While the number of verified cases for the network *ReLU 5 50* decreases (which can be explained in the same way as above), the number of verified cases for the network *Sigmoid 3 10* increases (and the results for the other two

**Fig. 6.** The running time of the experiments in RQ1 with benchmark networks

networks do not change). Our explanation is that when we increase the number of images K to 10, it is easier for the Algorithm 2 to conclude that there is no attack, and so the Algorithm 1 still collects enough evidence to conclude H0. On the other hand, with the number of images is 5, Algorithm 2 may return a lot of UNKNOWN (due to spurious triggers), and so the hypothesis testing in the Algorithm 1 goes back and forth between the two hypotheses H0 and H1 and eventually times out.

A slightly surprising result is obtained for the network *Tanh 3 10*, i.e., our trigger generation process generates two triggers for the target labels 2 and 5 when the success rate is set to be 0.8. This is surprising as these networks are not generated with backdoor attack. This result can be potentially explained by the combination of the relatively low success rate (i.e., 0.8) and the phenomenon known as universal adversarial perturbations [23]. With the returned triggers, the users may want to investigate the network further and potentially improve it with techniques such as robust training [7,22].

*RQ3: Is our approach efficient time-wise?* To answer this question, we collect the wallclock time to run the experiments in RQ1 and RQ2. For each network, we record the average running time for 10 different target labels. The results for 45 small networks are shown in Fig. 6. The x-axis shows the groups of 15 networks categorized based on their activation functions and the y-axis shows the logarithmic scale of the running time in the form of boxplots (where the box shows the result of 25 percentile to 75 percentile, the bottom and top lines are the minimum and maximum, and the orange line is median). The execution time ranges from 14 s to less than 6 h for these networks. Furthermore, we can see that there is not much difference between the running time of the networks using the ReLU and Sigmoid activation functions. However, the running time of the networks using the Tanh function is one order of magnitude larger than those of the ReLU and Sigmoid networks. The reason is that the Tanh networks have many non-safe cases (as shown in Fig. 4) and, as a result, the verification process needs to check more images at more trigger positions. The running time of those networks adopted from [32] ranges from more than 5 min to less than 4 h, as shown in Table 1. Finally, the running time for each network in RQ2 (i.e., the time required to verify the networks against backdoor attacks) according to different settings is shown in Table 2.

**Table 1.** The running time of the experiments in RQ1 with networks adapted from [32]

**Table 2.** The running time of the experiments in RQ2

*RQ4: can our approach generate backdoor triggers?* Being able to generate counterexamples is a part of a useful verification method. We conduct another experiment to evaluate the effectiveness of our backdoor trigger generation approach. We train a new set of 45 networks that have the same structure as those used for answering RQ1. The difference is that this time each network is trained to contain backdoor through data poisoning. In particular, for each network, we randomly extract 20% of the training data, stamp a white square with shape (1, 3, 3) in one corner of the images, assign a random target label, and then train the neural network from scratch with the poisoned training data. While such an attack is shown to be effective [12], it is not guaranteed to be always successful on a randomly selected set of images. Thus, we do the following to make sure that there exists a trigger for a set of selected images. From 10000 images in the test set, we first filter out those images which are classified wrongly or already classified with the target label. The remaining images are collected into a set X0. Next, to make sure that the selected images have a high chance of being attacked successfully, we apply another filter on X0. This time, we stamp each image in X0 with a white square at the same trigger position as we poison the training data. We then keep the image if its stamped version is classified by the network with the target label. The remaining images after the second filter are collected into another set X. We apply our approach, in particular, the backdoor trigger generation on X, if |X|÷|X0| ≥ 0.8, i.e., the backdoor attack has a success rate of 80%.

The results are shown in Fig. 7 in which the y-axis shows the number of networks. The timeout is set to be 120 s. Among the 45 networks, we can see that a trigger is successfully generated for 33 (i.e., 73%) of the networks. A close investigation of these networks shows that the generated trigger is the exact white square that is used to stamp the training data. There are 12 networks for which the trigger is not generated. We

**Fig. 7.** The results of backdoor trigger generation

investigate these networks and see that they are either too biased (i.e., classifying every image with the target label and thus |X0| = 0) or the attack on these networks does not perform well (i.e., |X|÷|X0| < 0.8). In other words, the backdoor attack on these networks failed and, as a result, the generation process does not even begin with these networks. In a nutshell, we successfully generate the trigger for every successful backdoor attack. Finally, note that the running time of the backdoor generation process is reasonable (i.e., on average, 50 s to generate a backdoor trigger for one network) and thus it does not affect the overall performance of our verification algorithm.

# **5 Related Work**

The work which is closest to ours is [37] in which Wang *et al.* aim to certify neural networks' robustness against backdoor attack using randomized smoothing. However, there are many noticeable differences between their approach and ours. First, while our work focuses on verifying the absence of backdoor, their work aims to certify the robustness of individual images based on the provided training data and learning algorithm (which can be used to implicitly derive the network). Second, by using random noises to estimate the networks' behaviors, their approach can only obtain very loose results. As shown in their experiments, they can only certify the robustness against backdoor attack with triggers contains two pixels and on a "toy" network with only two layers and two labels, after simplifying the input features by rounding them into 0 or 1. Compare to their approach, our approach can apply to networks used to solve real image classification problems as shown in our experiments.

Our work is closely related to a line of work on verifying neural networks. Existing approaches mostly focus on local robustness property and can be roughly classified into two categories: exact methods and approximation methods. The exact methods aim to model the networks precisely and solve the verification problem using techniques such as mixed-integer linear programming [34] or SMT solving [8,15]. On the one hand, these approaches can guarantee sound and complete results in verifying neural networks. On the other hand, they often have limited scalability and thus are limited to small neural networks. Moreover, these approaches have difficulty in handling activation functions except the ReLU function.

In comparison, the approximation approaches over-approximate neural network behavior to gain better scalability. AI2 [10] is the first work pursuing this direction using the classic abstract interpretation technique. After that, more researchers try to explore different abstract domains for better precision without sacrificing too much scalability [29,30,32]. In general, the approximation approaches are more scalable than the exact methods, and they are capable of handling activation functions such as Sigmoid and Tanh. However, due to the over-approximation, these methods may fail to verify a valid property.

We also notice that it is possible to incorporate abstraction refinement to the approximation methods and gain better precision, for instance, by splitting an abstraction into multiple parts to reduce the imprecision due to over-approximation. There are many works [21,40,41] which fall into this category. We remark that our approach is orthogonal to the development of sophisticated verification techniques for neural networks.

Finally, our approach, especially the part on backdoor trigger generation, is related to many approaches on generating adversarial samples for neural networks. Some representative approaches in this category are FGSM [11], JSMA [24], and C&W [4] which aim to generate adversarial samples to violate the local robustness property, and [42] which aims to violate fairness property.

#### **6 Conclusion**

In this work, we propose the first approach to formally verify that a neural network is safe from backdoor attacks. We address the problem on how to verify the absence of a backdoor that reaches a certain level of success rate. Our approach is based on abstract interpretation and we provide an implementation based on DeepPoly abstract domain. The experiment results show the potential of our approach. In the future, we intend to extend our approach with more abstract domains as well as improve the performance to verify more real-life networks. Besides that, we also intend to apply our approach to verify the networks designed for other tasks, such as sound or text classification.

**Acknowledgements.** This research is supported by the Ministry of Education, Singapore under its Academic Research Fund Tier 3 (Award ID: MOET32020-0004). Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not reflect the views of the Ministry of Education, Singapore. This research is also partly supported by the Starry Night Science Fund of Zhejiang University Shanghai Institute for Advanced Study, Grant No. SN-ZJU-SIAS-001.

#### **References**

**Open Access** This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

# Trainify**: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning**

Peng Jin1, Jiaxu Tian1, Dapeng Zhi1, Xuejun Wen2, and Min Zhang1,3(B)

1 Shanghai Key Laboratory of Trustworthy Computing, ECNU, Shanghai, China

<EMAIL_ADDRESS>2 Huawei International, Singapore, Singapore 3 Shanghai Institute of Intelligent Science and Technology, Tongji University, Shanghai, China

**Abstract.** Deep Reinforcement Learning (DRL) has demonstrated its strength in developing intelligent systems. These systems shall be formally guaranteed to be trustworthy when applied to safety-critical domains, which is typically achieved by formal verification performed after training. This *train-then-verify* process has two limits: (i) trained systems are difficult to formally verify due to their continuous and infinite state space and inexplicable AI components (*i.e.*, deep neural networks), and (ii) the *ex post facto* detection of bugs increases both the time- and money-wise cost of training and deployment. In this paper, we propose a novel verification-in-the-loop training framework called Trainify for developing safe DRL systems driven by counterexample-guided abstraction and refinement. Specifically, Trainify trains a DRL system on a finite set of coarsely abstracted but efficiently verifiable state spaces. When verification fails, we refine the abstraction based on returned counterexamples and train again on the finer abstract states. The process is iterated until all predefined properties are verified against the trained system. We demonstrate the effectiveness of our framework on six classic control systems. The experimental results show that our framework yields more reliable DRL systems with provable guarantees without sacrificing system performance such as cumulative reward and robustness than conventional DRL approaches.

**Keywords:** Deep reinforcement learning · Model checking · CEGAR · ACTL

# **1 Introduction**

Deep Reinforcement Learning (DRL) has shown its strength in developing intelligent systems for complex control tasks such as autonomous driving [37,40]. Verifiable safety and robustness guarantees are crucial to these safety-critical DRL systems before deploying [23,44]. A typical example is autonomous driving, which is arguably still a long way off due to safety concerns [21,39]. Recently, tremendous efforts have been made toward adapting existing and devising new formal methods for DRL systems in order to provide provable safety guarantees [18,25,45,46,51].

Formally verifying DRL systems is still a challenging problem. The challenge arises from DRL systems' three features. First, the state space of a DRL system is usually continuous and infinite [28]. Second, the behavior of a DRL system is non-linear and determined by high-order system dynamics [17]. Last but not least, the controllers, typically deep neural networks (DNN), are almost inexplicable because of their black-box development [20,52]. The three features make it unattainable to verify DRL systems using conventional formal methods, *i.e.*, modeling them as state transition systems and verifying temporal properties using dedicated decision procedures [4]. Most existing approaches have to simplify the problem by abstraction or over-approximation techniques and restrict to specific properties such as safety or reachability [46].

Another common problem with most existing formal verification approaches to DRL systems is that they are applied after the training is concluded. These *train-then-verify* approaches have two limitations. First, verification results may be inconclusive due to abstraction or overestimation. The non-linearity of both system dynamics and deep neural networks makes it difficult to control the overestimation in a reasonable range, resulting in false positives in verification results [50]. Second, the *ex post facto* detection of bugs increases both the timeand money-wise cost of training and deployment. No evidence shows that the iterative training and verification help improve system reliability, as tuning the parameters in neural networks may cause an unpredictable impact on the properties because of the inexplicability [24].

To address the challenges in training and verifying DRL systems, in this paper we propose a novel *verification-in-the-loop* framework for training safe and reliable DRL systems with verifiable guarantees. Provided that a set of properties are predefined for a target DRL system to develop, our framework trains the system and verifies it against the properties in every iteration. To overcome the verification challenges in DRL systems, for the first time, we propose a novel approach in our framework to train the systems on a finite set of *abstract states*, based on the observation that *approximate abstractions can still preserve near-optimal behavior* [1]. These states are the abstractions of the actual states. Training on the finite abstract states allows us to model the AI-embedded systems as finite-state transition systems. We can leverage classic model checking techniques to verify their more complicated temporal properties than safety and reachability.

As system performance may be affected by the abstraction granularity, we employ the idea of the counterexample-guided abstraction and refinement (CEGAR) [8] in model checking along the training process. We start with a coarsely abstracted but efficiently verifiable state space and train and verify DRL systems on the abstract state space. Once verification fails, we refine the abstract state space based on the returned counterexamples and retrain the system on the finer-grained refined state space. The process is repeated until all the properties are verified successfully. We, therefore, call the training and verification framework *CEGAR-driven*, by which we can reach an appropriate abstraction granularity that guarantees both system performance and verification scalability.

Our verification-in-the-loop training framework has four advantages compared with conventional DRL training and verification approaches. Firstly, our approach produces correct-by-construction DRL systems that are verifiably safe with respect to user-defined safety requirements. Secondly, more complicated properties such as safety and liveness can be verified thanks to the dedicated training approach on abstracted state space. Another advantage of the training approach is that it is orthogonal to state-of-the-art DRL algorithms such as Deep Q-Network (DQN) [34] and Deep Deterministic Policy Gradient (DDPG) [32]. Thirdly, our approach provides a flexible mechanism for fine-tuning an appropriate abstraction granularity to balance system performance and verification scalability. Lastly, training on abstract states renders DRL systems to be more robust against adversarial and environmental perturbations because small perturbation to an actual state may not alter the decision of the neural network on the same abstract state.

We implement a prototype tool called Trainify (abbreviated for Train and Verify, available at https://github.com/aptx4869tjx/RL verification). We perform extensive experiments on six classic control tasks in public benchmarks to evaluate the effectiveness of our framework. For each task, we train two DRL systems under the same settings in our approach and corresponding conventional DRL algorithm, respectively. We compare the two systems in terms of the properties that they shall satisfy and the performance in terms of cumulative reward and robustness. Experimental results show that the systems trained in our approach are more efficient to verify and more reliable than those trained in conventional methods; moreover, their performance is competitive and higher.

In summary, this paper makes the following three major contributions:

*Paper Organization.* Section 2 briefly introduces deep reinforcement learning. Section 3 presents the model-checking problem of DRL systems. Section 4 presents our training and verification framework. Section 5 shows six case studies and experimental results. Section 6 mentions some related work, and Sect. 7 concludes the paper.

# **2 Deep Reinforcement Learning (DRL)**

DRL is a technique for learning optimal control policies using deep neural networks according to evaluative feedback [31]. An agent in a DRL system interacts with the environment and records its state st at each time step t. It feeds st into a deep neural network to compute an action at and transitions to the next state st+1 according to at and the system dynamics. The system dynamics describe the non-linear behavior of the agent over time. The agent receives a scalar reward according to reward functions. Some algorithms estimate the distance between the action determined by the network and the expected action in the same state. Then, it updates the parameters in the network according to the estimated distance to maximize the cumulative reward.

#### *A Running Example.*

Figure 1 shows a classic DRL task of learning a control policy to drive a car to the right hilltop. The car is initially positioned on a track between two mountains. The track is one-dimensional, and thus the car's position is represented as a real num-

**Fig. 1.** A DRL example of mountain car system.

ber. Velocity is another dimension in the car's state and is represented as a real number too. Thus, the car's state is a pair (p, v) of position p and velocity v. An action a is a real number representing the force imposed on the car. The action is computed by a neural network on both p and v.

The sign of a means the direction of the force, *i.e.*, positive for the right and negative for the left, respectively. Given a state st = (pt, vt) and an action at at time step t, the system transitions to the next step st+1 = (pt+1, vt+1) following the given dynamics:

$$p\_{t+1} = p\_t + v\_t \Delta\_t,\tag{1}$$

$$v\_{t+1} = v\_t + (a\_t - m\_c \times g \times \cos(3p\_t))\Delta\_t,\tag{2}$$

where mc denotes the car's mass, g denotes the gravity, and Δt is the unit interval between two consecutive steps. In DRL, time is usually discretized to facilitate implementation. The car is assumed to move in uniform motion during a unit interval.

*Reward Setting.* The reward function R maps state st, action at and state st+1 to a real number, which represents the rewarded value by applying at to st to transition to st+1. The purpose of R is to guide the agent to achieve the preset goals by making cumulative reward as great as possible. The definition of R is based on prior knowledge or expert experience before training.

In the Mountain Car example, the controller receives the reward which is defined as R(pt, vt, at,pt+1, vt+1) = −1.0 at each time step when pt+1 < 0.45. The reward is a negative constant because the goal in this example is to force the car to reach the right hilltop (p = 0.45) as quickly as possible. If the corresponding cumulative reward value is larger than another when the car reaches the destination, it means that the car takes fewer steps. A reward function can be a more complex formula than a constant when the reward strategy is related to states and actions.

*Training.* The essence of DRL training is to update parameters in neural networks so that the networks can compute optimal actions for input states. A deep neural network is a directed graph comprised of an input layer, multiple hidden layers, and an output layer, as shown in Fig. 2. Each layer contains several nodes called *neurons*. They are connected to the neurons on the following layer. Each edge has a weight. The values passed on the edge are multiplied by the weight. A neuron on

**Fig. 2.** A simple neural network.

hidden layers takes the sum of all the incoming values, adds a bias, and feeds the result to its activation function σ. The output of σ is passed to the neurons on the following layer. There are several commonly used activation functions, e.g., ReLU (σ(x) = max(x, 0)), Sigmoid (σ(x) = 1 1+e−x ) and Tanh (σ(x) = ex−e−x ex+e−x ), etc. In DRL, the inputs to a neural network are system states. The outputs are (probably continuous) actions that shall be performed to the present state.

During training, agents continuously interact with the environment to obtain trajectories. A trajectory is a 4-tuple, consisting of a state s, the action a on s, the reward of executing a on s, and the successor state after the execution. A predefined loss function uses the collected trajectories to estimate an action value and compute the distance between the estimated value and the one computed by the neural network for the same state. Guided by the distance, the parameters in the network are updated using gradient descent algorithms [12]. The process is repeated until the system reaches a predefined maximal iteration limit or a preset cumulative reward threshold.

#### **Algorithm 1:** Training for the Mountain Car Task using DQN

There are several well-established training algorithms, such as Deep Q-Network (DQN) [35] and Deep Deterministic Policy Gradient (DDPG) [32]. Algorithm 1 depicts a high-level process of training the mountain car using DQN. We call the process of training the car to move from the initial position to the destination an *episode*. For each episode, the initial state is firstly determined (Line 2). Then, the controller determines the action to be adopted based on the current state st and the neural network N (Line 4). After performing the action, the controller receives a reward value (−1.0 in this case) and transitions to the next state based on the system dynamics (Line 5). A loss is estimated by calling the loss function L with partially sampled trajectories. The loss is represented by P (Line 6) used to update the parameters of the network N (Line 7). We omit the details of L, as it is not the emphasis of our paper.

*The Target DRL Systems in this Work.* The types of DRL systems are diverse from different perspectives, such as the availability of system dynamics [17] and the determinism of actions. In this work, we assume system dynamics is prior knowledge for training, and the actions are deterministic. That is, a unique action is determined to take on the present state, and its successor state is also uniquely determined by system dynamics.

# **3 Model Checking of DRL Systems**

#### **3.1 The Model Checking Problem**

A trained deterministic DRL system can be represented as a tuple M = (S, A, f, π, S0, L), where S is the state space which is usually infinite, S0 ⊆ S is the initial state space, A is a set of actions, f : S × A → S is the system dynamics, π : S → A is a policy function, and L : S → 2AP is a state labeling function. In this work, we use π to denote the policy that is implemented by the trained deep neural network in the system.

The model M of a DRL system is essentially a Kripke structure [10], which is a 4-tuple (S, R, S0, L). Given two arbitrary states s, s in S, there is a transition from s to s , denoted by (s, s ) ∈ R, if and only if there is an action a in A such that a = π(s) and s = f(s, a). Given that a property is formalized by a formula Φ in some logic, the model checking problem of the system is to decide whether M satisfies Φ, denoted by M |= Φ.

In this work, we formulate properties in ACTL [4], a segment of CTL where only universal path quantifiers are allowed and negation is restricted to atomic propositions [14,15]. ACTL consists of state formula Φ and path formula ϕ in the following syntax:

$$\begin{array}{lclclcl}\Phi & ::= & true & false & a & \mid \neg a & \mid \Phi\_1 \land \Phi\_2 & \mid \Phi\_1 \lor \Phi\_2 & \mid \: A \,\varphi, \\\varphi & ::= & X\,\Phi & \mid \: \Phi\_1 \; U\,\Phi\_2 & \mid \: \Phi\_1 \; R\,\Phi\_2. \end{array}$$

The temporal operators fall into two main categories, *i.e.*, quantifiers over paths and path-specific quantifiers. In ACTL, only the universal path quantifier A is considered. Path-specific quantifiers refer to X, U and R.

Using the above basic temporal operators, we can define another two important path-specific quantifiers G (*globally*) and F (*finally*) with G Φ = *false* R Φ and F Φ = *true* U Φ. Intuitively, G Φ means that Φ has to hold on the entire subsequent path, and F Φ means that Φ eventually has to hold (somewhere on the subsequent path).

We choose ACTL to formulate system properties or requirements in our framework for two main reasons. Firstly, in our framework, we rely on refinement to the abstract states where system properties are violated. Such states can be obtained as counterexamples returned by model checkers when the system properties defined in ACTL are verified not valid by model checking. Secondly, the verification results of ACTL formulas can be preserved by property-based abstraction [9,11]. Such preservation is vital to ensure the correctness of our verification results because the abstraction is necessary for our framework to guarantee the scalability of the verification algorithm.

#### **3.2 Challenges in Model Checking DRL Systems**

Unlike the model checking problems for finite-state systems, model checking M |= Φ for DRL systems is particularly challenging. The challenge arises from the three features of DRL systems, *i.e.*, (i) the infinity and continuity of state space S, (ii) the non-linearity of system dynamics f, and (iii) the inexplicability of the policy π that is encoded as deep neural networks. Usually, the state space of DRL systems is continuous and infinite, and behaviors are non-linear due to high-order system dynamics. Even worse, the actions of states are determined by inexplicable deep neural networks, which means that the transitions between states cannot be defined as straightforwardly as those of traditional software systems.

To build a model M for a DRL system, we have to compute the successor of each state s by applying the neural network π on s to compute the action a and then performing a to s according to the system's dynamics f. Specifically, the successor of s can be represented as f(s, π(s)). The non-linearity of both f and π and the infinity of S makes the verification problem difficult. Most existing approaches rely on the over-approximation of f and π to simplify the problem [16,25,29,46]. However, over-approximation inevitably introduces overestimation and restricts to only safety properties and reachability analysis in bounded steps.

# **4 The CEGAR-Driven DRL Approach**

#### **4.1 The Framework**

Figure 3 shows the overview of our framework. It consists of three parts, *i.e.*, training, verification and refinement. In the training part, a DRL system is trained on a finite set of abstract states. An actual state is first mapped to its corresponding abstract state, then fed into the neural network to compute a corresponding action. The action is applied to the actual state to drive the system to transition to the next state. The reward is accumulated according to a predefined reward function, and the neural network is updated in the same way as conventional DRL algorithms. In the verification part, we build a Kripke structure on the finite abstract state space based on the trained neural network. Then, we verify the desired properties that are predefined in ACTL formulas Φ. If all the properties are verified valid, we stop training, and a DRL system is developed. If some property is verified not valid, we move to the refinement part. When verification fails, counterexamples are returned. They are the abstract states where the property is violated. We refine these states by subdividing them into fine-grained sub-states and substitute those *bad* states. We resume to train the system on the refined abstract state space and repeat the whole process.

**Fig. 3.** The training, verification and refinement framework for developing DRL systems.

The integration of training, verification and refinement seamlessly constitutes a *verification-in-the-loop* DRL approach, driven by the counterexample-guided abstraction and refinement. We start with a coarse abstraction. After every training episode, we model check the system against all the predefined properties. If all the properties are verified, we stop training and obtain a verified system. Otherwise, counterexamples are returned. The abstract state space is refined for further training. After several iterations, a DRL system is trained with all the predefined properties rigorously verified.

#### **4.2 Training on Abstract States**

DRL is a process of learning optimal actions on all system states for specific objectives. A trained model partitions the state space into a family of sets such that the same action is taken in the states from a set [38]. Continuous state spaces can be adaptively discretized into finite ones for learning without affecting learning performance [41,42]. Motivated by this observation, we discretize a continuous state space into a finite set of fragments. We call each fragment an abstract state and train the DRL system by feeding abstract states into the deep neural network for decision making.

**Fig. 4.** An example of encoding an abstract state space into an R-tree.

*System State Abstraction.* Given an n-dimension DRL system, a concrete system state s is represented as a vector of n real numbers. Each number has a physical meaning about the system, such as speed and position in the running example. Let Li and Ui be the lower and upper bounds for the i-th dimension value of S. Then, the state space S of the control system is Πn i=1[Li, Ui].

Initially, we use interval boxes to discretize S. An interval box I is a vector of n intervals, denoted by (I1, I2,...,In). Each interval Ii(1 ≤ i ≤ n) represents all the system states, denoted by SIi , where a state s belongs to SIi if and only if the i-th value in s is in Ii. An interval box I represents the intersection of all the sets SIi (i = 1,...,n).

Let di ∈ R (0 < di ≤ Ui − Li) be the diameter by which we subdivide evenly the interval [Li, Ui] in each dimension i into (Ui − Li)/di unit intervals, and Ii = [Li, Ui]/di denote the set of all the unit intervals. Then, we obtain the abstract state space **S** = I1 × ... × In, which is an abstraction of the infinite continuous state space S. We call the vector (d1, d2,...,dn) of the n diameters *abstraction granularity* and denote it by δ.

Given a continuous state space S and its corresponding abstract state space **S**, we call the mapping function from the states in S to the corresponding abstract states in **S** a *transformer* A : S → **S**. The transformer can be encoded as an R-tree, a tree-like data structure devised for efficiently indexing multidimensional objects [22]. Figure 4 depicts an example of building an R-tree to index an abstract state space of the continuous space [v0, v4] × [p0, p5]. A rectangle on a leaf node represents an abstract state, and the one on a non-leaf node represents the minimum bounding rectangle enclosing all the rectangles on its child nodes. There can be multiple rectangles on a single node. R-tree supports intersection search, *i.e.*, searching for the abstract states that intersect with the interval we are querying. Given a concrete state, an R-tree can quickly return its corresponding abstract state. Note that in Fig. 4, we assume state space is discretized evenly for clarity. During training, the size of abstract states becomes diverse after iterative refinement, and the R-tree should be updated correspondingly.

*The Training Algorithms.* The algorithms for training on abstract states can be achieved by extending existing DRL algorithms such as DQN and DDPG. The extension can be easily achieved by adapting the neural networks and loss functions in DRL systems so that they can admit abstract states as inputs.

For neural networks, we only need to modify the input layer by doubling the number of neurons on the input layer, denoted by N . Given an n-dimension system, we declare 2n neurons. Each pair of neurons read the lower and upper bounds of an interval in an abstract state, respectively. This dedicated structure guarantees that a trained network can produce the same action for all the states that correspond to the same abstract state.

Figure 5 shows an example of adapting the network in the Mountain Car for training it on abstract states. For traditional DRL algorithms, two input neurons are needed in the neural network to take p and v as inputs, respectively. To train on abstract states, four input neurons are needed to take the lower and upper bounds of the position and velocity intervals in abstract states. For instance, let the interval box (Ip, Iv) be the abstract state of (p, v). Then, the lower bounds Ip, Iv and the upper bounds Ip, Iv of p, v

**Fig. 5.** Adapting neural networks for abstract states.

are input to the four neurons, respectively. Apparently, this adaption guarantees that the neural network always produces the same action on the states that are transformed into the same abstract state.

We consider incorporating these two steps to extend Algorithm 1 as an illustrative example. Algorithm 2 depicts the main workflow where the differences are highlighted. The main difference from the traditional training process lies in line 6. Given a concrete state s = (s1,...,sn), A will return the abstract state **s** = ([l1, u1],..., [ln, un]) such that li ≤ si ≤ ui with i = 1,...,n, which is also the result fed into neural network. Although the dimension of input states increases, the form of corresponding output actions does not change. Therefore, the loss function can naturally adapt to changes in input states.

#### **4.3 Model Checking Trained DRL Systems**

A DRL system can be naturally verified using abstract model checking [26]. The actual states of the system are first abstracted in the same way used in training, and then the transitions between abstract states are determined by the corresponding action and dynamics. ACTL formulas are then model checked on the abstract state transition system.

*Building Kripke Structure.* During the training phase, the actual state space has already been abstracted into a finite set **S** of abstract states. Therefore, the main task for abstract model checking is to build a Kripke structure by defining the transition relation on **S**.

Algorithm 3 depicts the process of building a Kripke structure K for a trained DRL system. Firstly, K is initialized on set **S** with R being empty. Starting from an initial abstract state **s**0, we compute its successors and define the transitions from **s**0 to them. We repeat the process until all reachable states are traversed.

Given an abstract state **s**, we compute its abstract successor states by applying the corresponding action a and the dynamics to **s**. Because the system is trained on abstract states, all the actual states in **s** have the same action, *i.e.*, a = N (**s**). Let f ∗(**s**, a) = {f(s, a)|s ∈ **s**} be the set of all the successors of the actual states in **s**. Due to the nonlinearity of f and the infinity of **s**,

**Algorithm 3:** Building Kripke Structure **Input:** Initial state **s**0, state space **S**, system dynamics f, neural network N **Output:** A Kripke Structure K **1** K = Initialize Kripke Structure() **2** Queue ← {**s**0} **3 while** *Queue is not empty* **do 4** Fetch **s** from Queue **5 for** i = 1,...,n **do 6** [li, ui] ← g(f(**s**, N (**s**)), i) **7** {**s**1,..., **s**m} := h([l1, u1],..., [ln, un], **S**) **8 for** j = 1,...,m **do 9** K.add edge(**s** → **s**j ) **10 if s**j *is not traversed* **then 11** Push **s**j into Queue **12 return** K

we over-approximate the set f ∗(**s**, a) = {f(s, a)|s ∈ **s**} as an interval box. As shown in Fig. 6, the dashed box is an over-approximation of f ∗(**s**, a). The overapproximation may overlap one or more abstract states, e.g., **s**1,..., **s**4 in the example. All the overlapped abstract states are successors of **s**. In Algorithm 3, function g calculates the interval box and function h determines the overlapped abstract states. Note that the shapes of abstract states may be different because they are refined during training, which is to be detailed in Sect. 4.4.

We use an interval to approximate the i-th dimension's values in all the successor states. Then, all the successor states are approximated as a vector of n intervals. We can compute the upper and lower bounds for each i by solving the following two optimization problems, respectively:

**Fig. 6.** Transitions between abstract states

$$\begin{aligned} \underset{s \in \mathbf{s}}{\arg\max} & \quad v\_i \cdot f(s, \mathcal{N}'(\mathbf{s})) \\ \underset{s \in \mathbf{s}}{\arg\min} & \quad v\_i \cdot f(s, \mathcal{N}'(\mathbf{s})) \end{aligned}$$

where, vi is a one-hot vector with the i-th element being 1. Because all the states in **s** have the same action according to the network, N (**s**) in the above optimization problems can be substituted for a constant, *i.e.*, the action taken by the system on all the states in **s**. The substitution significantly simplifies the optimization problems; no information of the networks is needed in the simplified problems. The simplified problems can be efficiently solved using off-the-shelf scientific computing tools such as SciPy [48].

We consider an example in the mountain car system. We assume that the current abstract state **s** is ([0, 0.2], [0, 0.02]) and the adopted action is 0.001, which says that the controller accelerates to the right for all states in **s**. Based on the dynamics defined by Eq. 1, we can compute the upper bounds of both position and velocity in the next step by solving the following two optimization problems:

$$\underset{p\_t \in [0, 0.2], v\_t \in [0, 0.02]}{\text{arg}\max} \quad p\_t + v\_t \tag{p\_{t+1}}$$

$$\underset{p\_t \in [0, 0.2], v\_t \in [0, 0.02]}{\arg\max} \quad v\_t + 0.001 - 0.0025 \cos(3p\_t) \tag{5.41}$$

The lower bounds of pt+1 and vt+1 are calculated similarly. Then, we obtain an abstract state **s** = ([0, 0.22], [−0.0035, 0.0165]), which is an overestimated set of all the actual successors of the states in **s**. There is a transition from **s** to any abstract state **s** = ([p, p], [v, v]) in **S**, if **s** and **s** overlap, *i.e.*, (0< p < 0.22∨0< p <0.22) ∧ (−0.0035< v <0.0165 ∨ −0.0035<v <0.0165) is true. Note that the transition from **s** to **s** includes all the transitions between the actual states in **s** and **s** , respectively. It may also include those that do not actually exist due to the overestimation.

There are other approaches for over-approximating the set f ∗(**s**, a), such as template polyhedrons like rectangle and octagon [2]. Note that there is always a trade-off between the tightness of the polyhedral and the efficiency of computing it. For instance, an octagon can approximate the set more tightly than a rectangle. However, it costs double effort to compute the borders. The tighter an over-approximation is, the more accurate the set of computed successors is, but the more time it costs to compute the approximation.

*Property-Based Abstraction.* For those high-dimensional DRL systems, the abstract state space may be still too huge to model check directly when the abstraction granularity becomes small after refinement. To improve the model checking scalability, we further abstract the constructed Kripke structure based on the ACTL formula Φ to be model checked using the abstraction approach in the work [9].

**Definition 1 (State Abstraction).** *Given an abstract state space* **S** = I1 × ..., ×In *and an ACTL formula* Φ*, let* DΦ *be the set of dimensions that occur in* Φ *and* **S**- = Πd∈DΦ Id*. Function* αΦ : **S** → **S** *is an abstract transformer such that for every* **s** ∈ **S** *and* **s** ∈ **S**-*,* **s** = αΦ(**s**) *if and only if* **s**[d] = **s**[d] *for all* d ∈ DΦ*.*

Given a Kripke structure K = (**S**, R, **S**0, L) and an ACTL formula Φ, let αΦ : **S** → **S** be the abstract transformer, and AP ⊆ AP be all the atomic propositions in Φ. We can construct the following abstract Kripke structure K- = (**S**-, R, - **S**-0,L-) based on αΦ, where:

– **S**- = Πd∈DΦ Id; – R- = {(αΦ(**s**), αΦ(**s** ))|**s**, **s** ∈ **S**.(**s**, **s** ) ∈ R}; – **S**-0 = {αΦ(**s**) | **s** ∈ **S**0}; – L- : **S**- → 2AP such that L-(**s**) = L(**s**) ∩ AP where **s** ∈ **S** and **s** = αΦ(**s**). We call K-

 a simulation of K with respect to Φ. An important property of the simulation is that the property represented by Φ is preserved by the abstract model K-. **Theorem 1 (Soundness).** *Let* K-

 *be a simulation of* K *with respect to an ACTL formula* Φ*,* K-|= Φ *implies* K |= Φ*.*

The proof of Theorem 1 is straightforward. We omit the proof due to space limit. According to the theorem, we can conclude that K |= Φ holds whenever we find a simulation K of K and model check that K-|= Φ holds.

**Fig. 7.** An example of refinements on abstract states where properties are violated.

#### **4.4 Counterexample-Guided Refinement**

If a formula Φ is verified not true, our algorithm returns corresponding counterexamples. A counterexample is an abstract state where Φ is violated. We refine the abstract state into finer ones and substitute them in the abstract state space for further training.

A na¨ıve refinement approach subdivides each dimension of states into two intervals. Assuming that a property is violated on an abstract state **s** = ([l0, u0],..., [ln, un]), we can simply divide each dimension evenly into two intervals ([li,(li + ui)/2], [(li + ui)/2, ui]), and obtain 2n finer abstract states. Apparently, the refinement may lead to state space explosion, particularly for highdimensional systems.

In our approach, we only refine the states on the dimensions that are used to define the properties being verified to avoid state explosion. Considering the mountain car example, we assume that the formula is AF[p ≥ 0.45], saying that the car will eventually reach the hilltop where p = 0.45. Suppose that the property fails and counterexamples are returned. We assume **s** = ([0, 0.2], [0, 0.02]) is the state where the property is violated, as shown in Fig. 7 (a). We bisect the state into two fine-grained sub-states, **s**1 = ([0, 0.1], [0, 0.02]) and **s**2 = ([0.1, 0.2], [0, 0.02]). Then, we substitute the two fine-grained states for **s** on the R-tree for further training. Figure 7 (b) shows the new R-tree after the substitution.

It is worth mentioning that counterexamples may be false positives. Abstract states may include the actual states that are unreachable in the trained system because of the approximation of system dynamics. Unfortunately, it is difficult to check which states are actually unreachable because we need to know their corresponding initial state to check the reachability of these bad states. However, the corresponding initial state is *enclosed* in an abstract state and cannot be identified due to the abstraction. In our approach, we perform refinement without checking whether the counterexamples are real or not. After refinement, the abstract states become finer-grained. Counterexamples can be discarded by training and verifying on these finer-grained abstract states. The price of such extra refinements is that more iterations of training and verification are conducted, but the benefit is that the performance of the trained systems is better.

# **5 Implementation and Evaluation**

#### **5.1 Implementation**

We implement our framework into a prototype toolkit called Trainify in Python. In the toolkit, we leverage the open-source library *pyModelChecking* [6] as the back-end model checker and the scientific computing tool SciPy [48] as an optimization solver.

#### **5.2 Benchmarks and Experimental Settings**

We evaluate the effectiveness of our approach on a wide range of classic control tasks from public benchmarks. For each control task, we train two DRL systems using our approach and the corresponding conventional DRL approach, respectively. We compare the two trained systems in terms of their reliability, verifiability and system performance.

*Benchmarks*. We choose six classic control problems. Three of them are from the DRL training platform Gym [5], including Mountain Car, Pendulum and Cartpole. The other three, *i.e.*, B1, B2 and Tora, are the problems that are widely used for evaluation by state-of-the-art tools [19,25,27,28].

*Training Configurations and Evaluation Metrics.* We adopt the same system configurations and training parameters for each task, including neural network architecture, system dynamics, time interval, DRL algorithms and the number of training episodes.

We choose three metrics, including the satisfaction of predefined properties, cumulative reward and robustness, to evaluate and compare the reliability, verifiability and performance of the DRL systems trained in our approach and those trained in the conventional DRL approach for the same task. The first metric is about reliability and verifiability. The other two are about performance. The cumulative reward is an important figure to evaluate a trained system's performance because maximizing the cumulative reward is the objective of learning. Robustness is another essential criterion for DRL systems because the systems are expected to be robust against perturbations from both the environment and adversarial attacks. Note that we classify robustness into performance category instead of reliability because we restrict the reliability of DRL systems to the safety and functional requirements.

*Experimental Settings.* All experiments are conducted on a workstation running Ubuntu 18.04 with a 32-core AMD Ryzen Threadripper CPU @ 3.7 GHz and 128 GB RAM.

#### **5.3 Reliability and Verifiability Comparison**