We consider the problem of certifying the robustness of deep neural networks
against real-world distribution shifts. To do so, we bridge the gap between
hand-crafted specifications and realistic deployment settings by proposing a
novel neural-symbolic verification framework, in which we train a generative
model to learn perturbations from data and define specifications with respect
to the output of the learned model. A unique challenge arising from this
setting is that existing verifiers cannot tightly approximate sigmoid
activations, which are fundamental to many state-of-the-art generative models.
To address this challenge, we propose a general meta-algorithm for handling
sigmoid activations which leverages classical notions of counter-example-guided
abstraction refinement. The key idea is to "lazily" refine the abstraction of
sigmoid functions to exclude spurious counter-examples found in the previous
abstraction, thus guaranteeing progress in the verification process while
keeping the state-space small. Experiments on the MNIST and CIFAR-10 datasets
show that our framework significantly outperforms existing methods on a range
of challenging distribution shifts.

本研究考虑了如何证明深度神经网络对真实世界的分布转化具有鲁棒性，提出了一种基于神经符号学的验证框架，并采用生成模型学习数据扰动，解决了现有验证方法对于许多最先进生成模型的 sigmoid 激活函数的处理问题，实验结果表明，该框架在 MNIST 和 CIFAR-10 数据集上能够显著优于现有方法，可以有效应对各种严峻的分布转化挑战。

面向实际分布偏移的认证鲁棒性

Toward Certified Robustness Against Real-World Distribution Shifts

Overwhelming theoretical and empirical evidence shows that mildly
overparametrized neural networks -- those with more connections than the size
of the training data -- are often able to memorize the training data with
$100\%$ accuracy. This was rigorously proved for networks with sigmoid
activation functions and, very recently, for ReLU activations. Addressing a
1988 open question of Baum, we prove that this phenomenon holds for general
multilayered perceptrons, i.e. neural networks with threshold activation
functions, or with any mix of threshold and ReLU activations. Our construction
is probabilistic and exploits sparsity.

本文探究神经网络模型，证明了具有 sigmoid 或 ReLU 激活函数的过度参数化的模型在训练数据超过一定数量后，具有百分之百的记忆能力。