From 324eddc16f935f024bfe387e359388931bccd509 Mon Sep 17 00:00:00 2001
From: Julien Girard <julien.girard2@cea.fr>
Date: Wed, 29 Nov 2023 11:44:33 +0100
Subject: [PATCH] [doc] MNIST example is actually working now
---
doc/mnist.rst | 12 ++++++------
examples/mnist/property.why | 6 +++---
2 files changed, 9 insertions(+), 9 deletions(-)
diff --git a/doc/mnist.rst b/doc/mnist.rst
index 6570d7d..38e0e98 100644
--- a/doc/mnist.rst
+++ b/doc/mnist.rst
@@ -92,7 +92,7 @@ to declare and define :math:`\epsilon`.
type label_ = int
We will first write some predicates to take into account the fact
-that we only have two available labels in the dataset sample (0, 1 and 2)
+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.).
We will also define a predicate that, given a label ``l`` and an image ``i``, checks whether the neural network ``nn`` indeed advises the correct label.
@@ -102,13 +102,13 @@ We will also define a predicate that, given a label ``l`` and an image ``i``, ch
predicate valid_image (i: image) =
forall v: index. valid_index i v -> (0.0: t) .<= i[v] .<= (1.0: t)
- predicate valid_label (l: label_) = 0 <= l <= 2
+ predicate valid_label (l: label_) = 0 <= l <= 9
predicate advises (n: nn) (i: image) (l: label_) =
valid_label l ->
forall j: int. valid_label j -> j <> l -> (n@@i)[l] .> (n@@i)[j]
-We write that :math:`\lVert x - x' \rVert_\infty \leq \epsilon` with another
+We write :math:`\lVert x - x' \rVert_\infty \leq \epsilon` with another
predicate:
.. code-block:: whyml
@@ -139,8 +139,8 @@ samples, we can define a goal and check the property
.. code-block:: whyml
goal robustness:
- let nn = read_neural_network "MNIST_256_2" ONNX in
- let dataset = read_dataset "mnist_test.csv" CSV in
+ let nn = read_neural_network "nets/MNIST_256_2.onnx" ONNX in
+ let dataset = read_dataset "csv/mnist_test.csv" CSV in
let eps = (0.375:t) in
robust nn dataset eps
@@ -161,7 +161,7 @@ done via CAISAR as follows:
.. code-block:: console
- $ caisar verify --prover nnenum -L examples/mnist/nets --format whyml examples/mnist/property.why
+ $ caisar verify --prover nnenum -L examples/mnist/ --format whyml examples/mnist/property.why
[caisar] Goal robustness: Invalid
The result tells us that there exists at least one image in ``mnist_test.csv``
diff --git a/examples/mnist/property.why b/examples/mnist/property.why
index 24cfa42..3a98618 100644
--- a/examples/mnist/property.why
+++ b/examples/mnist/property.why
@@ -11,7 +11,7 @@ theory MNIST
predicate valid_image (i: image) =
forall v: index. valid_index i v -> (0.0: t) .<= i[v] .<= (1.0: t)
- predicate valid_label (l: label_) = 0 <= l <= 2
+ predicate valid_label (l: label_) = 0 <= l <= 9
predicate advises (n: nn) (i: image) (l: label_) =
valid_label l ->
@@ -32,8 +32,8 @@ theory MNIST
Dataset.forall_ d (robust_around n eps)
goal robustness:
- let nn = read_neural_network "MNIST_256_2" ONNX in
- let dataset = read_dataset "mnist_test.csv" CSV in
+ let nn = read_neural_network "nets/MNIST_256_2.onnx" ONNX in
+ let dataset = read_dataset "csv/mnist_test.csv" CSV in
let eps = (0.375:t) in
robust nn dataset eps
end
--
GitLab