Marabou swMATH ID: 31368 Software Authors: Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S.,Wu, H., Zelji ́c, A., Dill, D.L., Kochenderfer, M.J., Barrett, C. Description: The Marabou Framework for Verification and Analysis of Deep Neural Networks. Deep neural networks are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that need, we present Marabou, a framework for verifying deep neural networks. Marabou is an SMT-based tool that can answer queries about a network’s properties by transforming these queries into constraint satisfaction problems. It can accommodate networks with different activation functions and topologies, and it performs high-level reasoning on the network that can curtail the search space and improve performance. It also supports parallel execution to further enhance scalability. Marabou accepts multiple input formats, including protocol buffer files generated by the popular TensorFlow framework for neural networks. We describe the system architecture and main components, evaluate the technique and discuss ongoing work. Homepage: https://rd.springer.com/chapter/10.1007/978-3-030-25540-4_26 Source Code: https://github.com/NeuralNetworkVerification/Marabou Related Software: Reluplex; MNIST; XNOR-Net; PRODeep; DeepFool; NNV; ReachNN; AI2; VERIFAI; Fashion-MNIST; AlexNet; ImageNet; GitHub; NeuralCDE; torchcde; Diffrax; JuliaReach; nnenum; Verisig; GoTube Cited in: 8 Publications all top 5 Cited by 40 Authors 2 Hamilton, Nathaniel P. 2 Johnson, Taylor T. 2 Manzanas Lopez, Diego 2 Musau, Patrick 1 Amir, Guy 1 Bak, Stanley 1 Bao, Yang 1 Barrett, Clark W. 1 Bodeveix, Jean-Paul 1 Chen, Guangke 1 Chen, Liqian 1 Chen, Taolue 1 Deshmukh, Jyotirmoy V. 1 Filali, Mamoun 1 Goubault, Eric 1 Gu, Zonghua 1 Huang, Chengchao 1 Huang, Xiaowei 1 Huang, Zhiqiu 1 Katz, Guy 1 Li, Renjue 1 Liu, Jiangchao 1 Mohammadinejad, Sara 1 Pal, Neelanjana 1 Palumby, Sébastien 1 Paulsen, Brandon 1 Putot, Sylvie 1 Rustenholz, Louis 1 Sankaranarayanan, Sriram 1 Song, Fu 1 Tran, Hoang-Dung 1 Wang, Chao 1 Wu, Haoze 1 Yang, Pengfei 1 Yang, Xiaodong 1 Yang, Yongqiang 1 Yang, Zhibin 1 Zhang, Lijun 1 Zhang, Yedi 1 Zhao, Zhe Cited in 1 Serial 2 Formal Aspects of Computing Cited in 3 Fields 8 Computer science (68-XX) 1 Algebraic geometry (14-XX) 1 Convex and discrete geometry (52-XX) Citations by Year