一句话：提出对偶数抽象域，可靠过近似 Clarke 雅可比，并实现 DeepJ 分析非光滑神经网络的 Lipschitz 鲁棒性与优化景观。
本文研究局部输入区域内 Lipschitz 连续但未必可微函数的 Clarke 雅可比界的静态分析。作者构建基于对偶数的抽象域，可靠过近似计算 Clarke 雅可比所需的一阶导数，并提出前向 dual interval 求值；形式化证明该求值能给出真实 Clarke 雅可比的、基于区间域的可靠过近似。该框架可处理比已有工作更广的函数类，特别是神经网络与 Lipschitz 但不可微扰动的任意复合。作者实现工具 DeepJ，并在多个深度神经网络和不可微输入扰动上评估，获得区间 Clarke 雅可比以分析全连接与卷积网络在旋转、对比度变化、雾霾及其复合扰动下的 Lipschitz 鲁棒性和局部优化景观，展示了通用性与可扩展性。
We present a novel abstraction for bounding the Clarke Jacobian of a Lipschitz continuous, but not necessarily differentiable function over a local input region. To do so, we leverage a novel abstract domain built upon dual numbers, adapted to soundly over-approximate all first derivatives needed to compute the Clarke Jacobian. We formally prove that our novel forward-mode dual interval evaluation produces a sound, interval domain-based over-approximation of the true Clarke Jacobian for a given input region. Due to the generality of our formalism, we can compute and analyze interval Clarke Jacobians for a broader class of functions than previous works supported – specifically, arbitrary compositions of neural networks with Lipschitz, but non-differentiable perturbations. We implement our technique in a tool called DeepJ and evaluate it on multiple deep neural networks and non-differentiable input perturbations to showcase both the generality and scalability of our analysis. Concretely, we can obtain interval Clarke Jacobians to analyze Lipschitz robustness and local optimization landscapes of both fully-connected and convolutional neural networks for rotational, contrast variation, and haze perturbations, as well as their compositions.
@article{paperbot1545,
title = {A dual number abstraction for static analysis of Clarke Jacobians},
author = {Jacob Laurel and Rem Yang and Gagandeep Singh and Sasa Misailovic},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498718}
}