Scalable and Modular Robustness Analysis of Deep Neural Networks
summary
BBPoly implements network block summarization on top of the DeepPoly abstract domain to speed robustness verification using only CPU. It segments networks (sigma layers per block), computes block summary and input summary, and uses a bounded back-substitution heuristic. On MNIST/CIFAR10 and residual nets up to ~1 million neurons, BBPoly yields comparable precision to DeepPoly but analyzes huge ResNets in about one hour per image (DeepPoly times out at 3h or needs ~40h), trading some precision for scalability.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:14Formal Methods for Network Analysis
- 0:50Contributions
- 1:30Outline
- 2:56Illustrative Example
- 3:34Recap: Deep Poly Analysis
- 4:57Back-substitution for tighter bound
- 6:12Key Insight: "Jump" By Summary
- 7:39Robustness Verified
- 8:07BBPoly Approach
- 10:41Evaluation
- 11:20Results on MNIST FCN and CNN
- 12:19Results on ResNets
- 13:33Key Takeaways
related talks
17mMini-Batch Robustness Verification of Deep Neural Networks
28mTowards the Universal Law of Robustness for Deep Neural Networks
50mLifting the Curtain on Machine Learning
15mReduced Products of Abstract Domains for Fairness Certification of Neural Networks
17mInput-Relational Verification of Deep Neural Networks
48mDynamic Neural Networks with DyNet
32mStructured Deep Learning with Probabilistic Neural Prog
20mIncremental Verification of Neural Networks