From 4967a7c3cfb8a6d55247664d18f3f398c39dec5e Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Thu, 19 Jan 2023 16:31:44 +0100
Subject: [PATCH] [doc] Update documentation.
---
doc/mnist.rst | 17 ++++++-----------
1 file changed, 6 insertions(+), 11 deletions(-)
diff --git a/doc/mnist.rst b/doc/mnist.rst
index 6e08ace..e99cbd4 100644
--- a/doc/mnist.rst
+++ b/doc/mnist.rst
@@ -4,10 +4,11 @@
***********************************
CAISAR provides a convenient way for verifying (local) robustness properties of
-neural networks on datasets, for classification problems only, in a specific
-``CSV`` format. In particular, each of the ``CSV`` lines is interpreted as
+neural networks working on datasets with values in :math:`[0, 1]`, for
+classification problems only. For the moment, CAISAR supports datasets in a
+specific ``CSV`` format only, where each ``CSV`` lines is interpreted as
providing the classification label in the first column, and the dataset element
-features in the other columns.
+features in the remaining columns.
We recall that a neural network is deemed robust on a dataset element whenever
it classify with a same label all other elements being at an
@@ -35,7 +36,7 @@ a fragment (:math:`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 :math:`784` columns represent the greyscale value of the respective
-pixels.
+pixels, rescaled into :math:`[0, 1]`.
Properties
----------
@@ -121,15 +122,9 @@ dataset, with each element's feature pertubed by :math:`1 \%`, looks like this:
use caisar.DatasetClassificationProps
goal robustness:
- let normalized_dataset = min_max_scale true (0.0:t) (1.0:t) dataset in
- robust model normalized_dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
+ robust model dataset (0.0100000000000000002081668171172168513294309377670288085937500000:t)
end
-Note the presence of the ``min_max_scale`` function defined in
-``DatasetClassification`` for normalizing all feature values in :math:`[0,1]`.
-Besides classic *Min-Max scaling*, CAISAR also provides ``z_norm`` function for
-*Z-normalization*.
-
This file is available, as is, under the ``/examples/mnist/`` folder as
`property.why
<https://git.frama-c.com/pub/caisar/-/blob/master/examples/mnist/property.why>`_.
--
GitLab