Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks
OPEN ACCESS
Loading...
Author / Producer
Date
2023-06
Publication Type
Journal Article
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
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).
Permanent link
Publication status
published
External links
Editor
Book title
Journal / series
Volume
7 (PLDI)
Pages / Article No.
138
Publisher
Association for Computing Machinery
Event
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
fixpoint; abstract interpretation; equlibrium models; adversarial robustness
Organisational unit
03948 - Vechev, Martin / Vechev, Martin