Verifying Feedforward Neural Networks for Classification in Isabelle/HOL

By Achim D. Brucker and Amy Stell.

Neural networks are being used successfully to solve classification problems, e.g., for detecting objects in images. It is well known that neural networks are susceptible if small changes applied to their input result in misclassification. Situations in which such a slight input change, often hardly noticeable by a human expert, results in a misclassification are called adversarial attacks. Such attacks can be life-threatening if, for example, they occur in image classification systems used in autonomous cars or medical diagnosis. Systems employing neural networks, e.g., for safety or security critical functionality, are a particular challenge for formal verification, which usually expects a program (e.g., given as source code in a programming language). Such a program does, per se, not exist for neural networks. In this paper, we address this challenge by presenting a formal embedding of feedforward neural networks into Isabelle/HOL, together with a discussion of properties that are desirable for neural networks in critical applications. Our Isabelle-based prototype can import neural networks trained in TensorFlow, and we demonstrate our approach using a neural network trained for the classification of digits.

Keywords:
Neural network, Deep Learning, Classification Network, Feedforward Network, Verification, Isabelle/HOL

Supplementary material:
[  Formalization  ]

Please cite this work as follows:
A. D. Brucker and A. Stell, “Verifying feedforward neural networks for classification in Isabelle/HOL,” in Formal methods (FM 2023), M. Chechik, J.-P. Katoen, and M. Leucker, Eds. Heidelberg: Springer-Verlag, 2023. doi: 10.1007/978-3-031-27481-7_24. Author copy: https://logicalhacking.com/publications/brucker.ea-feedforward-nn-verification-2023/

BibTeX
@InCollection{ brucker.ea:feedforward-nn-verification:2023,
  abstract        = {Neural networks are being used successfully to solve
                     classification problems, e.g., for detecting objects in
                     images. It is well known that neural networks are susceptible
                     if small changes applied to their input result in
                     misclassification. Situations in which such a slight input
                     change, often hardly noticeable by a human expert, results in
                     a misclassification are called adversarial attacks. Such
                     attacks can be life-threatening if, for example, they occur in
                     image classification systems used in autonomous cars or
                     medical diagnosis. Systems employing neural networks, e.g.,
                     for safety or security critical functionality, are a
                     particular challenge for formal verification, which usually
                     expects a program (e.g., given as source code in a programming
                     language). Such a program does, per se, not exist for neural
                     networks. In this paper, we address this challenge by
                     presenting a formal embedding of feedforward neural networks
                     into Isabelle/HOL, together with a discussion of properties
                     that are desirable for neural networks in critical
                     applications. Our Isabelle-based prototype can import neural
                     networks trained in TensorFlow, and we demonstrate our
                     approach using a neural network trained for the classification
                     of digits.},
  keywords        = {Neural network, Deep Learning, Classification Network,
                     Feedforward Network, Verification, {Isabelle/HOL}},
  location        = {L{\"u}beck, Germany},
  author          = {Achim D. Brucker and Amy Stell},
  booktitle       = {Formal Methods (FM 2023)},
  language        = {english},
  doi             = {10.1007/978-3-031-27481-7_24},
  publisher       = {Springer-Verlag },
  address         = {Heidelberg },
  series          = {Lecture Notes in Computer Science },
  number          = {14000},
  editor          = {Marsha Chechik and Joost-Pieter Katoen and Martin Leucker},
  title           = {Verifying Feedforward Neural Networks for Classification in
                     {Isabelle/HOL}},
  areas           = {formal methods, software engineering},
  year            = {2023},
  isbn            = {978-3-642-38915-3},
  supplabel01     = {Formalization},
  supplementary01 = {https://doi.org/10.5281/zenodo.7418170},
  note            = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-feedforward-nn-verification-2023/}},
  pdf             = {https://logicalhacking.com/publications/brucker.ea-feedforward-nn-verification-2023/brucker.ea-feedforward-nn-verification-2023.pdf},
}