# Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks

arXiv: https://arxiv.org/abs/2110.08260 · HTML: https://mlsanity.com/paper/2110.08260/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 29 of its 76 references that are in the map.
- First posted on arXiv 14 Oct 2021.

## Builds on (most cited first, 29 of 29)

- [PyTorch: An Imperative Style, High-Performance Deep Learning Library](https://mlsanity.com/paper/1912.01703/) (2019)
- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Towards Deep Learning Models Resistant to Adversarial Attacks](https://mlsanity.com/paper/1706.06083/) (2017)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Certified Adversarial Robustness via Randomized Smoothing](https://mlsanity.com/paper/1902.02918/) (2019)
- [Deep Equilibrium Models](https://mlsanity.com/paper/1909.01377/) (2019)
- [OptNet: Differentiable Optimization as a Layer in Neural Networks](https://mlsanity.com/paper/1703.00443/) (2017)
- [Provable defenses against adversarial examples via the convex outer adversarial polytope](https://mlsanity.com/paper/1711.00851/) (2017)
- [Certified Robustness to Adversarial Examples with Differential Privacy](https://mlsanity.com/paper/1802.03471/) (2018)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [On the Effectiveness of Interval Bound Propagation for Training Verifiably Robust Models](https://mlsanity.com/paper/1810.12715/) (2018)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Semidefinite relaxations for certifying robustness to adversarial examples](https://mlsanity.com/paper/1811.01057/) (2018)
- [SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver](https://mlsanity.com/paper/1905.12149/) (2019)
- [Implicit Deep Learning](https://mlsanity.com/paper/1908.06315/) (2019)
- [Monotone operator equilibrium networks](https://mlsanity.com/paper/2006.08591/) (2020)
- [Stiff Neural Ordinary Differential Equations](https://mlsanity.com/paper/2103.15341/) (2021)
- [PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull Approximations](https://mlsanity.com/paper/2103.03638/) (2021)
- [Lipschitz Bounded Equilibrium Networks](https://mlsanity.com/paper/2010.01732/) (2020)
- [An Alternative Surrogate Loss for PGD-based Adversarial Testing](https://mlsanity.com/paper/1910.09338/) (2019)
- [Faster Dynamic Matrix Inverse for Faster LPs](https://mlsanity.com/paper/2004.07470/) (2020)
- [Scaling Polyhedral Neural Network Verification on GPUs](https://mlsanity.com/paper/2007.10868/) (2020)
- [Guaranteeing Safety for Neural Network-Based Aircraft Collision Avoidance Systems](https://mlsanity.com/paper/1912.07084/) (2019)
- [Semialgebraic Representation of Monotone Deep Equilibrium Models and Applications to Certification](https://mlsanity.com/paper/2106.01453/) (2021)
- [Linear Encodings for Polytope Containment Problems](https://mlsanity.com/paper/1903.05214/) (2019)
- [Diversity can be Transferred: Output Diversification for White- and Black-box Attacks](https://mlsanity.com/paper/2003.06878/) (2020)
- [Containment Problems for Projections of Polyhedra and Spectrahedra](https://mlsanity.com/paper/1509.02735/) (2015)
- [Efficiently intertwining widening and narrowing](https://mlsanity.com/paper/1503.00883/) (2015)

## Built on by (most cited first, 1 of 1)

- [Learning from Uncertain Data: From Possible Worlds to Possible Models](https://mlsanity.com/paper/2405.18549/) (2024)

## 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).