Exploiting Verified Neural Networks via Floating Point Numerical Error
summary
A verification gap lets machine-precision disagree with the verifier: using MIPVerify on CIFAR10 and MNIST with a 2/255 bound the authors programmatically brighten an image to a quasi-safe point, search for a nearest quasi-adversary, then apply random floating-point perturbations against five convolution implementations (CPU/GPU, matrix/direct/ Winograd) and reliably produce inputs that violate the claimed robustness. They also synthesize weights that force ReLU-active merges to hide counterexamples from incomplete verifiers; verification often times out near decision boundaries, causing aborts.
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:41Neural Network Verification
- 1:44Verification of Real-valued Networks
- 2:52Considered Implementations
- 3:13Floating-point Error Characteristics
- 3:52Exploiting Floating Point Error
- 6:25How About Incomplete Verifiers?
- 9:13Conclusion & Discussion
related talks
42mTowards Verification of General Neural Networks: A Dual Approach
16mVerification of Neural Networks' Global Robustness
20mIncremental Verification of Neural Networks
17mVerification of Bit-Flip Attacks against Quantized Neural Networks
59mVerification and Machine Learning
15mSMT-Based Modeling and Verification of Spiking Neural Networks: A Case Study
17mInput-Relational Verification of Deep Neural Networks
26mTowards a Certified Proof Checker for Deep Neural Network Verification