Aleksandar Zeljić
Stanford University
ARGO Seminar, Feb 2020 
ACAS X
New implementation for aircraft colision avoidance
Encounter geometry ACAS X Advisory
Model as Markov Decision Process solve using DP:
 Lookup table ~100s GB
 Downsample by removing smooth table states ~2GB
 Train a DNN: ~3MB
Motivation
Instead of handcrafting 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:
Open questions:
 What are the specifications?
 How do we fix implementations?
 What is the correct semantics? Reals vs. Floats
VNN problem

 

InputOuput properties:
Robustness properties:

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 wighted sum +
Piecewise linear function
Fix all ReLUs linear problem
ReLUs cases
Simplex +
Casesplitting
Linear problem
Added piecewise linear constraints
Initial assignment
Update NonBasic Variable
Cannot Update Basic Variable
Pivot
And the search goes on…
When we satisfy linear constraints …
Check piecewise linear constraints
When repeatedly broken
Split
Solution
Marabou
 Own simplex core replaces GLPK
 Networklevel reasoning  Symbolic bound tightening
 Parallel Divide & Conquer algorithm
Architecture overview
Search

Simplex  finds a satisfying assignment of linear constraints

SMT  manages splits of piecewise linear constraints
 Splitting and Backtracking
 Currently very simple

Bound tightening  propagates bounds through the network
 Forces ReLUs into a single case
Manging the state space size
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