Modeling and Verification of Sigma Delta Neural Networks using Satisfiability Modulo(…)
summary
Presents an SMT encoding of SDNNs that models rounding, delta and sigma operations, derives per-neuron interval bounds to prune the search, and encodes an adversarial robustness property for temporal inputs. Evaluates on a temporal MNIST benchmark with sequence lengths 4, 8, 16, 32 and three attack types (complete frame drop, partial-frame occlusion, partial-pixel perturbation). Finds interval bounds speedup—SMT with bounds scales better as sequence length grows—and reports all verification queries complete within about one hour on the reported examples.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:03Verifying neural networks
- 3:11Objective and contributions
- 5:37Sigma Delta Neural Networks
- 7:46Adversarial robustness in SDNs
- 9:14SMT encoding for SDN verification
- 12:31Temporal data processing
- 15:01Adversarial robustness formulation
- 16:50Experimental results
- 18:37Conclusion
- 19:20Q&A
related talks
15mSMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
16mVerification of Neural Networks' Global Robustness
59mVerification and Machine Learning
55mTowards Verified Deep Learning
20mIncremental Verification of Neural Networks
42mTowards Verification of General Neural Networks: A Dual Approach
14mAutomated Verification of Soundness of DNN Certifiers
11mExploiting Verified Neural Networks via Floating Point Numerical Error