Machine Learning Verification - CS 8395 - Spring 2020¶

Vanderbilt University

Week 1 - Syllabus Overview¶

About the course, introduction to machine learning verification, challenges, intro to reading/reviewing papers.

Towards Verified AI - Seshia, Sadigh, Sastry - link
Formal Specification for Deep Neural Networks - Seshia et al - (https://link.springer.com/chapter/10.1007/978-3-030-01090-4_2)

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks - Katz et al - link
The Marabou Framework for Verification and Analysis of Deep Neural Networks - Katz et al - link

AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation Gehr et al - link
- Video: https://www.youtube.com/watch?v=LJnjCMV8KzA&list=PLZVw65tJnqIRDhCnnvk6Neh29-aeRYBB0&index=2&t=0s
ReLUVal - Formal security analysis of neural networks using symbolic intervals - Wang et al - link code
- Video: https://www.youtube.com/watch?v=jm_7SKOC-cA&list=PLZVw65tJnqIRDhCnnvk6Neh29-aeRYBB0&index=3&t=0s

Algorithms for Verifying Deep Neural Networks - Changliu Liu et al - link code
Video: https://www.youtube.com/watch?v=on17gZFUP9Y&list=PLZVw65tJnqIR2r5aHTrj_Ew-oJImV6MU5&t=180s
Note: this paper is quite long, so we will spend a couple weeks on it: week 5 through section 6, week 6 section 7 to end

End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Tasks link
Towards Responsibility-Sensitive Safety of Automated Vehicles with Reachable Set Analysis link

NNV: https://github.com/verivital/nnv and NNMT: https://github.com/verivital/nnmt
Reluplex: https://github.com/guykatzz/ReluplexCav2017
Marabou: https://github.com/NeuralNetworkVerification/Marabou
AI^2 / ERAN / DeepZ / DeepPoly / DeepG: https://github.com/eth-sri/eran and https://github.com/eth-sri/deepg
Reluval: https://github.com/tcwangshiqi-columbia/ReluVal
CNN-Cert: https://github.com/IBM/CNN-Cert
Sherlock: https://github.com/souradeep-111/sherlock
Verisig: https://github.com/Verisig/verisig
CROWN: https://github.com/IBM/CROWN-Robustness-Certification and https://github.com/huanzhang12/RecurJac-and-CROWN
PLANET: https://github.com/progirep/planet
DeepGO: https://github.com/trustAI/DeepGO
MIPVerify: https://github.com/vtjeng/MIPVerify.jl
Neurify: https://github.com/tcwangshiqi-columbia/Neurify
Syrenn: https://github.com/95616ARG/SyReNN
NSVerify: https://vas.doc.ic.ac.uk/software/neural/
DNNV: https://github.com/dlshriver/DNNV