Formal Verification of CNN-based Perception Systems

Reference. Formal Verification of CNN-based Perception Systems

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.

Cite

Cite as @kouvarosFormalVerificationCNNbased2018 (helia, typst) · \cite{kouvarosFormalVerificationCNNbased2018} (LaTeX)

BibTeX

bibtex · 15 lines

@article{kouvarosFormalVerificationCNNbased2018,
 title = {Formal {{Verification}} of {{CNN-based Perception Systems}}},
 author = {Kouvaros, Panagiotis and Lomuscio, Alessio},
 date = {2018-11-28},
 doi = {10.48550/arXiv.1811.11373},
 url = {http://arxiv.org/abs/1811.11373},
 urldate = {2025-02-19},
 keywords = {Computer Science - Computer Vision and Pattern Recognition,Computer Science - Machine Learning,Statistics - Machine Learning},
 pubstate = {prepublished},
 langid = {english},
 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.},
 eprintclass = {cs},
 eprinttype = {arXiv},
 eprint = {1811.11373}
}

hayagriva YAML (typst)

yaml · 17 lines

kouvarosFormalVerificationCNNbased2018:
  type: article
  title: Formal {Verification} of {CNN-based Perception Systems}
  author:
  - Kouvaros, Panagiotis
  - Lomuscio, Alessio
  date: 2018-11-28
  url:
    value: http://arxiv.org/abs/1811.11373
    date: 2025-02-19
  serial-number:
    arxiv: '1811.11373'
    doi: 10.48550/arXiv.1811.11373
  language: en-US
  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.
  parent:
    type: periodical

Download: kouvarosFormalVerificationCNNbased2018.bib · kouvarosFormalVerificationCNNbased2018.yml

Cited by (1)

Verification of Deep Convolutional Neural Networks Using ImageStars tranVerificationDeepConvolutional2020CAV · 2020

Convolutional Neural Networks (CNN) have redefined stateof-the-art in many real-world applications, such as facial recognition, image classification, human pose estimation, and semantic segmentation. Despite their success, CNNs are vulnerable to adversarial attacks, where slight changes to their inputs may lead to sharp changes in their output in even well-trained networks. Set-based analysis methods can detect or prove the absence of bounded adversarial attacks, which can then be used to evaluate the effectiveness of neural network training methodology. Unfortunately, existing verification approaches have limited scalability in terms of the size of networks that can be analyzed.

PDF · DOI · arXiv · pldb

Cites 20 works (0 here)

External (20)

AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation (2018)
Verifying Properties of Binarized Deep Neural Networks (2018)
Reachability Analysis for Neural Agent-Environment Systems (2018)
A Dual Approach to Scalable Verification of Deep Networks (2018)
Venus; supplementary material (Anonymous) (2018)
Formal specification for deep neural networks (Seshia et al., UC Berkeley tech report) (2018)
Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017)
An approach to reachability analysis for feed-forward ReLU neural networks (2017)
Towards Practical Verification of Machine Learning: The Case of Computer Vision Systems (2017)
Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks (2017)
Safety Verification of Deep Neural Networks (2017)
The Limitations of Deep Learning in Adversarial Settings (2016)
Deep Learning (Goodfellow, Bengio, Courville) (2016)
Gurobi optimizer reference manual (2016)
ImageNet Large Scale Visual Recognition Challenge (2015)
Image Processing, Analysis, and Machine Vision (2014)
Explaining and Harnessing Adversarial Examples (2014)
Pattern Recognition and Machine Learning (Bishop) (2006)
Multiple View Geometry in Computer Vision (2004)
Gradient-based learning applied to document recognition (1998)