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.

Week 2 - High-Level Overview of Machine Learning Verification

• 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)

Week 3 - Satisfiability Approaches for Neural Network Verification

• 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

Week 4 - AI^2 and ReluVal

• 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

Weeks 5 and 6 - Survey of Neural Network Verification Methods

• 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

Week 7

• 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

Week 8 - Project Discussion

Resources

Related Courses / Tutorials

• Neural Network Verification - M. Pawan Kumar - VMCAI’19 Winter School (http://mpawankumar.info/tutorials/vmcai2019/)

Software and Tools

• 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

Events - Workshops, Symposia, Etc.

• (https://sites.google.com/view/vnn19/)
• (https://sites.google.com/view/vnn20/)
• https://www.dagstuhl.de/en/program/calendar/semhp/?semnr=18121