Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks
summary
A new abstract-interpretation framework abstracts the concrete fixpoints of numerical fixpoint iterators and implements it in CRAFT, introducing the CH-Zonotope domain plus an error-consolidation step that restores properness after ReLU so containment checks stay cheap. The method proves sound, precise fixpoint abstractions without joins, supports efficient propagation over hundreds of iterations, and targets monDEQ; evaluation reports two orders of magnitude speedup, one order of magnitude better scalability and 25% higher certified accuracy (also up to 1000× faster and twice as many certified properties versus semi-SDP).
AI-written summary · about
chapters (14)
- 0:00Introduction
- 0:24Motivation for abstract interpretation
- 1:26Certifiably trustworthy AI
- 2:50MonDEQ and fixpoint iterators
- 3:52Challenges in abstracting iterators
- 4:54Unbounded loops with termination
- 5:57Fixpoint invariants for MonDEQ
- 7:42Requirements for abstract domain
- 8:24Zonotope and Box limitations
- 9:07CH-Zonotope domain
- 10:09Error consolidation for zonotopes
- 11:11Certification for MonDEQ
- 12:57Summary and applications
- 13:17Q&A
related talks
58mBuilding Trust and Safety in Artificial Intelligence with Abstract Interpretation
31mAbstract Neural Networks
11mAbstract Interpretation for Automatic Differentiation
19mInterval Universal Approximation for Neural Networks
14mEfficient Implementation of Neural Networks Usual Layers on Fixed-Point Architectures
19mAdversities in Abstract Interpretation - Accommodating Robustness by Abstract(…)
19mAbstract Neural Networks
31mARENA: Enhancing Abstract Refinement for Neural Network Verification