Reachability in Simple Neural Networks

• Autorzy: Sälzer Marco , Lange Martin

Identyfikatory

DOI

10.3233/FI-222160

• Języki publikacji: EN

Abstrakty

EN

We investigate the complexity of the reachability problem for (deep) neural networks: does it compute valid output given some valid input? It was recently claimed that the problem is NP-complete for general neural networks and specifications over the input/output dimension given by conjunctions of linear inequalities. We recapitulate the proof and repair some flaws in the original upper and lower bound proofs. Motivated by the general result, we show that NP-hardness already holds for restricted classes of simple specifications and neural networks. Allowing for a single hidden layer and an output dimension of one as well as neural networks with just one negative, zero and one positive weight or bias is sufficient to ensure NP-hardness. Additionally, we give a thorough discussion and outlook of possible extensions for this direction of research on neural network verification.

Słowa kluczowe

EN

machine learning; computational complexity; formal specification and verification

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2022
• Tom: Vol. 189, nr 3-4
• Strony: 241--259
• Opis fizyczny: Bibliogr. 22 poz., rys.

Twórcy

autor

Sälzer Marco

• School of Electr. Eng. and Computer Science University of Kassel, Germany

autor

Lange Martin

• School of Electr. Eng. and Computer Science University of Kassel, Germany

Bibliografia

• [1] Krizhevsky A, Sutskever I, Hinton GE. ImageNet classification with deep convolutional neural networks. Commun. ACM, 2017. 60(6):84-90. doi:10.1145/3065386.
• [2] Hinton G, Deng L, Yu D, Dahl GE, Mohamed Ar, Jaitly N, Senior A, Vanhoucke V, Nguyen P, Sainath TN, et al. Deep Neural Networks for Acoustic Modeling in Speech Recognition: The Shared Views of Four Research Groups. IEEE Signal Process. Mag., 2012. 29(6):82-97. doi:10.1109/MSP.2012.2205597.
• [3] Grigorescu SM, Trasnea B, Cocias TT, Macesanu G. A survey of deep learning techniques for autonomous driving. J. Field Robotics, 2020. 37(3):362-386. doi:10.1002/rob.21918.
• [4] Litjens G, Kooi T, Bejnordi BE, Setio AAA, Ciompi F, Ghafoorian M, van der Laak JAWM, van Ginneken B, S´anchez CI. A survey on deep learning in medical image analysis. Medical Image Anal., 2017. 42:60-88. doi:10.1016/j.media.2017.07.005.
• [5] Dixon M, Klabjan D, Bang JH. Classification-based financial markets prediction using deep neural networks. Algorithmic Finance, 2017. 6(3-4):67-77. doi:10.3233/AF-170176.
• [6] Huang X, Kroening D, Ruan W, Sharp J, Sun Y, Thamo E, Wu M, Yi X. A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence and interpretability. Comput. Sci. Rev., 2020. 37:100270. doi:10.1016/j.cosrev.2020.100270.
• [7] Katz G, Barrett CW, Dill DL, Julian K, Kochenderfer MJ. Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. In: Majumdar R, Kuncak V (eds.), Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, volume 10426 of Lecture Notes in Computer Science. Springer, 2017 pp. 97-117. doi:10.1007/978-3-319-63387-9 5.
• [8] Ehlers R. Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks. In: D’Souza D, Kumar KN (eds.), Automated Technology for Verification and Analysis - 15th International Symposium, ATVA 2017, Pune, India, October 3-6, 2017, Proceedings, volume 10482 of Lecture Notes in Computer Science. Springer, 2017 pp. 269-286. doi:10.1007/978-3-319-68167-2 19.
• [9] Narodytska N, Kasiviswanathan SP, Ryzhyk L, Sagiv M, Walsh T. Verifying Properties of Binarized Deep Neural Networks. In: McIlraith SA, Weinberger KQ (eds.), Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018. AAAI Press, 2018 pp. 6615-6624. URL https://www.aaai.org/ocs/index.php/AAAI/AAAI18/paper/view/16898.
• [10] Bunel R, Turkaslan I, Torr PHS, Kohli P, Mudigonda PK. A Unified View of Piecewise Linear Neural Network Verification. In: Bengio S, Wallach HM, Larochelle H, Grauman K, Cesa-Bianchi N, Garnett R (eds.), Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montréal, Canada. 2018 pp. 4795-4804. URL https://proceedings.neurips.cc/paper/2018/hash/be53d253d6bc3258a8160556dda3e9b2-Abstract.html.
• [11] Ruan W, Huang X, Kwiatkowska M. Reachability Analysis of Deep Neural Networks with Provable Guarantees. In: Lang J (ed.), Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden. ijcai.org, 2018 pp. 2651-2659. doi:10.24963/ijcai.2018/368. M. Sӓlzer and M. Lange / Reach. Is NP-Complete Even for the Simplest NN 259
• [12] Ruan W, Huang X, Kwiatkowska M. Reachability Analysis of Deep Neural Networks with Provable Guarantees. CoRR, 2018. abs/1805.02242. 1805.02242, URL http://arxiv.org/abs/1805.02242.
• [13] Katz G, Barrett CW, Dill DL, Julian K, Kochenderfer MJ. Reluplex: a calculus for reasoning about deep neural networks. Form Methods Syst Des, 2021. doi:10.1007/s10703-021-00363-7.
• [14] Sӓlzer M, Lange M. Reachability is NP-Complete Even for the Simplest Neural Networks. In: Reachability Problems - 15th International Conference, RP 2021, Liverpool, UK, October 25-27, 2021, Proceedings,
• volume 13035 of Lecture Notes in Computer Science. Springer, 2021 pp. 149-164. doi:10.1007/978-3-030-89716-1 10.
• [15] Karmarkar N. A new polynomial-time algorithm for linear programming. Comb., 1984. 4(4):373-396. doi:10.1007/BF02579150.
• [16] Akintunde M, Lomuscio A, Maganti L, Pirovano E. Reachability Analysis for Neural Agent-Environment Systems. In: Thielscher M, Toni F, Wolter F (eds.), Principles of Knowledge Representation and Reasoning: Proceedings of the Sixteenth International Conference, KR 2018, Tempe, Arizona, 30 October - 2 November 2018. AAAI Press, 2018 pp. 184-193. URL https://aaai.org/ocs/index.php/KR/KR18/paper/view/17991.
• [17] Karp RM. Reducibility Among Combinatorial Problems. In: Miller RE, Thatcher JW (eds.), Proceedings of a symposium on the Complexity of Computer Computations, held March 20-22, 1972, at the IBM Thomas J. Watson Research Center, Yorktown Heights, New York, USA, The IBM Research Symposia Series. Plenum Press, New York, 1972 pp. 85-103. doi:10.1007/978-1-4684-2001-2 9.
• [18] Korte B, Vygen J. Combinatorial Optimization. Springer Berlin, Heidelberg, 2006. ISBN 978-3-540-29297-5. doi:10.1007/3-540-29297-7.
• [19] Khan A, Sohail A, Zahoora U, Qureshi AS. A survey of the recent architectures of deep convolutional neural networks. Artif. Intell. Rev., 2020. 53(8):5455-5516. doi:10.1007/s10462-020-09825-6.
• [20] Wu Z, Pan S, Chen F, Long G, Zhang C, Yu PS. A Comprehensive Survey on Graph Neural Networks. IEEE Trans. Neural Networks Learn. Syst., 2021. 32(1):4-24. doi:10.1109/TNNLS.2020.2978386.
• [21] Sӓlzer M, Lange M. Fundamental Limits in Formal Verification of Message-Passing Neural Networks. In: The Eleventh International Conference on Learning Representations. 2023 URL https://openreview.net/forum?id=WlbG820mRH-.
• [22] Stockmeyer LJ. The polynomial-time hierarchy. Theor. Comp. Sci., 1976. 3(1):1-22