Maximum Resilience of Artificial Neural Networks

Abstract

The deployment of Artificial Neural Networks (ANNs) in safety-critical applications poses a number of new verification and certification challenges. In particular, for ANN-enabled self-driving vehicles it is important to establish properties about the resilience of ANNs to noisy or even maliciously manipulated sensory input. We are addressing these challenges by defining resilience properties of ANN-based classifiers as the maximum amount of input or sensor perturbation which is still tolerated. This problem of computing maximum perturbation bounds for ANNs is then reduced to solving mixed integer optimization problems (MIP). A number of MIP encoding heuristics are developed for drastically reducing MIP-solver runtimes, and using parallelization of MIP-solvers results in an almost linear speed-up in the number (up to a certain limit) of computing cores in our experiments. We demonstrate the effectiveness and scalability of our approach by means of computing maximum resilience bounds for a number of ANN benchmark sets ranging from typical image recognition scenarios to the autonomous maneuvering of robots.

Appendix

Proposition 1

iff constraints (2a) to (4b) hold.

First we establish a lemma to assist the proof.

Lemma 1

.

Proof

($\Rightarrow$) Assume $b^{(l)}_i=1$, then (3a) holds trivially and (3b) implies $\textsf {im}^{(l)}_i\ge 0$.

($\Leftarrow$) Assume $\textsf {im}^{(l)}_i \ge 0$, then (3b) holds trivially and (3a) only holds if $b^{(l)}_i=1$.

Proof

(Proposition 1).

First we rewrite the condition $x^{(l)}_i = \textsf {max} (0, \textsf {im}^{(l)}_i)$ to allow further processing.

($\Rightarrow$) If $(b^{(l)}_i = 1 \Rightarrow x^{(l)}_i = \textsf {im}^{(l)}_i) \wedge (b^{(l)}_i = 0 \Rightarrow x^{(l)}_i = 0 )$ holds, as $b^{(l)}_i$ is a $0-1$ integer variable, we consider both cases:

• (case $b^{(l)}_i = 1$ ) From the left clause we derive $x^{(l)}_i = \textsf {im}^{(l)}_i$. From Lemma 1 we have $\textsf {im}^{(l)}_i\ge 0$. By injecting $b^{(l)}_i = 1$, $x^{(l)}_i = \textsf {im}^{(l)}_i$, and $\textsf {im}^{(l)}_i\ge 0$ to constraints (2a) to (4b), all constraints hold due to very large $M^{(l)}_i$.

• (case $b^{(l)}_i = 0$ ) From the right clause we derive $x^{(l)}_i = 0$. From Lemma 1 we have $\textsf {im}^{(l)}_i < 0$. By injecting $b^{(l)}_i = 0$, $x^{(l)}_i = 0$, and $\textsf {im}^{(l)}_i < 0$ to constraints (2a) to (4b), all constraints hold due to very large $M^{(l)}_i$.

($\Leftarrow$) If all constraints in (2a) to (4b) hold, we do case split to consider cases $b^{(l)}_i = 0$ and $b^{(l)}_i = 1$, and how they make $(b^{(l)}_i = 1 \Rightarrow x^{(l)}_i = \textsf {im}^{(l)}_i) \wedge (b^{(l)}_i = 0 \Rightarrow x^{(l)}_i = 0 )$ hold.

• (case $b^{(l)}_i = 1$ ) From (2b) and (4a) we know that $x^{(l)}_i =\textsf {im}^{(l)}_i$.

• (case $b^{(l)}_i = 0$ ) From (2a) and (4b) we know that $x^{(l)}_i = 0$.

In both cases, $(b^{(l)}_i = 1 \Rightarrow x^{(l)}_i = \textsf {im}^{(l)}_i) \wedge (b^{(l)}_i = 0 \Rightarrow x^{(l)}_i = 0 )$ holds.

Proposition 2

Given a feed-forward ANN with softmax output layer and a constant $\alpha > 0$, then for all $i, j\in \{1, \ldots , d^{(L)}\}$:

$$ x^{(L)}_{i_1} \ge \alpha \, x^{(L)}_{i_2} \Leftrightarrow x^{(L-1)}_{i_1} \ge \ln (\alpha ) + x^{(L-1)}_{i_2}.$$

Proof