Towards Verified Deep Learning
summary
Argues that formal methods plus environment models let verification scale: replaces neural nets by an over-approximation (always wrong) and an under-approximation (perfect) to compute a region of uncertainty, projects that to a semantic input space, then runs adversarial search. Uses SqueezeDet, a 3D-SDN differentiable renderer, VBOT/GTA for images, the SCENIC probabilistic programming language to sample scenes and the Verify toolkit to find concrete counterexamples that cause missed detections and simulated collisions; retraining on those safety counterexamples raises detection metrics.
AI-written summary · about
chapters (19)
- 0:00Intro
- 1:25Context
- 3:33Formal Methods
- 10:00Context Matters
- 12:40Example
- 14:34Properties
- 16:10Robustness
- 16:40Local Robustness
- 21:15Semantic adversarial analysis
- 23:06Differentiable rendering
- 28:56Verification
- 32:25CPSML
- 35:10CPSML Example
- 42:22Retraining
- 44:30Scenic
- 46:20Deep Neural Networks
- 47:55Verified
- 51:35Conclusion
- 52:39Questions Directions
related talks
17mInput-Relational Verification of Deep Neural Networks
42mTowards Verification of General Neural Networks: A Dual Approach
24mTesting Techniques for Critical Deep Learning Applications
56mAbstract Domains for Machine Learning Verification
20mIncremental Verification of Neural Networks
59mWhats and Whys of Neural Network Verification (A Declarative Programming Perspec...
59mDifferential Verification of Deep Neural Networks
33mFormal Verification of Probabilistic Deep Reinforcement Learning Policies with(…)