# Formal Verification of CNN-based Perception Systems

arXiv: https://arxiv.org/abs/1811.11373 · HTML: https://mlsanity.com/paper/1811.11373/

## Key facts

- Cited by 13 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 Nov 2018.

## Built on by (most cited first, 13 of 13)

- [Robust Machine Learning Systems: Challenges, Current Trends, Perspectives, and the Road Ahead](https://mlsanity.com/paper/2101.02559/) (2021)
- [An Abstraction-Refinement Approach to Verifying Convolutional Neural Networks](https://mlsanity.com/paper/2201.01978/) (2022)
- [Verification of Geometric Robustness of Neural Networks via Piecewise Linear Approximation and Lipschitz Optimisation](https://mlsanity.com/paper/2408.13140/) (2024)
- [Reachable Polyhedral Marching (RPM): An Exact Analysis Tool for Deep-Learned Control Systems](https://mlsanity.com/paper/2210.08339/) (2022)
- [Reachability Analysis of Convolutional Neural Networks](https://mlsanity.com/paper/2106.12074/) (2021)
- [A Neurosymbolic Approach to the Verification of Temporal Logic Properties of Learning enabled Control Systems](https://mlsanity.com/paper/2303.05394/) (2023)
- [Statistical Challenges with Dataset Construction: Why You Will Never Have Enough Images](https://mlsanity.com/paper/2408.11160/) (2024)
- [Verification of Neural Networks against Convolutional Perturbations via Parameterised Kernels](https://mlsanity.com/paper/2411.04594/) (2024)
- [Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool](https://mlsanity.com/paper/2207.06759/) (2022)
- [PCV: A Point Cloud-Based Network Verifier](https://mlsanity.com/paper/2301.11806/) (2023)
- [Formal Verification of Long Short-Term Memory based Audio Classifiers: A Star based Approach](https://mlsanity.com/paper/2311.12130/) (2023)
- [Lipschitz Optimization for Formal Verification of Homographies](https://mlsanity.com/paper/2605.23203/) (2026)
- [Certified Training for Convolutional Perturbations](https://mlsanity.com/paper/2607.18195/) (2026)

## Abstract (arXiv)

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.