AI2 swMATH ID: 40547 Software Authors: Gehr, T.; Mirman, M.; Drachsler-Cohen, D.; Tsankov, P.; Chaudhuri, S.; Vechev, M.T. Description: AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation. We present AI 2 , the first sound and scalable analyzer for deep neural networks. Based on overapproximation, AI 2 can automatically prove safety properties (e.g., robustness) of realistic neural networks (e.g., convolutional neural networks). The key insight behind AI 2 is to phrase reasoning about safety and robustness of neural networks in terms of classic abstract interpretation, enabling us to leverage decades of advances in that area. Concretely, we introduce abstract transformers that capture the behavior of fully connected and convolutional neural network layers with rectified linear unit activations (ReLU), as well as max pooling layers. This allows us to handle real-world neural networks, which are often built out of those types of layers. We present a complete implementation of AI 2 together with an extensive evaluation on 20 neural networks. Our results demonstrate that: (i) AI 2 is precise enough to prove useful specifications (e.g., robustness), (ii) AI 2 can be used to certify the effectiveness of state-of-the-art defenses for neural networks, (iii) AI 2 is significantly faster than existing analyzers based on symbolic analysis, which often take hours to verify simple fully connected networks, and (iv) AI 2 can handle deep convolutional networks, which are beyond the reach of existing methods. Homepage: https://ieeexplore.ieee.org/document/8418593 Related Software: Reluplex; Marabou; NNV; ImageNet; AlexNet; GitHub; Gurobi; NeuroDiff; ReluDiff; DeepXplore; DeepFool; POPQORN; ReachNN; CIFAR; z3; DiffRNN; UCI-ml; MNIST; Fashion-MNIST; DeepGauge Cited in: 38 Documents all top 5 Cited by 124 Authors 5 Katz, Guy 3 Ivanov, Radoslav 2 Alur, Rajeev 2 Barrett, Clark W. 2 Huang, Xiaowei 2 Julian, Kyle D. 2 Khedr, Haitham 2 Kochenderfer, Mykel J. 2 Lee, Insup 2 Lindemann, Lars 2 Pappas, George J. 2 Paulsen, Brandon 2 Ruan, Wenjie 2 Shoukry, Yasser 2 Wang, Chao 2 Weimer, James E. 1 Althoff, Matthias 1 Amir, Guy 1 Bak, Stanley 1 Bensalem, Saddek 1 Carpenter, Taylor J. 1 Castellini, Alberto 1 Chen, Guangke 1 Chen, Taolue 1 Cleaveland, Matthew 1 Cohen, Elazar 1 Dai, Ting 1 Deshmukh, Jyotirmoy V. 1 Dill, David L. 1 Dimitrov, Dimitar Iliev 1 Dohmen, Taylor 1 Drachsler-Cohen, Dana 1 Elboher, Yizhak Yisrael 1 Farinelli, Alessandro 1 Farjudian, Amin 1 Fatnassi, Wael 1 Ferlez, James 1 Fischer, Marc 1 Goubault, Eric 1 Gros, Timo P. 1 Günnemann, Stephan 1 Guo, Xingwu 1 Hermanns, Holger 1 Hoffmann, Jörg 1 Hoos, Holger H. 1 Hoxha, Bardh 1 Ioualalen, Arnault 1 Jia, Kai 1 Johnson, Taylor T. 1 Kabaha, Anan 1 Khurshid, Sarfraz 1 Klauck, Michaela 1 Kobayashi, Naoki 1 König, Matthias 1 Kopetzki, Anna-Kathrin 1 Kröning, Daniel 1 Ladner, Tobias 1 Li, Yannan 1 Li, Yiran 1 Lin, Vivian 1 Liu, Jiaxiang 1 Maayan, Osher 1 Martel, Matthieu 1 Mazzi, Giulio 1 Mohammadinejad, Sara 1 Palumby, Sébastien 1 Petkovic, Milena R. 1 Pham, Long H. 1 Prokhorov, Danil V. 1 Putot, Sylvie 1 Ranzato, Francesco 1 Rinard, Martin C. 1 Rössig, Ansgar 1 Rustenholz, Louis 1 Sankaranarayanan, Sriram 1 Sato, Issei 1 Schapira, Michael 1 Sekiyama, Taro 1 Shaikh, Razin A. 1 Sharp, James D. 1 Singh, Gagandeep 1 Sokolsky, Oleg 1 Soloveichik, David 1 Song, Fu 1 Sotoudeh, Matthew 1 Sprecher, Christian 1 Steinmetz, Marcel 1 Strong, Christopher A. 1 Subramani, Krishnan 1 Sun, Bing 1 Sun, Jun 1 Sun, Meng 1 Sun, Youcheng 1 Tang, Qiyi 1 Thakur, Aditya V. 1 Thamo, Emese 1 Tran, Hoang-Dung 1 Trivedi, Ashutosh 1 Unno, Hiroshi 1 van Rijn, Jan N. ...and 24 more Authors all top 5 Cited in 8 Serials 3 Machine Learning 2 Artificial Intelligence 1 Automatica 1 Mathematical Structures in Computer Science 1 Journal of Global Optimization 1 Formal Methods in System Design 1 Computer Science Review 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 8 Fields 38 Computer science (68-XX) 5 Systems theory; control (93-XX) 3 Numerical analysis (65-XX) 3 Operations research, mathematical programming (90-XX) 2 Probability theory and stochastic processes (60-XX) 1 Algebraic geometry (14-XX) 1 Ordinary differential equations (34-XX) 1 Convex and discrete geometry (52-XX) Citations by Year