Formal Verification of CNN-based Perception Systems

TL;DR

This paper presents a novel method for verifying the local robustness of CNN-based perception systems against affine and photometric transformations, using reachability analysis and MILP encodings, demonstrated on MNIST.

Contribution

It introduces a new notion of local robustness for CNNs that captures transformations not addressed by prior robustness definitions.

Findings

The method effectively verifies CNN robustness against specific transformations.

Implementation on MNIST shows practical applicability of the approach.

The approach outperforms previous methods in capturing transformation-based robustness.

Abstract

We address the problem of verifying neural-based perception systems implemented by convolutional neural networks. We define a notion of local robustness based on affine and photometric transformations. We show the notion cannot be captured by previously employed notions of robustness. The method proposed is based on reachability analysis for feed-forward neural networks and relies on MILP encodings of both the CNNs and transformations under question. We present an implementation and discuss the experimental results obtained for a CNN trained from the MNIST data set.