Marabou

Motivating example

Input geometry

ACAS X

New implementation for aircraft colision avoidance

Model as Markov Decision Process solve using DP:

• Lookup table ~100s GB
• Down-sample by removing smooth table states ~2GB
• Train a DNN: ~3MB

Motivation

Instead of hand-crafting complex software:

• Train deep learning models that solve the problem
• Very successul: Image recognition, game AI (Go, StarCraft), …

Application in safety critical domains?

• Lack of transparency and trust, e.g. adversarial examples
• Need for explainability, certification, and verification

Verification of Neural Networks

Traditionally:

In Machine Learning:

Open questions:

• What are the specifications?
• How do we fix implementations?
• What is the correct semantics? Reals vs. Floats

VNN problem

Approaches to VNN

Reachability

• AI, MaxSens, ExactReach

Optimization

• MIPVerify,NSVerify,ILP, Duality, ConvDual, Certify

Search and Optimization

• Sherlock, Planet, BaB, Reluplex/Marabou

Search and Reachability

• FastLin, FastLip, DVL, ReluVal/Neurify

Reluplex

Linear problem

Added piece-wise linear constraints

Initial assignment

Update NonBasic Variable

Cannot Update Basic Variable

Pivot

And the search goes on…

When we satisfy linear constraints …

Check piece-wise linear constraints

When repeatedly broken

Split

Solution

Marabou

• Re-implementation of Reluplex algorithm

• FCFF and Convolutional DNNs with piece-wise linear activation functions

  • Network formats: .nnet, .pb (TensorFlow)

  • Properties: .txt, via Python interface

• Own simplex core replaces GLPK
• Network-level reasoning - Symbolic bound tightening
• Parallel Divide & Conquer algorithm

Architecture overview

Search

1. Simplex - finds a satisfying assignment of linear constraints

   • Updates and Pivots

2. SMT - manages splits of piece-wise linear constraints

   • Splitting and Backtracking
   • Currently very simple

3. Bound tightening - propagates bounds through the network

   • Forces ReLUs into a single case

Manging the state space size

• ReLU splits - guesses to simplify the problem

  • exponential search space

  • Independents splits spurious search space

How can we focus the search?

Narrowing input ranges can fix hundreds of ReLUs

Which ranges do we choose? On which inputs?

RELU Activation patterns

Estimate activations in region

Estimate state space

Activation distribution

Comparing distributions

Choose unbalanced distribution

Try with a small timeout

It times out

Split and increase timeout

Some are UNSAT

Some TIMEOUT

SAT

Divide & Conquer summary

Evaluation

./marabou --dnc --num-workers=4 --online-split=4 --init-to=5s --to-factor=1.5

Runtime comparison:

Marabou vs Relu*

Marabou vs Planet

Scalability of Divide & Conquer

Ongoing work - Parallelization

• Partitioning strategy:

  • Direct ReLU Splitting - targets perception networks
  • Balanced splits - lighter, and better performance

• Polarity-based branching - targets SAT instances

• Pre-processing - probe for ReLUs with fixed polarity

• CDCL solver integration and lifting the Boolean structure

TaxiNet - Preliminary results

Marabou - tool for DNN verification and analysis

• FCFF and Conv. DNNs with p.w. linear activation functions

  • NN formats: .nnet, .pb (TensorFlow), .onnx (in progress)

  • Properties: .txt, via Python interface

• Network-level reasoning - Symbolic bound tightening

• Parallel Divide & Conquer algorithm

https://​github.​com/​neuralnetworkverification/​Marabou/​

Authors

• Guy Katz