Building Trust and Safety in Artificial Intelligence with Abstract Interpretation
summary
Abstract interpretation is used to certify and train DNNs so they generalize to infinite unseen inputs, with specific domains like DeepPoly and zonotopes and a relational verifier Raven for universal perturbations. A synthesized transformer approach yields up to 4x better precision than interval and 2.8x vs zonotope. Case studies: a VMware RL controller shows high-reward models are unstable by robustness/monotonicity scores; job-scheduling GNNs fail strategy‑proofness in multi‑step tests; a DSL cuts a 20k‑line analyzer to a few lines.
AI-written summary · about
chapters (16)
- 0:00Trustworthy AI with abstract interpretation
- 3:21Adversarial attacks and OOD challenges
- 6:52AI model development pipeline
- 9:03Testing neural networks with AI
- 12:44DNN vs program verification
- 17:36Abstract interpretation for self-driving data centers
- 20:35Verifying GNNs for job scheduling
- 23:21Strategy-proofness in GNN schedulers
- 26:16Verifying financial model gradients
- 30:32Relational verification of neural networks
- 33:26Incremental certification for verification
- 37:00DSL for abstract interpreters
- 41:18Training neural networks with differentiable abstract interpreters
- 43:46Robustness vs accuracy trade-offs
- 45:54Interpreting proofs for verified NNs
- 50:13Q&A
related talks
01h 30mTrustworthy AI & Open Source
56mAbstract Domains for Machine Learning Verification
14mAutomated Verification of Soundness of DNN Certifiers
19mAdversities in Abstract Interpretation - Accommodating Robustness by Abstract(…)
18mTaming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Tr...
20mVerifying Neural Networks with PyRAT
31mARENA: Enhancing Abstract Refinement for Neural Network Verification
15mAbstract Interpretation of Fixpoint Iterators with Applications to Neural Networks