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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
- 2.
For clarity, we usually omit the dependency of \(\varPhi _m\) from \(\alpha \).
- 3.
- 4.
- 5.
References
Abu-Mostafa, Y.S., Magdon-Ismail, M., Lin, H.-T.: Learning from Data, vol. 4. AMLBook, New York (2012)
Amodei, D., Olah, C., Steinhardt, J., Christiano, P., Schulman, J., Mané, D.: Concrete problems in Ai safety. arXiv preprint arXiv:1606.06565 (2016)
Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., Criminisi, A.: Measuring neural net robustness with constraints. CoRR, abs/1605.07262 (2016)
Bjørner, N., Phan, A.-D., Fleckenstein, L.: vZ-an optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_14
Bhattacharyya, S., Cofer, D., Musliner, D., Mueller, J., Engstrom, E.: Certification considerations for adaptive systems. In ICUAS, pp. 270–279. IEEE (2015)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, pp. 238–252. ACM (1977)
Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572 (2014)
Grossmann, I.E.: Review of nonlinear mixed-integer and disjunctive programming techniques. Optim. Eng. 3(3), 227–252 (2002)
Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. CoRR, abs/1610.06940 (2016)
Karpathy, A.: ConvNetJS: deep learning in your browser (2014). URL http://cs.stanford.edu/people/karpathy/convnetjs
Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. CoRR, abs/1702.01135 (2017)
Kurakin, A., Goodfellow, I., Bengio, S.: Adversarial examples in the physical world. arXiv preprint arXiv:1607.02533 (2016)
LeCun, Y., Cortes, C., Burges, C.J.: The MNIST database of handwritten digits (1998)
Mnih, V., Kavukcuoglu, K., Silver, D., Graves, A., Antonoglou, I., Wierstra, D., Riedmiller, M.: Playing atari with deep reinforcement learning. arXiv preprint arXiv:1312.5602 (2013)
Nguyen, A., Yosinski, J., Clune, J.: Deep neural networks are easily fooled: high confidence predictions for unrecognizable images. In CPVR, pp. 427–436 (2015)
Papernot, N., McDaniel, P., Goodfellow, I., Jha, S., Celik, Z.B., Swami, A.: Practical black-box attacks against deep learning systems using adversarial examples. arXiv preprint arXiv:1602.02697 (2016)
Papernot, N., McDaniel, P., Wu, X., Jha, S., Swami, A.: Distillation as a defense to adversarial perturbations against deep neural networks. In: Oakland, pp. 582–597. IEEE (2016)
Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 243–257. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_24
Pulina, L., Tacchella, A.: Challenging SMT solvers to verify neural networks. AI Commun. 25(2), 117–135 (2012)
Rajan, S., Wang, S., Inkol, R., Joyal, A.: Efficient approximations for the arctangent function. IEEE Signal Process. Mag. 23(3), 108–111 (2006)
Scheibler, K., Winterer, L., Wimmer, R., Becker, B.: Towards verification of artificial neural networks. In: MBMV, pp. 30–40 (2015)
Ukil, A., Shah, V.H., Deck, B.: Fast computation of arctangent functions for embedded applications: a comparative analysis. In ISIE, pp. 1206–1211. IEEE (2011)
Xu, Y., Ralphs, T.K., Ladányi, L., Saltzman, M.J.: Computational experience with a software framework for parallel integer programming. INFORMS J. Comput. 21(3), 383–397 (2009)
Author information
Authors and Affiliations
Corresponding authors
Editor information
Editors and Affiliations
Appendix
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)}\}\):
Proof
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Cheng, CH., Nührenberg, G., Ruess, H. (2017). Maximum Resilience of Artificial Neural Networks. In: D'Souza, D., Narayan Kumar, K. (eds) Automated Technology for Verification and Analysis. ATVA 2017. Lecture Notes in Computer Science(), vol 10482. Springer, Cham. https://doi.org/10.1007/978-3-319-68167-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-68167-2_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-68166-5
Online ISBN: 978-3-319-68167-2
eBook Packages: Computer ScienceComputer Science (R0)