[doc] Rephrased the local robustness property, removing ambiguity on the word expected

doc/mnist.rst

@@ -39,26 +39,32 @@ remaining :math:`784` columns represent the greyscale value of the respective
 pixels, rescaled into :math:`[0, 1]`.
 
 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. That is, the
-model classifies all elements of a set being at an :math:`l_\infty`-distance of
-at most :math:`\epsilon \geq 0` with a same label. A general formulation of this
-latter states that, given a classifier :math:`C`, a set :math:`X`, and some
-perturbation :math:`\epsilon \geq 0`, it must hold that :math:`\forall x,x'
+robustness of a machine learning model on the elements of a set. 
+More formally, let :math:`\mathcal{X}` be an input set,
+(in our case a subset of :math:`\mathbb{R}^{28\times 28}`),
+:math:`\mathcal{Y} \subset \mathbb{R}` be an output set; and 
+:math:`C : \mathcal{X} \mapsto \mathcal{Y}` a classifier.
+For a given :math:`\epsilon \in \mathbb{R}`,
+a classifier is :math:`\epsilon`-locally-robust if it
+classifies all elements of :math:`\mathcal{X}`
+being at an :math:`l_\infty`-distance of
+at most :math:`\epsilon \geq 0` with the same label.
+A general formulation of this property is the following: :math:`\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 for which we also
-know the expected labels, we will instead verify a slightly different property:
-given a classifier :math:`C`, an element :math:`x \in X` such that :math:`C(x) =
-y`, and some perturbation :math:`\epsilon \geq 0`, it must hold that
+Since we actually deal with a *dataset* of finite elements,
+we will instead verify a slightly different property:
+given a classifier :math:`C`, an element :math:`x \in X`,
+and some perturbation :math:`\epsilon \geq 0`, it must hold that
 :math:`\forall x'. \ \lVert x - x' \rVert_\infty \leq \epsilon \Rightarrow C(x)
-= y = C(x')`. Obviously, such a property must be verified for all elements of a
+= C(x')`. Obviously, such a property must be verified for all elements of a
 dataset.
 
 Modelling the problem using WhyML
----------------------------------
+=================================
 
 As described for the example on :ref:`acas_xu`, we first need to write a
 specification file containing a WhyML theory to describe the verification
@@ -133,7 +139,7 @@ The corresponding neural network in ONNX format is available under the
 <https://git.frama-c.com/pub/caisar/-/blob/master/examples/mnist/nets/MNIST_256_2.onnx>`_.
 
 Verifying the property with CAISAR
-----------------------------------
+==================================
 
 Now we may verify whether the previous robustness specification holds on the
 MNIST fragment ``mnist_test.csv`` by means of the nnenum prover. This can be
@@ -149,6 +155,9 @@ for which nnenum is sure that the model ``MNIST_256_2.onnx`` is not robust with
 respect to :math:`1 \%` perturbation. At the moment, CAISAR is not able to tell
 which are the images in the dataset that cause such result.
 
+References
+==========
+
 .. [LiDeng2012] Li Deng, *The MNIST Database of Handwritten Digit Images for
                Machine Learning Research*, IEEE Signal Process. Mag., 2012, pp.
                141-142, doi: 10.1109/MSP.2012.2211477