Reluplex swMATH ID: 31367 Software Authors: Guy Katz, Clark Barrett, David Dill, Kyle Julian, Mykel Kochenderfer Description: Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. Deep neural networks have emerged as a widely used and effective means for tackling complex, real-world problems. However, a major obstacle in applying them to safety-critical systems is the great difficulty in providing formal guarantees about their behavior. We present a novel, scalable, and efficient technique for verifying properties of deep neural networks (or providing counter-examples). The technique is based on the simplex method, extended to handle the non-convex Rectified Linear Unit (ReLU) activation function, which is a crucial ingredient in many modern neural networks. The verification procedure tackles neural networks as a whole, without making any simplifying assumptions. We evaluated our technique on a prototype deep neural network implementation of the next-generation airborne collision avoidance system for unmanned aircraft (ACAS Xu). Results show that our technique can successfully prove properties of networks that are an order of magnitude larger than the largest networks verified using existing methods. Homepage: https://arxiv.org/abs/1702.01135 Source Code: https://github.com/guykatzz/ReluplexCav2017 Keywords: Artificial Intelligence; arXiv_cs.AI; Logic; arXiv_cs.LO; SMT Solver; Verifying; Deep Neural Networks Related Software: AI2; Marabou; Adam; NNV; MNIST; DeepFool; ImageNet; VERIFAI; Flow*; ReachNN; PyTorch; TensorFlow; DeepXplore; AlexNet; Sherlock; Verisig; SpaceEx; nncontroller; Breach; PRODeep Cited in: 29 Publications all top 5 Cited by 109 Authors 3 Huang, Xiaowei 3 Johnson, Taylor T. 3 Manzanas Lopez, Diego 3 Musau, Patrick 2 Bak, Stanley 2 Chen, Taolue 2 Hamilton, Nathaniel P. 2 Jia, Kai 2 Kochenderfer, Mykel J. 2 Pal, Neelanjana 2 Rinard, Martin C. 2 Ruan, Wenjie 2 Sankaranarayanan, Sriram 2 Tran, Hoang-Dung 2 Wu, Min 2 Yang, Xiaodong 1 Alur, Rajeev 1 Barrett, Clark W. 1 Bunel, Rudy 1 Carpenter, Taylor J. 1 Carr, Steven 1 Chen, Guangke 1 Chen, Liqian 1 Chen, Xin 1 Corso, Anthony 1 Croce, Francesco 1 Cui, Tengxiang 1 Deshmukh, Jyotirmoy V. 1 Dill, David L. 1 Dutta, Souradeep 1 Fang, Wang 1 Gambella, Claudio 1 Ghaddar, Bissan 1 Goubault, Eric 1 Guan, Ji 1 Günnemann, Stephan 1 Hein, Matthias 1 Hou, Gang 1 Hsieh, Cho-Jui 1 Huang, Chengchao 1 Huchette, Joey 1 Ivanov, Radoslav 1 Jansen, Nils 1 Jha, Susmit 1 Jiang, Yuan 1 Julian, Kyle 1 Katz, Guy 1 Kobayashi, Naoki 1 Kohli, Pushmeet 1 Kong, Weiqiang 1 Kopetzki, Anna-Kathrin 1 Koren, Mark 1 Kröning, Daniel 1 Kumar, M. Pawan 1 Kwiatkowska, Marta Z. 1 Lee, Insup 1 Lee, Ritchie 1 Li, Renjue 1 Liu, Jiangchao 1 Liu, Zhiming 1 Lu, Jingyue 1 Lv, Deyun 1 Ma, Will 1 Mohammadinejad, Sara 1 Moss, Robert J. 1 Naoum-Sawaya, Joe 1 Nguyen, Luan Viet 1 Palumby, Sébastien 1 Pappas, George J. 1 Paulsen, Brandon 1 Petkovic, Milena R. 1 Prabhakar, Pavithra 1 Putot, Sylvie 1 Rauber, Jonas 1 Rössig, Ansgar 1 Rustenholz, Louis 1 Sato, Issei 1 Sekiyama, Taro 1 Sharp, James D. 1 Song, Fu 1 Sotoudeh, Matthew 1 Sun, Youcheng 1 Thakur, Aditya V. 1 Thamo, Emese 1 Tiwari, Ashish Kumar 1 Tjandraatmadja, Christian 1 Topcu, Ufuk 1 Torr, Philip H. S. 1 Turkaslan, Ilker 1 Unno, Hiroshi 1 Vielma, Juan Pablo 1 Wang, Chao 1 Wang, Lu 1 Watanabe, Masahiko 1 Weimer, James E. 1 Wicker, Matthew 1 Woodcock, James C. P. 1 Wu, Huihui 1 Xiang, Weiming 1 Yang, Pengfei ...and 9 more Authors all top 5 Cited in 10 Serials 4 Formal Aspects of Computing 2 Machine Learning 2 The Journal of Artificial Intelligence Research (JAIR) 1 Theoretical Computer Science 1 Journal of Global Optimization 1 European Journal of Operational Research 1 Mathematical Programming. Series A. Series B 1 International Journal of Computer Vision 1 Journal of Machine Learning Research (JMLR) 1 Computer Science Review all top 5 Cited in 9 Fields 28 Computer science (68-XX) 3 Numerical analysis (65-XX) 3 Operations research, mathematical programming (90-XX) 2 Systems theory; control (93-XX) 1 Algebraic geometry (14-XX) 1 Ordinary differential equations (34-XX) 1 Convex and discrete geometry (52-XX) 1 Statistics (62-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year