PaperlayerView exact revision on arXiv

Source-linked AI summary

Marabou 2.0: A Versatile Formal Analyzer of Neural Networks

Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz, Clark Barrett

arXiv:2401.14461v2cs.AIcs.LGcs.LO

TL;DR

Marabou’s original system description no longer reflects the tool’s expanded capabilities, motivating a comprehensive account of version 2.0. The paper describes its architecture and applications, reporting strong competition results and improved runtime and memory use compared with an early version.

  • Problem

    Marabou’s earlier system description no longer accurately represents the tool’s capabilities after substantial changes since its initial release.

    Source: §1 · p. 1

  • Method

    The paper provides a comprehensive description of Marabou 2.0’s architecture, features, and applications, including network-level reasoning and proof production.

    Source: §1 · pp. 1–2, Network-level Reasoner · p. 4, §2.3 · p. 6

  • Results

    At VNN-COMP’23, Marabou placed second overall and ranked highest among CPU-based verifiers.

    Source: §3 · p. 8

  • Takeaways & Limitations

    Marabou is presented as a versatile, user-friendly toolkit for formal analysis across a wide range of tasks, with examples spanning explanation, robotics, and proof production.

    Source: Formal XAI · p. 8, Analyzing learning-based robotic systems · p. 9, Proof production for the ACAS-Xu… · p. 9

    Proof-production mode currently supports only a subset of Marabou’s features, with support for remaining features such as parallel solving still in progress.

    Source: §2.3 · p. 7

Abstract

from arXiv · show

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.

1 Introduction

Marabou 2.0 is a comprehensive system description of a tool whose capabilities have evolved substantially since its initial release. The paper presents those changes and reports performance evidence from VNN-COMP’23 and runtime comparisons with an earlier version.

1 Introduction

  • Formal analysis of DNNs has become a growing research area, with multiple DNN reasoners proposed in recent years.Examples include α-β-CROWN, ERAN, and Marabou.Source: §1 · p. 1
  • Marabou began as a from-scratch reimplementation of Reluplex, and has since undergone algorithmic, engineering, and implementation changes.The tool has been used in a wide range of formal DNN reasoning applications.Source: §1 · p. 1
  • Marabou 2.0 adds a new build/test system, optimized architecture and decision procedures, more activation functions, proof production, additional input formats, and a more powerful Python API.The paper aims to provide an accurate description of the tool’s current capabilities.Source: §1 · p. 1
  • The paper reports VNN-COMP’23 results and runtime comparisons against an early Marabou version as evidence of performance.The introduction also describes recent uses of the tool.Source: §1 · p. 2

2 Architecture and Core Components

Marabou 2.0 checks satisfiability of neural-network verification queries through an Engine that coordinates preprocessing, network-level reasoning, and constraint solving. Its components add support for broader reasoning, parallel solving, proof certificates, and multiple user interfaces.

2 Architecture and Core Components

  • The Engine checks an InputQuery of linear and nonlinear constraints, coordinating preprocessing, network reasoning, an SMT Solver, and optional (MI)LP solving; additional modules provide parallel and CEGAR solving.The front end supplies queries, typically encoding neural networks and their properties.Source: §2 · p. 2, §2.1 · p. 3

Preprocessor.

  • Preprocessing normalizes and simplifies queries, including bound propagation, which can remove piecewise-linear constraints that collapse to linear ones.A data-structure optimization in Marabou 2.0 speeds up iterative bound propagation by about 60x; preprocessing also merges equal variables and removes constants.Source: Preprocessor · p. 3

SMT Solver; 2.2 Context-Dependent Data-Structures

  • The SMT Solver uses lazy-DPLL(T) case analysis and DeepSoI to search for satisfying assignments; case splits and backtracking use context-dependent data structures to save and restore bounds and constraint phases.DeepSoI uses a violation cost and informs branching heuristics; bound-based case splits avoid adding equations and reduce Simplex runtime by over 50%.Source: SMT Solver · pp. 3–4, §2.2 · p. 6

Network-level Reasoner.

  • The Network-level Reasoner runs bound analyses at search states and feeds tightened bounds back to the SMT Solver.It implements seven analyses; DeepPoly/CROWN is the default, and the network topology can be inferred from constraints when possible.Source: Network-level Reasoner · pp. 4–5

(MI)LP Interface; Multi-thread Manager.

  • The (MI)LP interface can encode constraints precisely or with convex relaxations, while the Multi-thread Manager supports split-and-conquer and portfolio modes.Gurobi can be used for MILP solving; split-and-conquer partitions queries, while portfolio workers solve the same query with different random seeds.Source: (MI)LP Interface · p. 5, Multi-thread Manager · p. 5

CEGAR Solver.

  • The CEGAR Solver uses incremental linearization to reason more precisely about nonlinear constraints that are not piecewise linear.It currently supports Sigmoid and Tanh and can be extended to other activation functions.Source: CEGAR Solver · pp. 5–6

2.3 Proof Module

  • In proof-production mode, Marabou builds a proof tree with witnesses for lemmas and UNSAT subqueries, then checks the tree’s lemmas and leaves.Proof production is currently compatible with only a subset of Marabou features, including not all parallel-solving features.Source: §2.3 · pp. 6–7

2.4 Front End; 2.5 Availability, License, and Installation

  • The front end accepts network and property files or manually specified constraints through command-line, Python, and C++ interfaces; ONNX is the main network format and VNN-LIB is supported for properties.A Pythonic API layer offers more succinct constraint definitions; Marabou is available for Linux and macOS under a modified BSD license and through PyPI.Source: §2.4 · p. 7, §2.5 · p. 8

3 Highlighted Features and Applications

Marabou 2.0 is presented as a versatile analyzer whose features support applications beyond conventional verification, including fairness, explanations, robotics, and proof production. The section illustrates these uses and describes their supported scope.

Verifying the Decima job scheduler.

  • Marabou verified strategy-proofness for Decima, finding the property holds for most examined job profiles but is violated in some cases.The Python API enables manual encoding of the GNN and specification as linear and nonlinear constraints; the Network-level Reasoner infers its feed-forward structure with residual connections.Source: Verifying the Decima job scheduler · p. 8

Formal XAI.

  • Formal abductive explanations are provably sufficient input-feature subsets, with applications reported in computer vision, NLP, and DRL robotic navigation.Marabou has been used as a sub-routine in procedures for producing formal, provable DNN explanations.Source: Formal XAI · pp. 8–9

Analyzing learning-based robotic systems.

  • For robotic systems, Marabou encodes k-step policies, transitions, and loop closure to search for infinite loops, including cases gradient or optimization methods did not find.The detected loops have also been observed in the real world.Source: Analyzing learning-based robotic systems · p. 9

Proof production for the ACAS-Xu benchmarks.

  • Marabou produced unsatisfiability certificates for 113 of 180 ACAS-Xu benchmarks, with mild proof-generation and certification overhead.More than 99.99% of over 1.46 million proof-tree leaves were certified by the native checker; a trusted SMT solver certified the remainder.Source: Proof production for the ACAS-Xu… · p. 9

Specifications on neural activation patterns.

  • NAP specifications can be encoded through API constraints, including activating a ReLU by setting its input variable’s lower bound to 0.The Preprocessor and Network-level Reasoner can propagate internal-neuron constraints to tighten bounds.Source: Specifications on neural activation… · pp. 9–10

Robustness against semantically meaningful perturbations.

  • Marabou has verified perception-network robustness to semantically meaningful input perturbations and properties relating classifier outputs to a generative model.The Python API can load the classifier and generator and add constraints on or between their input and output variables.Source: Robustness against semantically… · p. 10

Minimal modifications of neural networks; Pruning and slicing neural networks.

Integrating Marabou into complex system verification.

  • Vehicle uses Marabou as its default verifier because its syntax is richer and more flexible than that of more specialized neural-network verifiers.Vehicle aims to bridge the gap between domain-level complex-system properties and low-level neural-network properties.Source: Pruning and slicing neural networks · p. 11

4 Runtime Evaluation

The runtime evaluation compares Marabou 2.0 with an early version across 745 instances from four application benchmark sets. Marabou 2.0 is substantially faster on most instances and uses less peak memory at the median.

4 Runtime Evaluation

  • At least 2× speed-up occurred on 428 instances and at least 10× speed-up on 263 instances.The comparison used a one-hour CPU timeout, one core, and 8GB memory per configuration; Marabou 2.0 had no external solvers configured.Source: §4 · pp. 11–12, Figure 3 · p. 11
  • Marabou 2.0 had median peak memory usage of 57MB, versus 604MB for the early version.The benchmark collection comprised 745 instances from Alternating Loop, DeepCert, NAP, and VeriX.Source: §4 · pp. 11–12

5 Conclusion and Next Steps

The conclusion characterizes Marabou as a versatile, user-friendly analyzer for neural-network-enabled systems that remains under active development. Planned work includes solver, hardware, and nonlinear-constraint capabilities.

5 Conclusion and Next Steps

  • Marabou is described as a versatile, user-friendly toolkit for a wide range of formal analysis tasks, with active development continuing.Planned work includes integrating CDCL, incremental solving, GPU support in the Network-level Reasoner, and handling other nonlinear constraints.Source: §5 · p. 12

A.1 Supported Non-linear Constraints in Marabou 2.0

The table lists supported nonlinear-constraint types and marks their handling across Marabou components. Support varies by type and component.

A.1 Supported Non-linear Constraints in Marabou 2.0

  • The table marks ReLU, Max, DNF, Sign, absolute value, and Leaky ReLU as supported across Preprocessing, NLR, SMT, and (MI)LP, but not CEGAR; proof support is marked for all except none of these six.Round and Clip are marked supported in Preprocessing, NLR, SMT, and (MI)LP, but not CEGAR or Proof; Sigmoid and Tanh are marked supported in Preprocessing, NLR, and (MI)LP, with CEGAR but not SMT or Proof.Source: §A.1 · p. 18
  • Softmax and bi-linear constraints are marked supported in Preprocessing, NLR, and (MI)LP, but not SMT, CEGAR, or Proof.Source: §A.1 · p. 18

B Marabou in VNN-COMP 2023 [11]

At VNN-COMP’23, Marabou placed second overall and scored highest among CPU-based verifiers, while trailing GPU-based solvers especially on larger networks.

B Marabou in VNN-COMP 2023 [11]

C.1 Descriptions of the Benchmarks

The benchmark descriptions cover contextual image perturbations, robot-navigation loops, mined neural activation patterns, and formal explanations; the NAP robustness benchmarks were not yet publicly available.

C.1 Descriptions of the Benchmarks

  • DeepCert evaluates haze perturbations on image classifier model 2A for GTSRB, drawing on a study of contextual image robustness.Source: §C.1 · p. 18
  • Alternating Loop benchmarks examine whether infinite loops exist in a robot-navigation system.Source: §C.1 · p. 18
  • NAP benchmarks check the robustness of mined NAPs on ACAS-Xu networks, but the referenced robustness benchmarks were not yet publicly available.Source: §C.1 · pp. 18–19
  • VeriX benchmarks involve repeatedly querying Marabou during formal explanation extraction on an MNIST classifier.The classifier is the same one used in the original work.Source: §C.1 · p. 19

C.2 Solver Performance on Individual Benchmarks

The supplied table headers identify solver versions and comparison fields, but provide no readable benchmark outcomes.

C.2 Solver Performance on Individual Benchmarks

  • The comparison is organized by family and benchmark, with Result, Time, and Mem. fields for Marabou 2.0 and Marabou (1c1c66).Source: §C.2 · pp. 19, 23
Loading 2401.14461v2…