Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks
Not on the map. Why?
Abstract (arXiv)
We present a new abstract interpretation framework for the precise over-approximation of numerical fixpoint iterators. Our key observation is that unlike in standard abstract interpretation (AI), typically used to over-approximate all reachable program states, in this setting, one only needs to abstract the concrete fixpoints, i.e., the final program states. Our framework targets numerical fixpoint iterators with convergence and uniqueness guarantees in the concrete and is based on two major technical contributions: (i) theoretical insights which allow us to compute sound and precise fixpoint abstractions without using joins, and (ii) a new abstract domain, CH-Zonotope, which admits efficient propagation and inclusion checks while retaining high precision. We implement our framework in a tool called CRAFT and evaluate it on a novel fixpoint-based neural network architecture (monDEQ) that is particularly challenging to verify. Our extensive evaluation demonstrates that CRAFT exceeds the state-of-the-art performance in terms of speed (two orders of magnitude), scalability (one order of magnitude), and precision (25% higher certified accuracies).
Key facts. Cited by 1 paper in the map (data through 7 Oct 2026). Builds on 29 of its 76 references that are in the map. First posted on arXiv 14 Oct 2021.
Builds on
29 of 76 references.
References · 29
- 2019PyTorch: An Imperative Style, High-Performance Deep Learning Librarycited by 20,160
- 2014Explaining and Harnessing Adversarial Examplescited by 7,287
- 2017Towards Deep Learning Models Resistant to Adversarial Attackscited by 6,326
- 2013Intriguing properties of neural networkscited by 5,114
- 2019Certified Adversarial Robustness via Randomized Smoothingcited by 1,324
- 2019Deep Equilibrium Modelscited by 603
- 2017OptNet: Differentiable Optimization as a Layer in Neural Networkscited by 588
- 2017Provable defenses against adversarial examples via the convex outer adversarial polytopecited by 564
- 2018Certified Robustness to Adversarial Examples with Differential Privacycited by 462
- 2018Efficient Neural Network Robustness Certification with General Activation Functionscited by 439
- 2018On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Modelscited by 322
- 2018Towards Fast Computation of Certified Robustness for ReLU Networkscited by 254
17 more
- 2018Formal Security Analysis of Neural Networks using Symbolic Intervalscited by 185
- 2018Semidefinite relaxations for certifying robustness to adversarial examplescited by 178
- 2019SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solvercited by 173
- 2019Implicit Deep Learningcited by 124
- 2020Monotone operator equilibrium networkscited by 100
- 2021PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximationscited by 77
- 2021Stiff Neural Ordinary Differential Equationscited by 77
- 2020Lipschitz Bounded Equilibrium Networkscited by 49
- 2019An Alternative Surrogate Loss for PGD-based Adversarial Testingcited by 45
- 2020Faster Dynamic Matrix Inverse for Faster LPscited by 44
- 2020Scaling Polyhedral Neural Network Verification on GPUscited by 43
- 2019Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systemscited by 26
- 2021Semialgebraic Representation of Monotone Deep Equilibrium Models and Applications to Certificationcited by 16
- 2019Linear Encodings for Polytope Containment Problemscited by 6
- 2020Diversity can be Transferred: Output Diversification for White- and Black-box Attackscited by 4
- 2015Containment Problems for Projections of Polyhedra and Spectrahedracited by 2
- 2015Efficiently intertwining widening and narrowingcited by 1
Built on by
Citing papers per year: 2024: 1.
1 paper.