一句话：提出一种通用构造，可将高阶自动微分的抽象解释归约为对实值直线程序的抽象推理。
本文研究如何对高阶自动微分（AD）进行可证明可靠的抽象解释。作者提出一种通用构造，把关于导数的抽象推理归约为关于实值直线程序的抽象推理，因此可几乎与任意数值抽象域结合，包括关系型和非关系型域，并形式化证明了该构造的可靠性。实现上分别实例化非关系型区间域和关系型 zonotope 域，用于计算一阶与高阶导数；其中将关系型域用于高阶 AD 属首次，也首次在抽象解释中同时追踪不同变量以及不同导数阶之间的相关性。案例研究包括神经网络的鲁棒解释和 Lipschitz 常数计算。结果显示，zonotope AD 计算的一阶、二阶导数精度最高分别比区间 AD 提升 4.76 倍和 6.98 倍；在 Lipschitz 认证中，所得界比基于区间的当前最优工具最高精确 11,850 倍。
We present a novel, general construction to abstractly interpret higher-order automatic differentiation (AD). Our construction allows one to instantiate an abstract interpreter for computing derivatives up to a chosen order. Furthermore, since our construction reduces the problem of abstractly reasoning about derivatives to abstractly reasoning about real-valued straight-line programs, it can be instantiated with almost any numerical abstract domain, both relational and non-relational. We formally establish the soundness of this construction.We implement our technique by instantiating our construction with both the non-relational interval domain and the relational zonotope domain to compute both first and higher-order derivatives. In the latter case, we are the first to apply a relational domain to automatic differentiation for abstracting higher-order derivatives, and hence we are also the first abstract interpretation work to track correlations across not only different variables, but different orders of derivatives.We evaluate these instantiations on multiple case studies, namely robustly explaining a neural network and more precisely computing a neural network’s Lipschitz constant. For robust interpretation, first and second derivatives computed via zonotope AD are up to 4.76× and 6.98× more precise, respectively, compared to interval AD. For Lipschitz certification, we obtain bounds that are up to 11,850× more precise with zonotopes, compared to the state-of-the-art interval-based tool.
@article{paperbot1416,
title = {A general construction for abstract interpretation of higher-order automatic differentiation},
author = {Jacob Laurel and Rem Yang and Shubham Ugare and Robert Nagel and Gagandeep Singh and Sasa Misailovic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563324}
}