Towards neural routing with verified bounds on performance

I. P. Buzhinsky ; A. A. Shalyto

Modelirovanie i analiz informacionnyh sistem, Tome 29 (2022) no. 3, pp. 228-245.

Résumé

When data-driven algorithms, especially the ones based on deep neural networks (DNNs), replace classical ones, their superior performance often comes with difficulty in their analysis. On the way to compensate for this drawback, formal verification techniques, which can provide reliable guarantees on program behavior, were developed for DNNs. These techniques, however, usually consider DNNs alone, excluding real-world environments in which they operate, and the applicability of techniques that do account for such environments is often limited. In this work, we consider the problem of formally verifying a neural controller for the routing problem in a conveyor network. Unlike in known problem statements, our DNNs are executed in a distributed context, and the performance of the routing algorithm, which we measure as the mean delivery time, depends on multiple executions of these DNNs. Under several assumptions, we reduce the problem to a number of DNN output reachability problems, which can be solved with existing tools. Our experiments indicate that sound-and-complete formal verification in such cases is feasible, although it is notably slower than the gradient-based search of adversarial examples. The paper is structured as follows. Section 1 introduces basic concepts. Then, Section 2 introduces the routing problem and DQN-Routing, the DNN-based algorithm that solves it. Section 3 proposes the contribution of this paper: a novel sound and complete approach to formally check an upper bound on the mean delivery time of DNN-based routing. This approach is experimentally evaluated in Section 4. The paper is concluded with some discussion of the results and outline of possible future work.

Détail

Keywords: formal verification, trustworthy AI, deep neural networks, routing problem.

Bibliographie

[1] D. Mukhutdinov, A. Filchenkov, A. Shalyto, and V. Vyatkin, “Multi-agent deep learning for simultaneous optimization for time and energy in distributed routing system”, Future Generation Computer Systems, 94 (2019), 587–600 | DOI

[2] J. A. Boyan and M. L. Littman, “Packet routing in dynamically changing networks: A reinforcement learning approach”, Proceedings of the 6th International Conference on Neural Information Processing Systems, 1993, 671–678

[3] G. Black and V. Vyatkin, “Intelligent component-based automation of baggage handling systems with IEC 61499”, IEEE Transactions on Automation Science and Engineering, 7:2 (2009), 337–351 | DOI

[4] A. Athalye, L. Engstrom, A. Ilyas, and K. Kwok, “Synthesizing robust adversarial examples”, Proceedings of the 35th International Conference on Machine Learning, 2018, 284–293

[5] K. Eykholt, I. Evtimov, E. Fernandes, B. Li, A. Rahmati, C. Xiao, A. Prakash, T. Kohno, and D. Song, “Robust physical-world attacks on deep learning visual classification”, IEEE/CVF Conference on Computer Vision and Pattern Recognition, 2018, 1625–1634

[6] C. Szegedy, W. Zaremba, I. Sutskever, J. B. Estrach, D. Erhan, I. Goodfellow, and R. Fergus, “Intriguing properties of neural networks”, International Conference on Learning Representations, 2014

[7] R. Drechsler (ed.), Advanced formal verification, 2004 | MR | Zbl

[8] G. Anderson, S. Pailoor, I. Dillig, and S. Chaudhuri, “Optimization and abstraction: A synergistic approach for analyzing neural network robustness”, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019, 731–744 | DOI

[9] S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari, “Output Range Analysis for Deep Feedforward Neural Networks”, NASA Formal Methods, eds. A. Dutle, C. Muñoz, and A. Narkawicz, Springer International Publishing, Cham, 2018, 121–138 | DOI

[10] Y. Y. Elboher, J. Gottschlich, and G. Katz, “An abstraction-based framework for neural network verification”, Computer Aided Verification, 2020, 43–65 | MR | Zbl

[11] X. Huang, M. Kwiatkowska, S. Wang, and M. Wu, “Safety verification of deep neural networks”, Computer Aided Verification, 2017, 3–29 | MR

[12] G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient SMT solver for verifying deep neural networks”, Computer Aided Verification, 2017, 97–117 | MR | Zbl

[13] G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljić, et al., “The Marabou framework for verification and analysis of deep neural networks”, Computer Aided Verification, 2019, 443–452 | MR

[14] M. Johnstone, D. Creighton, and S. Nahavandi, “Status-based routing in baggage handling systems: Searching verses learning”, IEEE Transactions on Systems, Man, and Cybernetics, Part C, 40:2 (2009), 189–200 | DOI

[15] A. N. Tarau, B. De Schutter, and H. Hellendoorn, “Model-based control for route choice in automated baggage handling systems”, IEEE Transactions on Systems, Man, and Cybernetics, Part C (Applications and Reviews), 40:3 (2010), 341–351 | DOI | MR

[16] O. Bastani, Y. Ioannou, L. Lampropoulos, D. Vytiniotis, A. Nori, and A. Criminisi, “Measuring neural net robustness with constraints”, Proceedings of the 30th International Conference on Neural Information Processing Systems, 2016, 2613–2621

[17] A. Fawzi, H. Fawzi, and O. Fawzi, “Adversarial vulnerability for any classifier”, Proceedings of the 32nd International Conference on Neural Information Processing Systems, 2018, 1178–1187

[18] A. Fawzi, O. Fawzi, and P. Frossard, “Analysis of classifiers' robustness to adversarial perturbations”, Machner Learning, 107:3 (2018), 481–508 | DOI | MR | Zbl

[19] S.-M. Moosavi-Dezfooli, A. Fawzi, and P. Frossard, “DeepFool: a simple and accurate method to fool deep neural networks”, IEEE Conference on Computer Vision and Pattern Recognition, 2016, 2574–2582

[20] A. Madry, A. Makelov, L. Schmidt, D. Tsipras, and A. Vladu, “Towards deep learning models resistant to adversarial attacks”, International Conference on Learning Representations, 2017 | MR

[21] A. Boopathy, T.-W. Weng, P.-Y. Chen, S. Liu, and L. Daniel, “CNN-Cert: An efficient framework for certifying robustness of convolutional neural networks”, Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, 2019, 3240–3247 | DOI

[22] P.-y. Chiang, R. Ni, A. Abdelkader, C. Zhu, C. Studor, and T. Goldstein, “Certified defenses for adversarial patches”, International Conference on Learning Representations, 2020

[23] M. Lecuyer, V. Atlidakis, R. Geambasu, D. Hsu, and S. Jana, “Certified robustness to adversarial examples with differential privacy”, IEEE S P, 2019, 656–672

[24] A. Raghunathan, J. Steinhardt, and P. Liang, “Certified Defenses against Adversarial Examples”, International Conference on Learning Representations, 2018

[25] V. Mnih, K. Kavukcuoglu, D. Silver, A. Graves, I. Antonoglou, D. Wierstra, and M. Riedmiller, “Playing Atari with deep reinforcement learning”, NIPS Deep Learning Workshop, 2013

[26] R. S. Sutton, A. G. Barto, et al., Introduction to reinforcement learning, Adaptive Computation and Machine Learning series, 135, MIT press, 1998 | MR

[27] E. Bacci and D. Parker, “Probabilistic Guarantees for Safe Deep Reinforcement Learning”, Formal Modeling and Analysis of Timed Systems, eds. N. Bertrand and N. Jansen, Springer International Publishing, Cham, 2020, 231–248 | DOI | MR

[28] O. Bastani, Y. Pu, and A. Solar-Lezama, “Verifiable reinforcement learning via policy extraction”, Proceedings of the 32nd International Conference on Neural Information Processing Systems, 2018, 2494–2504

[29] R. Ivanov, T. J. Carpenter, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Case study: verifying the safety of an autonomous racing car with a neural network controller”, Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, 2020, 1–7 | MR

[30] R. Ivanov, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Verisig: verifying safety properties of hybrid systems with neural network controllers”, Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, 2019, 169–178 | MR

[31] Y. Kazak, C. Barrett, G. Katz, and M. Schapira, “Verifying deep-RL-driven systems”, Proceedings of the 2019 Workshop on Network Meets AI ML, 2019, 83–89 | DOI

[32] L. Oakley, A. Oprea, and S. Tripakis, “Adversarial Robustness of AI Agents Acting in Probabilistic Environments”, Workshop on Foundations of Computer Security, 2020

[33] H.-D. Tran, F. Cai, M. L. Diego, P. Musau, T. T. Johnson, and X. Koutsoukos, “Safety verification of cyber-physical systems with reinforcement learning control”, ACM Transactions on Embedded Computer Systems, 18:5s (2019), 1–22 | DOI | MR

[34] A. Bianco and L. De Alfaro, “Model checking of probabilistic and nondeterministic systems”, Foundations of Software Technology and Theoretical Computer Science, 1995, 499–513 | DOI | MR | Zbl

[35] M. Belkin and P. Niyogi, “Laplacian eigenmaps and spectral techniques for embedding and clustering”, Proceedings of the 14th International Conference on Neural Information Processing Systems: Natural and Synthetic, 2002, 585–591

[36] V. Mnih, K. Kavukcuoglu, D. Silver, A. A.Rusu, J. Veness, M. G. Bellemare, A. Graves, M. Riedmiller, A. K. Fidjeland, G. Ostrovski, et al., “Human-level control through deep reinforcement learning”, Nature, 518:7540 (2015), 529–533 | DOI

[37] J. R. Norris, Markov chains, Cambridge University Press, 1998 | MR | Zbl

[38] C. Szegedy, V. Vanhoucke, S. Ioffe, J. Shlens, and Z. Wojna, “Rethinking the Inception architecture for computer vision”, IEEE Conference on Computer Vision and Pattern Recognition, 2016, 2818–2826

[39] C. Barrett and C. Tinelli, “Satisfiability Modulo Theories”, Handbook of Model Checking, eds. E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Springer International Publishing, Cham, 2018, 305–343 | DOI | MR | Zbl

[40] L. De Moura and N. Bjørner, “Z3: An efficient SMT solver”, Tools and Algorithms for the Construction and Analysis of Systems, 2008, 337–340

[41] A. Meurer, C. P. Smith, M. Paprocki, O. Čert{\i}k, S. B. Kirpichev, M. Rocklin, A. Kumar, S. Ivanov, J. K. Moore, S. Singh, et al., “SymPy: symbolic computing in Python”, PeerJ Computer Science, 3 (2017), e103 | DOI