一句话：提出仅抽象具体不动点的抽象解释框架与 CH-Zonotope 抽象域，在神经网络验证中显著提升速度、可扩展性与精度。
标准抽象解释通常需过近似所有可达程序状态，而对于带收敛与唯一性保证的数值不动点迭代器，精确且可靠地过近似其不动点（最终状态）十分困难。本文提出仅抽象具体不动点的抽象解释框架：给出无需 join 即可计算可靠、精确不动点抽象的理论，并设计 CH-Zonotope 抽象域，支持高效传播与包含检查且保持高精度。该框架在工具 CRAFT 中实现，并于难验证的 monDEQ 不动点神经网络架构上评估，结果显示其速度提升两个数量级、可扩展性提升一个数量级、认证精度提高 25%。
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).
@article{paperbot1977,
title = {Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks},
author = {Mark Niklas Müller and Marc Fischer and Robin Staab and Martin Vechev},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591252}
}