Input-Relational Verification of Deep Neural Networks
summary
A verifier that reasons about multiple executions builds a DiffPoly abstract domain to track concrete and symbolic difference bounds layer by layer, produces precise linear difference constraints between executions, and encodes the output check as an LP/MP solved with borobi inside the RaVeN verifier. RaVeN proves robustness to universal adversarial perturbations and local monotonicity more often than prior tools, scales to networks with millions of parameters (solver is the bottleneck), and later replaces the MP solver with a gradient solver for ~6× speed with minor precision loss.
AI-written summary · about
chapters (10)
- 0:00Relational verification intro
- 1:05Why verification is needed
- 2:11Limitations of verification
- 3:37UAP robustness properties
- 5:20Relational verification challenges
- 7:47DePoly abstract domain
- 10:20RAVEN verifier overview
- 12:51RAVEN evaluation results
- 13:55Follow-up work
- 14:35Conclusion and future
related talks
59mDifferential Verification of Deep Neural Networks
31mARENA: Enhancing Abstract Refinement for Neural Network Verification
55mTowards Verified Deep Learning
42mTowards Verification of General Neural Networks: A Dual Approach
16mVerification of Neural Networks' Global Robustness
20mIncremental Verification of Neural Networks
17mMini-Batch Robustness Verification of Deep Neural Networks
20mVerifying Neural Networks with PyRAT