Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

TL;DR

This paper presents Marabou 2.0, a versatile formal analyzer for neural networks, addressing the need for rigorous verification, explainability, and safe integration of neural networks into complex systems. It introduces an optimized architecture with an Engine (Preprocessor, SMT Solver with DeepSoI, and MILP/LP interface), a Network-level Reasoner, context-dependent data structures, a Proof Module, and a modern Front End. The paper also demonstrates a broad set of applications, including Decima scheduling verification, formal XAI, robotic systems, ACAS-Xu, and quantized networks, with competitive runtime performance on VNN-COMP'23. Future work targets CDCL integration, incremental solving, GPU acceleration, and tackling additional non-linear constraint handling to further broaden Marabou's applicability.

Abstract

This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool's architectural design and highlight the major features and components introduced since its initial release.

Figures (3)

• Figure 1: High-level overview of Marabou 2.0's system architecture.
• Figure 2: Two ways to define the same verification query through the Python API.
• Figure 3: Runtime performance of Marabou 2.0 and an early version of Marabou on four applications supported by both versions.