Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding (Extended Abstract)

1 Introduction

Deep neural networks (DNNs) could be vulnerable to small adversarial perturbations on their inputs [Biggio et al., 2013]. The formally-defined robustness metric of a DNN tries to bound such uncertain behavior, measuring how much the network's output may deviate when its input has a bounded perturbation. The local robustness problem has been extensively studied, with formal methods developed to bound the output range for a bounded disturbance around a given input [Katz et al., 2017; Singh et al., 2019; Huang et al., 2020b; Zhang et al., 2018; Wang et al., 2021a]. However, it is hard to apply these techniques in safety verification of a dynamic system (e.g., an autonomous vehicle) [Zhu et al., 2020; Wang et al., 2021d; Liu et al., 2022] as we will need to conduct local robustness analysis during runtime for each input sample that the system encounters or may encounter, and they are typically too computationally expensive for that.

This challenge motivates us to address the safety of DNNenabled dynamic systems by considering the problem of global robustness, which measures the worst-case DNN output deviation against bounded perturbation for all possible input values. We can conduct such worst-case analysis offline, decoupling it from the safety verification [Huang et al., 2019; Fan et al., 2020; Huang et al., 2022] by applying the maximum deviation for all possible inputs. However, the previous MILP (mixed-integer linear programming) or SMT-based techniques for global robustness analysis [Katz et al., 2017; Chen et al., 2021] are still too complex for DNNs in practical systems, even in offline computation. Various approaches were proposed to tackle the complexity challenge, but they are either still computationally expensive, e.g., with region-based robustness analyses [Gopinath et al., 2018; Mangal et al., 2019], or lack the deterministic guarantees, e.g., with sampling-based techniques [Ruan et al., 2019; Bastani et al., 2016; Mangal et al., 2019].

∗This is an extended abstract of a paper that won the Best Paper Award at Design, Automation and Test in Europe Conference (DATE 2022).

In this work, we propose an efficient certification approach to over-approximate the global robustness. Our approach introduces a novel network encoding structure, namely interleaving twin-network encoding, to compare two copies of the neural network side-by-side under different inputs, with extra interleaving dependencies added between them to improve efficiency. Our approach also includes over-approximation techniques based on network decomposition and LP (linear programming) relaxation, to further reduce the computation complexity. To the best of our knowledge, our approach is the first global robustness over-approximation method that certifies the robustness among the entire input domain with sound and deterministic guarantee. Experiments show that our approach is much more efficient and scalable than the exact global robustness methods such as Reluplex [Katz et al., 2017], with tight over-approximation. A case study of closeloop control system safety verification with perception DNN component further demonstrates the potential of our approach in practical systems.

2 Global Robustness Certification

2.1 ProblemFormulation

An n-layer neural network F : Rm0 → Rmn maps input x(0) ∈ Rm0 into output x(n) ∈ Rmn . The output of layer i is denoted as x(i) ∈ Rmi . The mapping between two consecutive layers x(i-1) and xi is composed with a linear transformation y(i) = W (i)x(i-1) + b(i) and (optionally) a ReLU

activation function, where the linear transformation result is denoted as variable y(i) ∈ Rmi . An illustrating example of a 2-layer neural network is shown in Fig. 1. For simplicity, all bias terms b(i) are 0.

As defined in [Katz et al., 2017; Wang et al., 2021d], the neural network global robustness measures the worst-case output variation when there is a small input perturbation for any possible input sample in the entire input domain X.

Definition 1 (Global Robustness). The j-th output of a neural network F is (δ, ε)-globally robust in the input domain X iff

In this work, we tackle the problem of measuring how robust a neural network is, as formally defined in Problem 1:

Problem 1. For a neural network F , given an input perturbation bound δ, determine the minimal output variation bound ε such that F is guaranteed to be (δ, ε)-globally robust.

[Katz et al., 2017] proposes to solve this problem by encoding two copies of the neural network side by side, as illustrated in the left part of Fig. 2. ˆx(0) represents a perturbed input of x(0) , by the bounded perturbation ∆x(0) . And ε will be the bound of output distance ∆x(n) . Under this encoding, Problem 1 can be formulated as an optimization problem:

Note that Eq. (1) can be solved with MILP by introducing a binary variable for each ReLU activation [Cheng et al., 2017], but the complexity is too high to be scalable. To overcome this, we present a new interleaving twin-network encoding (ITNE) scheme with two approximation techniques to efficiently find an over-approximated solution ¯ ε ≥ ε.

2.2 Interleaving Twin-Network Encoding

In this work, we design the interleaving twin-network encoding (ITNE) as shown in the right side of Fig. 2. Compared with the basic twin-network encoding (BTNE) [Katz et al., 2017] (the left side of Fig. 2), besides the connections between the input and output layers, interleaving connections are added for all hidden neurons between the two network copies. Specifically, for each neuron x = relu(y), two variables, ∆y = ˆ y - y and ∆x = ˆx - x, are added to encode the distance of y and x between the two copies. These distance variables reflect the hidden neuron variation caused by the perturbation. These changes enable the usage of the overapproximation techniques introduced below.

2.3 Over-Approximation Techniques

Leveraging ITNE, we design two over-approximation techniques, network decomposition (ND) and LP relaxation (LPR), to improve the global robustness certification efficiency. Inspired by the local robustness certification work in [Huang et al., 2020b], our ND and LPR techniques are specifically designed for global robustness.

ITNE-Based Network Decomposition (ND)

The main idea of ND is to divide a neural network into sub-networks and decompose the entire optimization problem into smaller problems to significantly reduce the optimization complexity. In the ITNE schema, instead of finding the output range of two copies of each sub-network, we look for the range of the original sub-network and the range of the output distance. For a decomposed network Fw(x(i) j ) with input x(i-w) and output x(i) j , given the input bounds x(i-w) and ∆x(i-w)1 , optimization problem in Eq. (1) is formulated on Fw(x(i) j ) to derive output ranges x(i) j and ∆x(i) j .

ITNE-Based LP Relaxation (LPR)

The idea of LPR is to relax the ReLU relation x = max(0, y), y ∈ [y, y] into linear constraints. When y ≤ 0 ≤ y, ReLU relation can be relaxed by three linear inequations:

In this work, we relax ReLUs in the original network x(n) = F(x(0) ) by Eq. (2), and relax the ReLU distance ∆x = relu(y + ∆y) - relu(y), as shown in Fig. 3. For ∀y ∈ R, the (∆x,∆y) mapping always falls in the shadowed area. Given ∆y ∈ [∆y,∆y], the relation between ∆x and ∆y can be bounded by a linear lower and upper bound:

1 We denote v = [v, v] as the range of variable v.

2.4 Illustrating Example

We consider the example neural network in Fig. 1, and set the input perturbation bound as δ = 0.1 and the input domain as x(0) ∈ [-1, 1]2 . The example neural network can be decomposed into three sub-networks:

In Fig. 4, we demonstrate the global robustness certification processes for different techniques. The exact MILP derives the exact output variation range [-0.2, 0.2]. When applying ND or LPR under BTNE, they are applied to each individual network copy. After ND, The distance information between x(1) and ˆx(1) is not encoded and is lost, resulting in a 7.5x over-approximation of the range of ∆x(2) . The LPR is based on the bounds y(1) , ˆ y(1) ∈ [-1.5, 1.5]2 , and y(2) , ˆ y(2) ∈ [-1.5, 1.5], resulting in a 10.9x overapproximation. On the other hand, under ITNE, the ITNEbased ND derives the range of ∆x(2) based on the range of x(1) and ∆x(1) , which is only 1.5x of the exact one. Given ∆y(1) ∈ [-0.15, 0.15]2 and ∆y(2) ∈ [-0.3, 0.3], the ITNEbased LPR derives a tight 1.38x over-approximation, significantly improving over BTNE.

2.5 Efficient Over-Approximation Algorithm

Finally, our global robustness certification algorithm is designed by combining the ITNE-based ND and LPR techniques with Selective Refinement (SR) 2 .

For layer i, ND constructs sub-networks Fw(x(i) j ), ∀j. MILP problems are built by LPR and SR to get the output variation bounds of layer i. The over-approximated output variation bound ε is derived by iteratively evaluating the output bounds (both the ∆yi and ∆xi ) of each hidden layer.

3 Evaluation and Applications

We first evaluate our algorithm on various DNNs and compare its results with exact global robustness (when available) and an under-approximated global robustness. Then, we demonstrate the application of our approach in a case study of safety verification for a vision-based robotic control system, and show the importance of efficient global robustness certification for safety-critical systems that involve neural nets. Finally, we discuss its comparison with adversarial training.

3.1 Performance Evaluation

We compare our approach with other methods on a set of DNNs, as shown in Table 1. DNNs 1 to 5 are 3-layer fully-connected (FC) networks trained on the Auto MPG dataset [Quinlan, 1993]. DNNs 6 to 8 are convolutional networks trained on the MNIST dataset [Lecun et al., 1998] 3 . The input perturbation bound δ = 0.001 for DNNs 1 to 5 and δ = 2/255 for DNNs 6 to 8. 4

We compare our over-approximated output variation bound εour with the exact bound ε solved by Reluplex [Katz et al., 2017; Katz et al., 2019] and the MILP encoding in Eq. (1).

2 While LPR can remove all integer variables in the MILP formulation to reduce the complexity, such extreme over-approximation may be too inaccurate. Thus, we try to selectively refine a limited number of neurons, by not relaxing their ReLU relations. This is similar to the layer-level refinement idea in [Huang et al., 2020b], but with a focus on global robustness.

3 Due to limited space, we only present 2 outputs of MNIST (out of 10) in Table 1. The rest show similar trends.

4 More detailed experiment settings can be found in the full paper [Wang et al., 2022b].

The runtime of Reluplex tR and MILP tM quickly increases with respect to neural network size. None of them can address 64-neuron DNN-5 within 24 hours. From DNNs 1 to 4, whose exact bounds ε are available, our algorithm can finish in seconds with only about 13% to 40% over-approximation. Starting from DNN 5, there is no other work in the literature that can derive a sound and deterministic global robustness in a reasonable time. To assess our over-approximated results for larger networks, we leverage adversarial examples from the Projected Gradient Descent (PGD) [Madry et al., 2018] among the entire dataset to derive an under-approximated output variation bound ε, inspired by [Ruan et al., 2019]. The experiments of DNNs 6 to 8 demonstrate that our method can provide meaningful over-approximation (less than 3x of the under-approximation) for DNNs with more than 5000 hidden neurons within 5 hours.

In our recent work [Wang et al., 2022c], we further improved the efficiency and tightness of our approach, where we leverage novel symbolic propagation technique inspired by βCROWN [Wang et al., 2021a] to replace the MILP solver in this work. The symbolic propagation technique takes advantage of GPU acceleration and can certify DNNs 6 to 8 within 3 hours and reduce the (εour - ε) gap by 9% - 60%.

3.2 Case Study on Control Safety Verification

For control systems that use neural networks for perception, a critical and yet challenging question is whether the system can remain safe under perturbation of network inputs. In [Wang et al., 2021d], we formulate this as a design-time safety assurance problem based on global robustness. Here, leveraging our global robustness certification technique, we demonstrate a solution for this safety assurance problem.

In particular, we consider an advanced cruise control (ACC) case study, where an ego vehicle, equipped with a camera, is following a reference vehicle. The captured images may be slightly perturbed. The distance from the reference vehicle is inferred from the images by a DNN. A feedback controller controls the ego vehicle based on the estimated distance. We model this example in the tool Webots [Michel, 2004] (Fig. 5). The ego vehicle is safe if distance d ∈ [0.5, 1.9] and speed ve ∈ [0.1, 0.7]. The reference vehicle speed vr is randomly adjusted within [0.2, 0.6]. The camera takes RGB images with resolution 24 × 48. A 5-layer convolutional network is trained with 100k precaptured images. We model the entire dynamic system as an LTI system with external disturbance terms 5 [Wang et al., 2022b], where the system states include distance and vehicle speed. The control input follows the feedback control law u = Kˆx, where ˆx is the estimated system state. According to the invariant set based verification [Huang et al., 2020a; Wang et al., 2020; Wang et al., 2021c], the vehicle control safety can be verified if the distance estimation error ∆d is within [-0.14, 0.14].

The distance estimation error ∆d = ∆d1 + ∆d2 contains the DNN model inaccuracy ∆d1 and the output variation ∆d2 caused by input perturbation. While |∆d1| ≤ 0.0730 is the worst-case model inaccuracy among the dataset, ∆d2 is the focus of this study and can be bounded by our global robustness certification algorithm. Assuming the input perturbation is bounded by δ = 2/255, the certified output variation bound becomes |∆d2| ≤ ϵ = 0.0568. Combined with ∆d1, we have |∆d| ≤ 0.1298. Therefore, under the assumed perturbation bound, we can assert that the DNN in this ACC system is safe.

5 External disturbances are caused by the randomness of reference vehicle speed and the inaccuracy of the linear model.

This is validated in Webots simulations, where adversarial perturbations are added by the Fast Gradient Sign Method (FGSM) [Goodfellow et al., 2015]. During simulations, when the perturbation bound δ = 2/255, we always have |∆d| ≤ 0.14 and a safe system. If we further increase input perturbation, |∆d| > 0.14 is observed when δ = 5/255 and unsafe states are observed when δ = 10/255. This shows the impact of input perturbation on system safety and the importance of our global robustness analysis.

3.3 Comparison with Adversarial Training

Neural network adversarial attack techniques and adversarial training algorithms are often jointly developed. Adversarial training performance is usually measured under the existing attack techniques, which may be less effective for more advanced attacks in the future. Instead, network robustness is a metric independent of attack techniques and can provide a deterministic guarantee. Compare to local robustness, where the guarantee is only on a finite set of data, global robustness can provide a universal guarantee for all possible inputs. Besides being a reliable metric, global robustness can also provide guidance to improve network robustness [Wang et al., 2022c; Fu et al., 2022] under arbitrary adversarial attacks.

4 Conclusion and FutureWork

We present an efficient certification algorithm to provide sound and deterministic global robustness analysis for ReLU neural networks. Experiments demonstrate that our approach is much more efficient and scalable than the exact certification approaches while providing tight over-approximation, and a case study further demonstrates its potential for practical systems. We believe that the approach has the potential to be applied in a variety of domains such as autonomous driving [Jiao et al., 2021; Zhu et al., 2021; Wang et al., 2021e] and smart building control [Xu et al., 2021], where disturbances and noises to sensor inputs are common. We will explore these applications in future work. We also plan to develop methods that can improve the global robustness of neural networks during their design and training, and investigate methods for joint design and verification, inspired by our recent works in this area [Wang et al., 2021b; Wang et al., 2022a; Wang et al., 2023a; Wang et al., 2023b].

Ethical Statement

There are no ethical issues with the proposed technique.

Acknowledgments

We gratefully acknowledge funding support by National Science Foundation (NSF) grants 1834701, 1724341, 2038853, Department of Energy (DOE) award DE-EE0009150, and Office of Naval Research grant N00014-19-1-2496.