Proof transfer for fast certification of multiple approximate neural networks
summary
FANC generates templates—connected symbolic shapes at an intermediate layer—and a cheap template transformer that adapts those templates to approximate networks (quantization, pruning, fine tuning) so an existing abstract-interpretation verifier (evaluated with DeepZ) can short-circuit layerwise propagation. Claims no precision loss vs. the baseline, measures up to 4.1x speedup across convolutional and fully connected models against adversarial patches, L0, rotation and brightening, and reports roughly 100 seconds per property per network.
AI-written summary · about
chapters (7)
- 0:00Incremental verification intro
- 3:13Proof reuse for modified networks
- 8:12Network modifications and distance
- 11:26Template-based incremental verification
- 15:40Incremental verifier workflow
- 20:51Experimental speed-up results
- 22:36Q&A
related talks
20mIncremental Verification of Neural Networks
42mTowards Verification of General Neural Networks: A Dual Approach
51mTips & Tricks for Fast Neural Net Inference in Production
14mAutomated Verification of Soundness of DNN Certifiers
23mPRIMA: General and Precise Neural Network Certification via Scalable Convex Hull
08mVerifying Low-dimensional Input Neural Networks via Input Quantization
44mFast Neural Networks… a no brainer!
20mVerifying Neural Networks with PyRAT