The Marabou Framework for Verification and Analysis of Deep Neural Networks
By Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle D. Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić and 3 more. International Conference on Computer Aided Verification, 2019
622 citations recorded by the source corpus.
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.
Subfields: Artificial Intelligence
View Paper: https://www.semanticscholar.org/paper/3c742ebff7df12e3fd0194023975e2211e4ba67a
How researchers see this paper
The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.
In Artificial Intelligence
- Joelle Pineau
- Amy Zhang
- Clark W. Barrett
- Shagun Sodhani
- F. Meier
- Mykel J. Kochenderfer
- Christopher Lazarus
- Tomer Arnon
Citations in the corpus
- Algorithms for Verifying Deep Neural Networks (2019, methodology): “Representative methods for search and optimization include Reluplex [30], Marabou [31], Planet [32], Sherlock [33], Venus [34], PeregriNN [35], and BaB [36] and its extensions [20], [37], [38].”
- Provable repair of deep neural networks (2021, neutral): “Prior work on DNN verification focused on safety and robustness [4, 6, 11, 15, 18, 30, 33, 34, 49].”
- Block Contextual MDPs for Continual Learning (2021, methodology): “We do not perform this type of formal verification, as current verification methods on neural networks only work for very small models, and are expensive to run (Katz et al., 2019).”
- SurveyGen-I: Consistent Scientific Survey Generation with Evolving Plans and Memory-Guided Writing (2025, unknown): “SurveyForge and SurveyX trail significantly, especially in foundational domains like Learning Algorithms and Big Data , reflecting weaker temporal grounding.”