Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Relational DNN Verification With Cross Executional Bound Refinement

Debangshu Banerjee, Gagandeep Singh

TL;DR

This work tackles relational verification of deep neural networks by jointly exploiting cross-execution dependencies. It introduces RACoon, a framework that uses cross executional bound refinement and a differentiable dual formulation of the LP relaxation to learn parametric activation bounds across multiple executions, improving precision over prior baselines. The method generalizes to arbitrary numbers of executions and conjunctions of linear outputs, and encodes the refined constraints into MILPs with scalable complexity. Experimental results on MNIST and CIFAR-10 demonstrate substantial gains in verifying k-UAP and worst-case Hamming properties, with practical runtimes on standard hardware, highlighting RACoon as a strong building block for more complete relational verifiers and extensions to broader relational scenarios.

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.

Relational DNN Verification With Cross Executional Bound Refinement

TL;DR

This work tackles relational verification of deep neural networks by jointly exploiting cross-execution dependencies. It introduces RACoon, a framework that uses cross executional bound refinement and a differentiable dual formulation of the LP relaxation to learn parametric activation bounds across multiple executions, improving precision over prior baselines. The method generalizes to arbitrary numbers of executions and conjunctions of linear outputs, and encodes the refined constraints into MILPs with scalable complexity. Experimental results on MNIST and CIFAR-10 demonstrate substantial gains in verifying k-UAP and worst-case Hamming properties, with practical runtimes on standard hardware, highlighting RACoon as a strong building block for more complete relational verifiers and extensions to broader relational scenarios.

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.
Paper Structure (33 sections, 16 theorems, 40 equations, 13 figures, 14 tables, 1 algorithm)

This paper contains 33 sections, 16 theorems, 40 equations, 13 figures, 14 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Works
  3. Preliminaries
  4. Cross Executional Bound Refinement
  5. RACoon Algorithm
  6. Experimental Evaluation
  7. Experiment setup
  8. Evaluating cross execution bound refinement
  9. Conclusion
  10. Impact and Ethics
  11. Formal encoding of relational properties
  12. k-UAP verification
  13. Worst case Hamming distance verification
  14. Theorectical guarantees for cross-execution bound refinement
  15. Theorectical guarantees for $n$ of executions
  16. ...and 18 more sections

Key Result

Theorem 4.1

$\vee_{i=1}^{2} (\mathbf{L_i}^{T} (\mathbf{x_i} + \pmb{\delta}) + b_i \geq 0)$ holds for all $\pmb{\delta} \in \mathbb{R}^{n_0}$ with $\|\pmb{\delta}\|_{\infty} \leq \epsilon$ if and only if $t^{*} \geq 0$.

Figures (13)

  • Figure 1: (a) MNIST (PGD)
  • Figure 2: (a) DiffAI (MNIST)
  • Figure 3: (a) ConvSmall (Standard)
  • Figure 4: (a) ConvSmall (Standard)
  • Figure 5: (a) ConvSmall (Standard)
  • ...and 8 more figures

Theorems & Definitions (30)

  • Theorem 4.1
  • Theorem 4.2
  • Lemma 2.1
  • proof
  • Theorem 2.2
  • proof
  • Theorem 2.3
  • proof
  • Lemma 2.4
  • proof
  • ...and 20 more