На пути к нейросетевой маршрутизации с верифицированными границами эффективности

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

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, vol. 94, pp. 587-600, 2019.

2. 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.

3. 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.

4. 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.

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”, in IEEE/CVF Conference on Computer Vision and Pattern Recognition, 2018, pp. 1625-1634.

6. 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.

7. R. Drechsler, Ed., Advanced formal verification. 2004, vol. 122.

8. 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.

9. 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.

10. Y. Y. Elboher, J. Gottschlich, and G. Katz, “An abstraction-based framework for neural network verification”, in Computer Aided Verification, 2020, pp. 43-65.

11. X. Huang, M. Kwiatkowska, S. Wang, and M. Wu, “Safety verification of deep neural networks”, in Computer Aided Verification, 2017, pp. 3-29.

12. 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.

13. 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.

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, vol. 40, no. 2, pp. 189-200, 2009.

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), vol. 40, no. 3, pp. 341-351, 2010.

16. 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.

17. 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.

18. A. Fawzi, O. Fawzi, and P. Frossard, “Analysis of classifiers’ robustness to adversarial perturbations”, Machner Learning, vol. 107, no. 3, pp. 481-508, 2018.

19. 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.

20. 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.

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”, in Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence, vol. 33, 2019, pp. 3240-3247.

22. 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.

23. 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.

24. A. Raghunathan, J. Steinhardt, and P. Liang, “Certified Defenses against Adversarial Examples”, in 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”, in NIPS Deep Learning Workshop, 2013.

26. R. S. Sutton, A. G. Barto, et al., Introduction to reinforcement learning. MIT press, 1998, vol. 135.

27. 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.

28. 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.

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”, in Proceedings of the 23rd International Conference on Hybrid Systems: Computation and Control, 2020, pp. 1-7.

30. 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.

31. 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.

32. L. Oakley, A. Oprea, and S. Tripakis, “Adversarial Robustness of AI Agents Acting in Probabilistic Environments”, in 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, vol. 18, no. 5s, pp. 1-22, 2019.

34. 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.

35. 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.

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, vol. 518, no. 7540, pp. 529-533, 2015.

37. J. R. Norris, Markov chains. Cambridge University Press, 1998.

38. 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.

39. 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.

40. 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.

41. 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.