Marabou

Framework for Verification and Analysis of DNNs

  Guy Katz
  Aleksandar Zeljić
   Clark Barrett
Haoze Wu
et al.           
Hebrew University
Stanford University

Overview


\input{images/dnn.tex}

 


Reachability properties:

$ x \in [x_l, x_u] \Rightarrow y \in [y_l, y_u] $


Robustness properties:

$ \exists x'. |{\bf x} - x'| < \epsilon \land | {\bf y} - y' | > \Delta $

Reluplex

Linear wighted sum   +    Piece-wise linear function
\[\relu{x} = max(0,x) = \begin{cases*} x, & if $x > 0$ \\ 0, & if $ x \leq 0 $ \\ \end{cases*} \]

Fixing all ReLUs $\rightarrow$ linear problem

$300$ ReLUs $\rightarrow 2^{300}$ cases

Simplex   +    Case-splitting

Linear problem

graphic-4

Added piece-wise linear constraints

graphic-5

Initial assignment

graphic-6

Update NonBasic Variable

graphic-7

Cannot Update Basic Variable

graphic-8

Pivot

graphic-9

And the search goes on…

graphic-10

When we satisfy linear constraints …

graphic-11

Check piece-wise linear constraints

graphic-12

When repeatedly broken

graphic-13

Split

graphic-14

Solution

graphic-15

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

graphic-17

Manging the state space size

  • ReLU splits - guesses to simplify the problem

    • exponential search space

    • Independents splits $\rightarrow$ 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

graphic-22

Estimate activations in region

graphic-23

Estimate state space

graphic-24

Activation distribution

graphic-25

Comparing distributions

graphic-26

Choose uneven distribution

graphic-27

Try with a small timeout

graphic-29

It times out

graphic-30

Split and increase timeout

graphic-31

Some are UNSAT

graphic-32

Some TIMEOUT

graphic-33

SAT

graphic-34

Divide & Conquer summary

TIMEOUT:

  • choose a dimension
  • split into $N$ problems
  • scale the timeout
  • queue $N$ problems

SAT:

  • stop other runs
  • return SAT


ALL UNSAT:

  • return UNSAT;

Evaluation

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

Runtime comparison:

Benchmark set Marabou Reluplex ReluVal Planet
ACAS Xu (135) ✔ ✔ ✔ ✔
TwinStream (81) ✔ ✔
CollisionAvoidance (500) ✔ ✔

Scaling experiment:

  • Marabou vs ReluVal
  • Runtime comparison on ACAS Xu
  • Increasing number of cores: 2, 4, 8, 16, 32, 64

stamp

Marabou vs Relu*

vsReluplex

vsReluval

Marabou vs Planet

vsPlanetACAS

vsPlanetCATS

Scalability of Divide & Conquer

scaling

Marabou - tool for DNN verification and analysis

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

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

    • Properties: .txt, via Python interface

  • Network-level reasoning - Symbolic bound tightening

  • Parallel Divide & Conquer algorithm


AVAILABLE TODAY https://​github.​com/​guykatzz/​Marabou/​

Authors

  • Guy Katz
  • Derek A. Huang
  • Duligur Ibeling
  • Kyle Julian
  • Christopher Lazarus
  • Rachel Lim
  • Parth Shah
  • Shantanu Thakoor
  • Haoze Wu
  • Aleksandar Zeljić
  • Mykel J. Kochendorfer
  • David Dill
  • Clark Barrett