4.2. (Local) Robustness of MNIST dataset¶

4.2.1. Use case presentation¶

MNIST is a dataset of handwritten digits normalized and centered to fit into grayscale images of \(28 \times 28\) pixels, along with the classification labels [LiDeng2012]. Although it is mostly irrelevant as dataset for benchmarking machine learning models for computer vision tasks, MNIST is still valuable for assessing robustness properties by means of formal method tools.

CAISAR provides in mnist_test.csv a fragment (\(100\) images) of the MNIST dataset under the examples/mnist/csv folder. Each line in this file represents an MNIST image: in particular, the first column represents the classification label, and the remaining \(784\) columns represent the greyscale value of the respective pixels, rescaled into \([0, 1]\).

4.2.2. Properties¶

Generally speaking, the property we are interested in verifying is the local robustness of a machine learning model on the elements of a set. More formally, let \(\mathcal{X}\) be an input set, (in our case a subset of \(\mathbb{R}^{28\times 28}\)), \(\mathcal{Y} \subset \mathbb{R}\) be an output set, and \(C : \mathcal{X} \mapsto \mathcal{Y}\) a classifier. For a given \(\epsilon \in \mathbb{R}\), a classifier is \(\epsilon\)-locally-robust if it classifies all elements of \(\mathcal{X}\) being at an \(l_\infty\)-distance of at most \(\epsilon \geq 0\) with the same label. A general formulation of this property is the following: \(\forall x,x' \in X. \ \lVert x - x' \rVert_\infty \leq \epsilon \Rightarrow C(x) = C(x')\).

Since we actually deal with a dataset of finite elements, we will instead verify a slightly different property: given a classifier \(C\), an element \(x \in X\), and some perturbation \(\epsilon \geq 0\), it must hold that \(\forall x'. \ \lVert x - x' \rVert_\infty \leq \epsilon \Rightarrow C(x) = C(x') = y\), where y is the expected dataset classification for x. Obviously, such a property must be verified for all elements of a dataset.

4.2.3. Modelling the problem using WhyML¶

As described for the example on Functional properties of ACAS Xu, we first need to write a specification file containing a WhyML theory to describe the verification problem. In principle, we need to formalize the local robustness property as well as the notions of classifier and dataset. The CAISAR standard library provides theories that defines those concepts. We will import the relevant theories with the use keyword. As described in The CAISAR modelling language, the Vector theory provides a vector type, a getter ([]) operation and a valid_index predicate that determines whether the get operation is within the range of the vector length. Model defines a type and an application function (@@). We will also need integers and floating point numbers to declare and define \(\epsilon\).

theory MNIST

  use ieee_float.Float64
  use caisar.types.Float64WithBounds as Feature
  use caisar.types.IntWithBounds as Label
  use caisar.model.Model
  
  use caisar.dataset.CSV
  use caisar.robust.ClassRobustCSV

  constant model_filename: string
  constant dataset_filename: string

We will first write some predicates to take into account the fact that MNIST counts 10 labels (integer from 0 to 9) in the dataset sample, and that the input images are normalized (floating point values between 0. and 1.).

  constant label_bounds: Label.bounds =
    Label.{ lower = 0; upper = 9 }
  
  constant feature_bounds: Feature.bounds =
    Feature.{ lower = (0.0:t); upper = (1.0:t) }

We will also define a predicate that, given a label l and an image i, checks whether the model m indeed advises the correct label.

  predicate advises (label_bounds: Label.bounds) (m: model t)
                     (l: Label.t) (e: FeatureVector.t) =
    Label.valid label_bounds l ->
    forall j. Label.valid label_bounds j -> j <> l ->
      (m @@ e)[l] .>= (m @@ e)[j]

We write \(\lVert x - x' \rVert_\infty \leq \epsilon\) with another predicate:

  predicate bounded_by_epsilon (e: FeatureVector.t) (eps: t) =
    forall i: index. valid_index e i -> .- eps .<= e[i] .<= eps

We can now define the property to check that is a straightforward description of property:

  predicate robust (feature_bounds: Feature.bounds)
                   (label_bounds: Label.bounds)
                   (m: model t) (eps: t)
                   (l: Label.t) (e: FeatureVector.t) =
    forall perturbed_e: FeatureVector.t.
      has_length perturbed_e (length e) ->
      FeatureVector.valid feature_bounds perturbed_e ->
      let perturbation = perturbed_e - e in
      bounded_by_epsilon perturbation eps ->
      advises label_bounds m l perturbed_e

Finally, to instantiate this property on concrete neural networks and data samples, we can define a goal and check the following property:

  goal robustness:
    let nn = read_model model_filename in
    let dataset = read_dataset dataset_filename in
    let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
    robust feature_bounds label_bounds nn dataset eps

The final property file (available at mnist.why) looks like this:

theory MNIST

  use ieee_float.Float64
  use caisar.types.Float64WithBounds as Feature
  use caisar.types.IntWithBounds as Label
  use caisar.model.Model
  
  use caisar.dataset.CSV
  use caisar.robust.ClassRobustCSV

  constant model_filename: string
  constant dataset_filename: string

  constant label_bounds: Label.bounds =
    Label.{ lower = 0; upper = 9 }
  
  constant feature_bounds: Feature.bounds =
    Feature.{ lower = (0.0:t); upper = (1.0:t) }

  goal robustness:
    let nn = read_model model_filename in
    let dataset = read_dataset dataset_filename in
    let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
    robust feature_bounds label_bounds nn dataset eps

end

In this file, the predicates were moved in the caisar dataset and robust theories, defined in CAISAR standard library.

4.2.4. Verifying the property with CAISAR¶

Neural network in ONNX format and part of the MNIST dataset are available under the folder /examples/mnist/.

We may verify whether the previous robustness specification holds by using the nnenum prover. This can be done via CAISAR as follows:

$ caisar verify -p nnenum \
    --define model_filename:nets/MNIST_256_2.onnx \
    --define dataset_filename:csv/mnist_test.csv \
    examples/mnist/mnist.why
(nnenum) MNIST.robustness: Invalid

The result tells us that there exists at least one image in mnist_test.csv for which nnenum is sure that the model MNIST_256_2.onnx is not robust with respect to \(1 \%\) perturbation. At the moment, CAISAR is not able to tell which are the images in the dataset that cause such result.