Formal Verification of CNN-based Perception Systems

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.

References in corpus (4)

• Explaining and Harnessing Adversarial Examples
• An approach to reachability analysis for feed-forward ReLU neural networks
• A Dual Approach to Scalable Verification of Deep Networks
• Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems

Cited by in corpus (6)

• Formal Verification of Input-Output Mappings of Tree Ensembles
• Provable Certificates for Adversarial Examples: Fitting a Ball in the Union of Polytopes
• Reachability Analysis for Feed-Forward Neural Networks using Face Lattices
• Reachability Analysis of Convolutional Neural Networks
• Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool
• Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach