From 67f51fa664fa64edba93128821a654cbc703c650 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 30 Nov 2023 16:08:23 +0000
Subject: [PATCH] [examples] Use original eps value for MNIST robustness.
---
doc/mnist.rst | 2 +-
examples/mnist/property.why | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/doc/mnist.rst b/doc/mnist.rst
index 38e0e98..a703f02 100644
--- a/doc/mnist.rst
+++ b/doc/mnist.rst
@@ -75,7 +75,7 @@ The CAISAR interpretation language `caisar.mlw
We will import the relevant theories with the ``use`` keyword.
As described in :ref:`interpretation`, the ``Vector`` theory provides
a vector type, a getter (``[]``) operation and a ``valid_index`` predicate
-that determine whether the get operation is within the range of the vector length.
+that determines whether the get operation is within the range of the vector length.
``NeuralNetwork`` defines a type and an application function (``@@``).
We will also need integers and floating point numbers
to declare and define :math:`\epsilon`.
diff --git a/examples/mnist/property.why b/examples/mnist/property.why
index 3a98618..da1190c 100644
--- a/examples/mnist/property.why
+++ b/examples/mnist/property.why
@@ -34,6 +34,6 @@ theory MNIST
goal robustness:
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
+ let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
robust nn dataset eps
end
--
GitLab