Incremental Verification of Neural Networks
summary
Complete, verifier-agnostic method IVAN reuses branch-and-bound work by saving a specification tree of partitioned subproblems and then avoids costly analyzer calls for unchanged subproblems, combines this with an augmented branching heuristic HΔ that prioritizes strategies that worked before, and applies a pruning pass to merge the benefits of reuse and reorder. Empirical claim: geometric mean speedups 2.4x on MNIST/CIFAR10, 3.8x on ACAS‑XU, up to 9.5x (and 43x on some hard properties), evaluated for weight updates including quantization and perturbations.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:38Neural networks need verification
- 2:23Reusing verification proofs
- 5:17Incremental verification challenges
- 7:24Faster verification technique
- 8:48Reorder with branching heuristics
- 11:16Main algorithm and prune tree
- 11:59Evaluation setup and baselines
- 13:43Speed-up results
- 15:08Summary
- 15:50Q&A
related talks
42mTowards Verification of General Neural Networks: A Dual Approach
16mVerification of Neural Networks' Global Robustness
11mExploiting Verified Neural Networks via Floating Point Numerical Error
17mInput-Relational Verification of Deep Neural Networks
17mMini-Batch Robustness Verification of Deep Neural Networks
55mTowards Verified Deep Learning
31mARENA: Enhancing Abstract Refinement for Neural Network Verification
27mProof Minimization in Neural Network Verification