Marabou

Framework for DNN Verification and Analysis

Aleksandar Zeljić
Stanford University

Motivating example

generalCA

Input geometry

hgeometry

ACAS X

New implementation for aircraft colision avoidance

Encounter geometry $\rightarrow$ ACAS X $\rightarrow$ Advisory


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:

Specification + Implementation + Decision Procedures

In Machine Learning:

? + DNN + Marabou

Open questions:

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

VNN problem


\input{images/dnn.tex}

 


Input-Ouput properties:

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


Robustness properties:

$ |{\bf x} - x'| < \epsilon \Rightarrow | {\bf y} - y' | < \Delta $

Approaches to VNN

Reachability

  • AI$^2$, 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 wighted sum   +    Piece-wise linear function
\[\relu{x} = max(0,x) = \begin{cases*} x, & if $x > 0$ \\ 0, & if $ x \leq 0 $ \\ \end{cases*} \]

Fix 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 unbalanced distribution

graphic-27

Try with a small timeout

graphic-29

It times out

graphic-30

Split and increase timeout