Safe, Autonomous and Intelligent Vehicles pp 187-197 | Cite as

# Compositional Verification for Autonomous Systems with Deep Learning Components

## Abstract

As autonomy becomes prevalent in many applications, ranging from recommendation systems to fully autonomous vehicles, there is an increased need to provide safety guarantees for such systems. The problem is difficult, as these are large, complex systems which operate in uncertain environments, requiring data-driven machine-learning components. However, learning techniques such as Deep Neural Networks, widely used today, are inherently unpredictable and lack the theoretical foundations to provide strong assurance guarantees. We present a compositional approach for the scalable, formal verification of autonomous systems that contain Deep Neural Network components. The approach uses assume-guarantee reasoning whereby *contracts*, encoding the input–output behavior of individual components, allow the designer to model and incorporate the behavior of the learning-enabled components working side-by-side with the other components. We illustrate the approach on an example taken from the autonomous vehicles domain.

## References

- 1.S. Bak, S. Chaki, Verifying cyber-physical systems by combining software model checking with hybrid systems reachability, in
*2016 International Conference on Embedded Software, EMSOFT 2016*, Pittsburgh, Pennsylvania, USA, October 1–7, 2016 (2016), pp. 10:1–10:10Google Scholar - 2.S. Bogomolov, G. Frehse, M. Greitschus, R. Grosu, C.S. Pasareanu, A. Podelski, T. Strump, Assume-guarantee abstraction refinement meets hybrid systems, in
*Proceedings of Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014*, Haifa, Israel, November 18–20, 2014 (2014), pp. 116–131Google Scholar - 3.N. Carlini, D. Wagner, Towards evaluating the robustness of neural networks, in
*Proceedings of 38th IEEE Symposium on Security and Privacy*(2017)Google Scholar - 4.C. Chilton, B. Jonsson, M.Z. Kwiatkowska, An algebraic theory of interface automata. Theor. Comput. Sci.
**549**, 146–174 (2014)MathSciNetCrossRefGoogle Scholar - 5.C. Chilton, B. Jonsson, M.Z. Kwiatkowska, Compositional assume-guarantee reasoning for input/output component theories. Sci. Comput. Program.
**91**, 115–137 (2014)CrossRefGoogle Scholar - 6.T. Dreossi, A. Donzé, S.A. Seshia, Compositional falsification of cyber-physical systems with machine learning components, in
*Proceedings of NASA Formal Methods - 9th International Symposium, NFM 2017*, Moffett Field, CA, USA, May 16–18, 2017 (2017), pp. 357–372Google Scholar - 7.R. Feinman, R.R. Curtin, S. Shintre, A.B. Gardner, Detecting adversarial samples from artifacts. Technical Report (2017). http://arxiv.org/abs/1703.00410
- 8.I.J. Goodfellow, J. Shlens, C. Szegedy, Explaining and harnessing adversarial examples. Technical Report (2014). http://arxiv.org/abs/1412.6572
- 9.D. Gopinath, G. Katz, C.S. Pasareanu, C. Barrett, Deepsafe: a data-driven approach for checking adversarial robustness in neural networks, in
*Proc. ATVA’18*(2017). https://arxiv.org/abs/1710.00486 - 10.X. Huang, M. Kwiatkowska, S. Wang, M. Wu, Safety verification of deep neural networks, in
*Proceedings of 29th International Conference on Computer Aided Verification (CAV)*(2017), pp. 3–29Google Scholar - 11.K. Julian, J. Lopez, J. Brush, M. Owen, M. Kochenderfer, Policy compression for aircraft collision avoidance systems, in
*Digital Avionics Systems Conference (DASC)*(2016), pp. 1–10Google Scholar - 12.T. Kanungo, D.M. Mount, N.S. Netanyahu, C.D. Piatko, R. Silverman, A.Y. Wu, An efficient k-means clustering algorithm: analysis and implementation. IEEE Trans. Pattern Anal. Mach. Intell.
**24**(7), 881–892 (2002)CrossRefGoogle Scholar - 13.G. Katz, C. Barrett, D. Dill, K. Julian, M. Kochenderfer, Reluplex: an efficient SMT solver for verifying deep neural networks, in
*Proceedings of the 29th International Conference on Computer Aided Verification (CAV)*(2017), pp. 97–117Google Scholar - 14.A. Komuravelli, C.S. Pasareanu, E.M. Clarke, Assume-guarantee abstraction refinement for probabilistic systems, in
*Proceedings of Computer Aided Verification - 24th International Conference, CAV 2012*, Berkeley, CA, USA, July 7–13, 2012 (2012), pp. 310–326Google Scholar - 15.A. Kurakin, I. Goodfellow, S. Bengio, Adversarial examples in the physical world, 2016. Technical Report. http://arxiv.org/abs/1607.02533
- 16.Y. LeCun, C. Cortes, C.J.C. Burges, The MNIST database of handwritten digits. http://yann.lecun.com/exdb/mnist/
- 17.Y. Li, Y. Gal, Dropout inference in Bayesian neural networks with alpha-divergences, in
*International Conference on Machine Learning*(2017), pp. 2052–2061Google Scholar - 18.J. Li, P. Nuzzo, A.L. Sangiovanni-Vincentelli, Y. Xi, D. Li, Stochastic assume-guarantee contracts for cyber-physical system design under probabilistic requirements. CoRR (2017). http://arxiv.org/abs/1705.09316
- 19.C.S. Pasareanu, D. Giannakopoulou, M.G. Bobaru, J.M. Cobleigh, H. Barringer, Learning to divide and conquer: applying the l* algorithm to automate assume-guarantee reasoning. Formal Methods Syst. Des.
**32**(3), 175–205 (2008)CrossRefGoogle Scholar - 20.C. Szegedy, W. Zaremba, I. Sutskever, J. Bruna, D. Erhan, I. Goodfellow, R. Fergus, Intriguing properties of neural networks, 2013. Technical Report. http://arxiv.org/abs/1312.6199