Relational DNN Verification With Cross Executional Bound Refinement

TL;DR

This paper introduces RACoon, a scalable verifier for deep neural networks that leverages cross-execution dependencies across all layers to improve the precision of verifying relational properties like robustness and Hamming distance.

Contribution

The paper presents RACoon, a novel relational verifier that captures dependencies between multiple executions at all layers, significantly enhancing verification precision over existing methods.

Findings

RACoon outperforms state-of-the-art baselines in accuracy.

It is scalable across various datasets and network architectures.

Provides more precise verification of relational properties.

Abstract

We focus on verifying relational properties defined over deep neural networks (DNNs) such as robustness against universal adversarial perturbations (UAP), certified worst-case hamming distance for binary string classifications, etc. Precise verification of these properties requires reasoning about multiple executions of the same DNN. However, most of the existing works in DNN verification only handle properties defined over single executions and as a result, are imprecise for relational properties. Though few recent works for relational DNN verification, capture linear dependencies between the inputs of multiple executions, they do not leverage dependencies between the outputs of hidden layers producing imprecise results. We develop a scalable relational verifier RACoon that utilizes cross-execution dependencies at all layers of the DNN gaining substantial precision over SOTA baselines on a wide range of datasets, networks, and relational properties.