Week #1: A first look into neural network verification

Summary of contributions

• LazySets#2177

• LazySets#2179

Introduction

In this notebook I will be presenting one of the objectives of my Julia Summer of Contributions project, the verification of Neural Networks, the algorithm that I will be focusing on and the tools that I will use along this project. The main focus of this projects are Zonotopes.

Zonotopes are set representations that have been applied in a range of scientific domains, most notably:

• Deep Neural Network(DNN) verification [1, 2].

• Reachability analysis for linear and nonlinear ordinary differential equations (ODEs), both continuous or hybrid (that is, continuous ODEs with jumps between discrete transitions). To cite a few applications:

  • Safety assessment in autonomous driving [3].

  • Power systems stability [4].

  • Set-based analysis in nonlinear biological models [5, 6].

• Robust model-predictive control [7, 8, 9].

Verification of Neural Networks

Mathematically, the robustness verification of a DNN can be stated as follows. Given a DNN $f(x)$, input set $B$ and an output set $S$, the verification problem seeks to answer whether the proposition

is true or false [10, 11]. The following picture illustrates this problem (taken from the ERAN library).

In general, robustness verification of DNNs guarantees that the outputs of the DNN are compliant with some predefined set of “safe” states, subject to perturbations in the inputs of the network. Such guarantees are becoming particularly important for DNNs applied to safety-critical systems, i.e. cases where incorrect outputs can lead to costly consequences.

$Ai^2$

$Ai^2$ is a verification algorithm for neural networks, first proposed in [1], it handles common network layer types, including fully connected and convolutional layers with rectified linear unit activations (ReLU) and max pooling layers.

First look into $Ai^2$ using Zonotopes

One of the objectives of this project is implementing the $Ai^2$ algorithm using the paper's [1] implementation using Zonotopes, in NeuralVerification.jl the implementation of $Ai^2$ uses Polytopes.

Zonotopes can be described as the image of a unit infinity-norm ball in $\mathbb{R}^n$ by an affine transformation, this is why zonotopes are widely used in Affine arithmetic. The order of a zonotope is defined as the quotient of its number of generators and its dimension, you can reduce the order of a given zonotope by subtracting generators.

Mathematically, it is equivalent to define a zonotope as the set Z

$$ where $c \in \mathbb{R}^n$ is its center and $\{g_i\}_{i=1}^p$, $g_i \in \mathbb{R}^n$, is the set of generators. This characterization defines a zonotope as the finite Minkowski sum of line segments.

Zonotopes are not a closed set under intersections, thus we use an overapproximation of the intersection in our algorithm

The library LazySets.jl will be used to handle the Zonotope operations

using LazySets

Z0 is copied from [1]

Z0 = Zonotope([1., 2], [[.5, .5], [0, .5], [.5, 0]])

using Plots

plot(Z0, ratio=1)

To apply the weights and biases of the neural network's layer we use an affine map, in the example, the layer has no biases, so a simpler linear map can be used

Z1 = linear_map([2. -1; 0 1], Z0)

plot(Z1)

Now we have to apply the ReLU transformation, later this will be done using Zonotopes, but for now, the zonotope will be transformed to a Polytope and done by hand

P = convert(HPolytope, Z1)

A2 = intersection(P, HalfSpace([-1., 0], 0.))

plot(A2)

After the intersection, the resulting polytope can be overapproximated with a Zonotope

Z2 = overapproximate(A2, Zonotope, CustomDirections([[1., 0], [1, 1], [1, -1]]))

plot(Z2)

Z4 = linear_map([1. 0; 0 1], Z2)

plot(Z4)

A3 = intersection(P, HalfSpace([1., 0], 0.))

plot(A3)

Z3 = overapproximate(A3, Zonotope, CustomDirections([[-1., 0], [-1, 1], [-1, -1]]))

plot(Z3)

Z5 = linear_map([0. 0; 0 1], Z3)

plot(Z5)

To make the union of the resulting Zonotopes, we make a Convex Hull and then it is overapproximated with a Zonotope

CH6 = convex_hull(Z4, Z5)

plot(CH6)

overapproximate(CH6, Zonotope, CustomDirections([[-1., 0], [-1, 1], [-1, -1]]))

Summary of the code

Z0 = Zonotope([1., 2], [[.5, .5], [0, .5], [.5, 0]]) # Initial Zonotope

Z1 =linear_map([2. -1; 0 1], Z0) # application of weights

P = convert(HPolytope, Z1) # convertion to polytope for intersections

# ReLU

A2 = intersection(P, HalfSpace([-1., 0], 0.)) # x1 >= 0

A3 = intersection(P, HalfSpace([1., 0], 0.)) # x1 < 0

cd = CustomDirections([[-1., 0], [-1, 1], [1, 1]]) # directions of the generators

Z2 = overapproximate(A2, Zonotope, cd) # overapproximate intersection with zonotope

Z3 = overapproximate(A3, Zonotope, cd)

Z4 = linear_map([1. 0; 0 1], Z2) # Z2 * (1 0; 0 1)

Z5 = linear_map([0. 0; 0 1], Z3) # Z3 * (0 0; 0 1)

CH6 = convex_hull(Z4, Z5) # union of Z4 and Z5

Z6 = overapproximate(CH6, Zonotope, cd) # overapproximate the union with a zonotope

l = @layout [a{0.3w} grid(2,2) b{0.3w}]

plot([Z1, Z2, Z4, Z3, Z5,CH6], layout = l, title=["Z1" "Z2" "Z4" "Z3" "Z5" "CH6"], ratio=1, size = (900, 256))

References

1. T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri and M. Vechev, "AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation," 2018 IEEE Symposium on Security and Privacy (SP), San Francisco, CA, 2018, pp. 3-18, doi: 10.1109/SP.2018.00058.

2. Liu, C., Arnon, T., Lazarus, C., Barrett, C., & Kochenderfer, M. J. (2019). Algorithms for verifying deep neural networks. arXiv preprint arXiv:1903.06758.

3. Althoff, M. (2010). Reachability analysis and its application to the safety assessment of autonomous cars. Doctoral dissertation, Technische Universität München.

4. Zhang, Y., Li, Y., Tomsovic, K., Djouadi, S., & Yue, M. (2019). Review on Set-Theoretic Methods for Safety Verification and Control of Power System. arXiv preprint arXiv:2001.00080. Accepted by IET ENERGY SYSTEM INTEGRATION on February, 2020.

5. Dang, T., Le Guernic, C., & Maler, O. (2009, August). Computing reachable states for nonlinear biological models. In International Conference on Computational Methods in Systems Biology (pp. 126-141). Springer, Berlin, Heidelberg.

6. Dang, T. (2019, April). Reachability Analysis and Hybrid Systems Biology-In Memoriam Oded Maler. In International Workshop on Hybrid Systems Biology (pp. 16-29). Springer, Cham.

7. Bravo, J. M., Alamo, T., Limon, D., & Camacho, E. F. (2003, September). Robust MPC of constrained discrete-time nonlinear systems based on zonotopes. In 2003 European Control Conference (ECC) (pp. 2035-2040). IEEE.

8. Le, V. T. H. (2012). Robust predictive control by zonotopic set-membership estimation. Doctoral dissertation.

9. Le, V. T. H., Stoica, C., Dumur, D., Alamo, T., & Camacho, E. F. (2011, December). Robust tube-based constrained predictive control via zonotopic set-membership estimation. In 2011 50th IEEE Conference on Decision and Control and European Control Conference (pp. 4580-4585). IEEE.

10. Liu, C., Arnon, T., Lazarus, C., Barrett, C., & Kochenderfer, M. J. (2019). Algorithms for verifying deep neural networks. arXiv preprint arXiv:1903.06758.

11. Royo, V. R., Calandra, R., Stipanovic, D. M., & Tomlin, C. (2019). Fast neural network verification via shadow prices. arXiv preprint arXiv:1902.07247.

12. Singh, G., Gehr, T., Mirman, M., Püschel, M., & Vechev, M. (2018). Fast and effective robustness certification. In Advances in Neural Information Processing Systems (pp. 10802-10813).