diff --git a/doc/mnist.rst b/doc/mnist.rst index 38e0e98a10aaefb6c30d5630020a1c88b6bab3b3..a703f0260b93aa84814a05e2eee7c8e85391f238 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 3a98618b79e94a702661efbe6dfe1650d3d0c77b..da1190ca4d67dd97e170b17140e7810df7840bfc 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