Mini-Batch Robustness Verification of Deep Neural Networks
summary
BaVerLy is a sound and complete verifier that jointly verifies mini-batches of ε-balls by encoding networks as MILP and grouping inputs with activation-pattern Hamming distance plus hierarchical clustering. It learns batch sizes with a multi-armed bandit and encodes the union of neighborhoods to avoid spurious counterexamples. Evaluated on MNIST and CIFAR-10 with fully connected and convolutional nets (up to ~7,000 neurons), it speeds up one-by-one verification by 2.3x average, up to 4.1x (example: 24 hours reduced to 6).
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:49Single-input verification problem
- 3:38Local robustness definition
- 5:44Group robustness problem
- 7:33Batch abstraction insights
- 8:35Dynamic batch learning
- 10:02Input clustering by activations
- 11:49BEAVERLY overview
- 12:32Experimental results
- 14:19Conclusion
- 14:42Q&A
related talks
16mVerification of Neural Networks' Global Robustness
20mIncremental Verification of Neural Networks
17mInput-Relational Verification of Deep Neural Networks
42mTowards Verification of General Neural Networks: A Dual Approach
14mScalable and Modular Robustness Analysis of Deep Neural Networks
27mProof Minimization in Neural Network Verification
11mExploiting Verified Neural Networks via Floating Point Numerical Error
55mTowards Verified Deep Learning