Toward Certified Robustness Against Real-World Distribution Shifts

TL;DR

This paper introduces a neural-symbolic verification framework that certifies neural network robustness against real-world distribution shifts by learning perturbations and refining sigmoid approximations, demonstrating superior performance on MNIST and CIFAR-10.

Contribution

It proposes a novel neural-symbolic verification method with a meta-algorithm for tight sigmoid approximation, bridging the gap between specifications and deployment settings.

Findings

Outperforms existing methods on MNIST and CIFAR-10 distribution shifts

Effectively handles sigmoid activation approximation challenges

Provides a scalable approach for real-world robustness certification

Abstract

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.