Automated Verification of Soundness of DNN Certifiers
summary
Automates soundness checks for abstract-interpretation DNN certifiers by encoding certifier specs in the ConstraintFlow DSL, translating networks to a symbolic DNN representation, and discharging the resulting forall properties to SMT solvers. Handles interval/DeepPoly-style domains and arbitrary architectures, verifies most existing transformers in 1–2 seconds, and emits executable certifiers via a CPU compiler; code and artifacts are available at the project GitHub/Zenodo links.
AI-written summary · about
chapters (6)
- 0:00Introduction
- 1:06Certifier soundness limits
- 3:34Certifier development challenges
- 7:02Formal verification of soundness
- 11:56Results and future directions
- 13:19Q&A
related talks
58mBuilding Trust and Safety in Artificial Intelligence with Abstract Interpretation
26mTowards a Certified Proof Checker for Deep Neural Network Verification
55mTowards Verified Deep Learning
59mWhats and Whys of Neural Network Verification (A Declarative Programming Perspec...
59mVerification and Machine Learning
20mVerifying Neural Networks with PyRAT
25mProof transfer for fast certification of multiple approximate neural networks
27mProof Minimization in Neural Network Verification