maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2022-3-228-245mais-1714Research ArticleTheory of ComputingНа пути к нейросетевой маршрутизации с верифицированными границами эффективностиTowards Neural Routing with Verified Bounds on Performancehttps://orcid.org/0000-0003-3713-6051БужинскийИгорь ПетровичBuzhinskyIgor Petrovichigor.buzhinsky@gmail.comhttps://orcid.org/0000-0002-2723-2077ШалытоАнатолий АбрамовичShalytoAnatoly Abramovichanatoly.shalyto@gmail.comУниверситет АалтоРоссияAalto UniversityRussian FederationУниверситет ИТМОРоссияITMO UniversityRussian Federation202225092022293228245Copyright © Бужинский И.П., Шалыто А.А., 20222022Бужинский И.П., Шалыто А.А.Buzhinsky I.P., Shalyto A.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1714

Когда алгоритмы на основе данных, особенно основанные на глубоких нейронных сетях (ГНС), заменяют классические, их более высокая производительность часто сопряжена с трудностями при анализе. Чтобы компенсировать этот недостаток, для ГНС были разработаны методы формальной верификации, которые могут предоставить надежные гарантии поведения программы. Эти методы, однако, обычно рассматривают только саму ГНС, исключая среду, в которой она работает, и применимость методов, учитывающих такие среды, часто ограничена. В данной работе рассматривается задача формальной верификации нейросетевого контроллера для задачи маршрутизации в конвейерной сети. В отличие от известных постановок задачи, рассматриваемые ГНС выполняются в распределенной среде, и производительность алгоритма маршрутизации, которая измеряется как среднее время доставки, зависит от многократного выполнения этих ГНС. При некоторых предположениях, проблема верификации сводится к ряду проблем достижимости выходов ГНС, которые можно решить с помощью существующих программных средств. Эксперименты показывают, что в таких случаях возможна строгая и полная формальная верификация, хотя она заметно медленнее, чем градиентный поиск состязательных примеров.Статья построена следующим образом. Раздел 1 вводит основные понятия. Затем в Разделе 2 представлена проблема маршрутизации и алгоритм DQN-маршрутизации на основе ГНС, который ее решает. В Разделе 3 описывается вклад данной статьи: новый надежный и полный подход к формальной проверке верхней границы среднего времени доставки маршрутизации на основе ГНС. Этот подход экспериментально оценивается в Разделе 4. Статья завершается обсуждением результатов и описанием возможной будущей работы.

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.

формальная верификациянадежный ИИглубокие нейронные сетизадача маршрутизацииformal verificationtrustworthy AIdeep neural networksrouting problemReferencesD. 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, vol. 94, pp. 587-600, 2019.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, vol. 94, pp. 587-600, 2019.J. A. Boyan and M. L. Littman, “Packet routing in dynamically changing networks: A reinforcement learning approach”, in Proceedings of the 6th International Conference on Neural Information Processing Systems, 1993, pp. 671-678.J. A. Boyan and M. L. Littman, “Packet routing in dynamically changing networks: A reinforcement learning approach”, in Proceedings of the 6th International Conference on Neural Information Processing Systems, 1993, pp. 671-678.G. Black and V. Vyatkin, “Intelligent component-based automation of baggage handling systems with IEC 61499”, IEEE Transactions on Automation Science and Engineering, vol. 7, no. 2, pp. 337-351, 2009.G. Black and V. Vyatkin, “Intelligent component-based automation of baggage handling systems with IEC 61499”, IEEE Transactions on Automation Science and Engineering, vol. 7, no. 2, pp. 337-351, 2009.A. Athalye, L. Engstrom, A. Ilyas, and K. Kwok, “Synthesizing robust adversarial examples”, in Proceedings of the 35th International Conference on Machine Learning, 2018, pp. 284-293.A. Athalye, L. Engstrom, A. Ilyas, and K. Kwok, “Synthesizing robust adversarial examples”, in Proceedings of the 35th International Conference on Machine Learning, 2018, pp. 284-293.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”, in IEEE/CVF Conference on Computer Vision and Pattern Recognition, 2018, pp. 1625-1634.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”, in IEEE/CVF Conference on Computer Vision and Pattern Recognition, 2018, pp. 1625-1634.C. Szegedy, W. Zaremba, I. Sutskever, J. B. Estrach, D. Erhan, I. Goodfellow, and R. Fergus, “Intriguing properties of neural networks”, in International Conference on Learning Representations, 2014.C. Szegedy, W. Zaremba, I. Sutskever, J. B. Estrach, D. Erhan, I. Goodfellow, and R. Fergus, “Intriguing properties of neural networks”, in International Conference on Learning Representations, 2014.R. Drechsler, Ed., Advanced formal verification. 2004, vol. 122.R. Drechsler, Ed., Advanced formal verification. 2004, vol. 122.G. Anderson, S. Pailoor, I. Dillig, and S. Chaudhuri, “Optimization and abstraction: A synergistic approach for analyzing neural network robustness”, in Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019, pp. 731-744.G. Anderson, S. Pailoor, I. Dillig, and S. Chaudhuri, “Optimization and abstraction: A synergistic approach for analyzing neural network robustness”, in Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019, pp. 731-744.S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari, “Output Range Analysis for Deep Feedforward Neural Networks”, in NASA Formal Methods, A. Dutle, C. Mun˜ oz, and A. Narkawicz, Eds., Cham: Springer International Publishing, 2018, pp. 121-138.S. Dutta, S. Jha, S. Sankaranarayanan, and A. Tiwari, “Output Range Analysis for Deep Feedforward Neural Networks”, in NASA Formal Methods, A. Dutle, C. Mun˜ oz, and A. Narkawicz, Eds., Cham: Springer International Publishing, 2018, pp. 121-138.Y. Y. Elboher, J. Gottschlich, and G. Katz, “An abstraction-based framework for neural network verification”, in Computer Aided Verification, 2020, pp. 43-65.Y. Y. Elboher, J. Gottschlich, and G. Katz, “An abstraction-based framework for neural network verification”, in Computer Aided Verification, 2020, pp. 43-65.X. Huang, M. Kwiatkowska, S. Wang, and M. Wu, “Safety verification of deep neural networks”, in Computer Aided Verification, 2017, pp. 3-29.X. Huang, M. Kwiatkowska, S. Wang, and M. Wu, “Safety verification of deep neural networks”, in Computer Aided Verification, 2017, pp. 3-29.G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient SMT solver for verifying deep neural networks”, in Computer Aided Verification, 2017, pp. 97-117.G. Katz, C. Barrett, D. L. Dill, K. Julian, and M. J. Kochenderfer, “Reluplex: An efficient SMT solver for verifying deep neural networks”, in Computer Aided Verification, 2017, pp. 97-117.G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljic´, et al., “The Marabou framework for verification and analysis of deep neural networks”, in Computer Aided Verification, 2019, pp. 443-452.G. Katz, D. A. Huang, D. Ibeling, K. Julian, C. Lazarus, R. Lim, P. Shah, S. Thakoor, H. Wu, A. Zeljic´, et al., “The Marabou framework for verification and analysis of deep neural networks”, in Computer Aided Verification, 2019, pp. 443-452.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, vol. 40, no. 2, pp. 189-200, 2009.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, vol. 40, no. 2, pp. 189-200, 2009.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), vol. 40, no. 3, pp. 341-351, 2010.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), vol. 40, no. 3, pp. 341-351, 2010.O. Bastani, Y. Ioannou, L. Lampropoulos, D. Vytiniotis, A. Nori, and A. Criminisi, “Measuring neural net robustness with constraints”, in Proceedings of the 30th International Conference on Neural Information Processing Systems, 2016, pp. 2613-2621.O. Bastani, Y. Ioannou, L. Lampropoulos, D. Vytiniotis, A. Nori, and A. Criminisi, “Measuring neural net robustness with constraints”, in Proceedings of the 30th International Conference on Neural Information Processing Systems, 2016, pp. 2613-2621.A. Fawzi, H. Fawzi, and O. Fawzi, “Adversarial vulnerability for any classifier”, in Proceedings of the 32nd International Conference on Neural Information Processing Systems, 2018, pp. 1178-1187.A. Fawzi, H. Fawzi, and O. Fawzi, “Adversarial vulnerability for any classifier”, in Proceedings of the 32nd International Conference on Neural Information Processing Systems, 2018, pp. 1178-1187.A. Fawzi, O. Fawzi, and P. Frossard, “Analysis of classifiers’ robustness to adversarial perturbations”, Machner Learning, vol. 107, no. 3, pp. 481-508, 2018.A. Fawzi, O. Fawzi, and P. Frossard, “Analysis of classifiers’ robustness to adversarial perturbations”, Machner Learning, vol. 107, no. 3, pp. 481-508, 2018.S.-M. Moosavi-Dezfooli, A. Fawzi, and P. Frossard, “DeepFool: a simple and accurate method to fool deep neural networks”, in IEEE Conference on Computer Vision and Pattern Recognition, 2016, pp. 2574-2582.S.-M. Moosavi-Dezfooli, A. Fawzi, and P. Frossard, “DeepFool: a simple and accurate method to fool deep neural networks”, in IEEE Conference on Computer Vision and Pattern Recognition, 2016, pp. 2574-2582.A. Madry, A. Makelov, L. Schmidt, D. Tsipras, and A. Vladu, “Towards deep learning models resistant to adversarial attacks”, in International Conference on Learning Representations, 2017.A. Madry, A. Makelov, L. Schmidt, D. Tsipras, and A. Vladu, “Towards deep learning models resistant to adversarial attacks”, in International Conference on Learning Representations, 2017.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”, in Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, vol. 33, 2019, pp. 3240-3247.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”, in Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, vol. 33, 2019, pp. 3240-3247.P.-y. Chiang, R. Ni, A. Abdelkader, C. Zhu, C. Studor, and T. Goldstein, “Certified defenses for adversarial patches”, in International Conference on Learning Representations, 2020.P.-y. Chiang, R. Ni, A. Abdelkader, C. Zhu, C. Studor, and T. Goldstein, “Certified defenses for adversarial patches”, in International Conference on Learning Representations, 2020.M. Lecuyer, V. Atlidakis, R. Geambasu, D. Hsu, and S. Jana, “Certified robustness to adversarial examples with differential privacy”, in IEEE S & P, 2019, pp. 656-672.M. Lecuyer, V. Atlidakis, R. Geambasu, D. Hsu, and S. Jana, “Certified robustness to adversarial examples with differential privacy”, in IEEE S & P, 2019, pp. 656-672.A. Raghunathan, J. Steinhardt, and P. Liang, “Certified Defenses against Adversarial Examples”, in International Conference on Learning Representations, 2018.A. Raghunathan, J. Steinhardt, and P. Liang, “Certified Defenses against Adversarial Examples”, in International Conference on Learning Representations, 2018.V. Mnih, K. Kavukcuoglu, D. Silver, A. Graves, I. Antonoglou, D. Wierstra, and M. Riedmiller, “Playing Atari with deep reinforcement learning”, in NIPS Deep Learning Workshop, 2013.V. Mnih, K. Kavukcuoglu, D. Silver, A. Graves, I. Antonoglou, D. Wierstra, and M. Riedmiller, “Playing Atari with deep reinforcement learning”, in NIPS Deep Learning Workshop, 2013.R. S. Sutton, A. G. Barto, et al., Introduction to reinforcement learning. MIT press, 1998, vol. 135.R. S. Sutton, A. G. Barto, et al., Introduction to reinforcement learning. MIT press, 1998, vol. 135.E. Bacci and D. Parker, “Probabilistic Guarantees for Safe Deep Reinforcement Learning”, in Formal Modeling and Analysis of Timed Systems, N. Bertrand and N. Jansen, Eds., Cham: Springer International Publishing, 2020, pp. 231-248.E. Bacci and D. Parker, “Probabilistic Guarantees for Safe Deep Reinforcement Learning”, in Formal Modeling and Analysis of Timed Systems, N. Bertrand and N. Jansen, Eds., Cham: Springer International Publishing, 2020, pp. 231-248.O. Bastani, Y. Pu, and A. Solar-Lezama, “Verifiable reinforcement learning via policy extraction”, in Proceedings of the 32nd International Conference on Neural Information Processing Systems, 2018, pp. 2494-2504.O. Bastani, Y. Pu, and A. Solar-Lezama, “Verifiable reinforcement learning via policy extraction”, in Proceedings of the 32nd International Conference on Neural Information Processing Systems, 2018, pp. 2494-2504.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”, in Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, 2020, pp. 1-7.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”, in Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, 2020, pp. 1-7.R. Ivanov, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Verisig: verifying safety properties of hybrid systems with neural network controllers”, in Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, 2019, pp. 169-178.R. Ivanov, J. Weimer, R. Alur, G. J. Pappas, and I. Lee, “Verisig: verifying safety properties of hybrid systems with neural network controllers”, in Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, 2019, pp. 169-178.Y. Kazak, C. Barrett, G. Katz, and M. Schapira, “Verifying deep-RL-driven systems”, in Proceedings of the 2019 Workshop on Network Meets AI & ML, 2019, pp. 83-89.Y. Kazak, C. Barrett, G. Katz, and M. Schapira, “Verifying deep-RL-driven systems”, in Proceedings of the 2019 Workshop on Network Meets AI & ML, 2019, pp. 83-89.L. Oakley, A. Oprea, and S. Tripakis, “Adversarial Robustness of AI Agents Acting in Probabilistic Environments”, in Workshop on Foundations of Computer Security, 2020.L. Oakley, A. Oprea, and S. Tripakis, “Adversarial Robustness of AI Agents Acting in Probabilistic Environments”, in Workshop on Foundations of Computer Security, 2020.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, vol. 18, no. 5s, pp. 1-22, 2019.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, vol. 18, no. 5s, pp. 1-22, 2019.A. Bianco and L. De Alfaro, “Model checking of probabilistic and nondeterministic systems”, in Foundations of Software Technology and Theoretical Computer Science, 1995, pp. 499-513.A. Bianco and L. De Alfaro, “Model checking of probabilistic and nondeterministic systems”, in Foundations of Software Technology and Theoretical Computer Science, 1995, pp. 499-513.M. Belkin and P. Niyogi, “Laplacian eigenmaps and spectral techniques for embedding and clustering”, in Proceedings of the 14th International Conference on Neural Information Processing Systems: Natural and Synthetic, 2002, pp. 585-591.M. Belkin and P. Niyogi, “Laplacian eigenmaps and spectral techniques for embedding and clustering”, in Proceedings of the 14th International Conference on Neural Information Processing Systems: Natural and Synthetic, 2002, pp. 585-591.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, vol. 518, no. 7540, pp. 529-533, 2015.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, vol. 518, no. 7540, pp. 529-533, 2015.J. R. Norris, Markov chains. Cambridge University Press, 1998.J. R. Norris, Markov chains. Cambridge University Press, 1998.C. Szegedy, V. Vanhoucke, S. Ioffe, J. Shlens, and Z. Wojna, “Rethinking the Inception architecture for computer vision”, in IEEE Conference on Computer Vision and Pattern Recognition, 2016, pp. 2818-2826.C. Szegedy, V. Vanhoucke, S. Ioffe, J. Shlens, and Z. Wojna, “Rethinking the Inception architecture for computer vision”, in IEEE Conference on Computer Vision and Pattern Recognition, 2016, pp. 2818-2826.C. Barrett and C. Tinelli, “Satisfiability Modulo Theories”, in Handbook of Model Checking, E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Eds. Cham: Springer International Publishing, 2018, pp. 305-343.C. Barrett and C. Tinelli, “Satisfiability Modulo Theories”, in Handbook of Model Checking, E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Eds. Cham: Springer International Publishing, 2018, pp. 305-343.L. De Moura and N. Bjørner, “Z3: An efficient SMT solver”, in Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 337-340.L. De Moura and N. Bjørner, “Z3: An efficient SMT solver”, in Tools and Algorithms for the Construction and Analysis of Systems, 2008, pp. 337-340.A. Meurer, C. P. Smith, M. Paprocki, O. Cˇ ertı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, vol. 3, e103, 2017.A. Meurer, C. P. Smith, M. Paprocki, O. Cˇ ertı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, vol. 3, e103, 2017.

The authors declare that there are no conflicts of interest present.