[doc] Some proofreading.

d74580e8 · Michele Alberti · Julien Girard-Satabin · 38f717b7 · d74580e8 · d74580e8
Commit d74580e8 authored 1 year ago by Michele Alberti Committed by Julien Girard-Satabin 1 year ago
--- a/doc/acas_xu.rst
+++ b/doc/acas_xu.rst
 .. _acas_xu:

 Functional properties of ACAS-Xu
-******************************** 
+********************************

 ACAS-Xu stands for Aircraft Collision Avoidance System. Introduced for instance
 in [Manfredi2016]_, it is a specification of a program which aim to output
@@ -129,11 +129,9 @@ and the relevant arithmetic operations according to the IEEE 754 floating-point
 standard in a theory, astutely called ``ieee_float``. Specifically, we will
 import the ``Float64`` sub-theory, that defines everything we need for 64-bit
 precision floating-point numbers. We thus import it in our theory using the
-``use`` keyword.
-This currently requires to write exact IEEE 754 floating
-point values in the specification file, which is
-understandably a setback in terms of usability, but have the
-advantage of being unambiguous on the specification.
+``use`` keyword. This currently requires to write exact IEEE 754 floating point
+values in the specification file, which is understandably a setback in terms of
+usability, but have the advantage of making the specification unambiguous.

 Our file looks like this so far:

@@ -148,12 +146,20 @@ CAISAR provide WhyML extensions to recognize and apply
 neural networks in ONNX and NNet formats on vector inputs.
 Given a file of such formats, CAISAR is able to provide the following:

-* a logical symbol of type ``nn``, built using the ``read_neural_network`` function, of type ``string -> format -> nn``. The first argument is the path to the neural network file, ``format`` is either ``ONNX`` or ``NNet``, and ``nn`` is the type of the neural network in WhyML;
-* a function symbol that returns the output of the application of the neural network to a given input;
+* a logical symbol of type ``nn``, built using the ``read_neural_network``
+  function, of type ``string -> format -> nn``. The first argument is the path
+  to the neural network file, ``format`` is either ``ONNX`` or ``NNet``, and
+  ``nn`` is the type of the neural network in WhyML;
+* a function symbol that returns the output of the application of the neural
+  network to a given input;
 * types and predicates to manipulate inputs vectors;

 The full reference for those WhyML extensions is available under the
-`stdlib/interpretation.mlw <https://git.frama-c.com/pub/caisar/-/blob/master/stdlib/interpretation.mlw>`_ file. To create a logical symbol for a neural network located in "nets/onnx/ACASXU_1_1.onnx", we can import the relevant theories in our file and use the ``read_neural_network`` function symbol like this:
+`stdlib/interpretation.mlw
+<https://git.frama-c.com/pub/caisar/-/blob/master/stdlib/interpretation.mlw>`_
+file. To create a logical symbol for a neural network located in
+``nets/onnx/ACASXU_1_1.onnx``, we can import the relevant theories in our file and
+use the ``read_neural_network`` function symbol like this:

 .. code-block:: whyml

@@ -166,14 +172,13 @@ The full reference for those WhyML extensions is available under the
   end

 Now is the time to define our verification goal, that will call ``P1_1_1`` for
-property :math:`\phi_1` on neural network :math:`N_{1,1}`.
-We first need to model the inputs of the neural network
-:math:`\rho, \theta, \psi, v_{own}, v_{int}` to the range of floating-point
-values each may take. We can do that by writing a predicate that encode those specification constraints.
-Since neural networks take vectors as inputs, we use the
-WhyML extension ``interpretation.Vector``.
-Since we manipulate integer indexes, we require the use of the ``int.Int`` Why3 library.
-
+property :math:`\phi_1` on neural network :math:`N_{1,1}`. We first need to
+model the inputs of the neural network :math:`\rho, \theta, \psi, v_{own},
+v_{int}` to the range of floating-point values each may take. We can do that by
+writing a predicate that encode those specification constraints. Since neural
+networks take vectors as inputs, we use the CAISAR library
+``interpretation.Vector``. Similarly, as we need to manipulate integer indexes,
+we require the use of the ``int.Int`` Why3 library.

 We can write this as a predicate for clarity:

@@ -196,27 +201,28 @@ We can write this as a predicate for clarity:
  end

 .. warning ::
-  You'll notice that the input value in the example are
-  different than what the specification states.
-  Recall that
-  :math:`1500 \leq \rho \leq 1800`, and :math:`-0.06 \leq \theta \leq 0.06`.
-  Training networks on such wide variation range leads to
-  instability, hence we need to normalize the inputs.
-  For this specific benchmark, we refer to the values the
-  original authors provide in their
-  `repository <https://github.com/NeuralNetworkVerification/Marabou/tree/master/resources/properties>`_.
-
-  Future release of CAISAR will provide built-in normalization functions to bridge the gap between
-  requirements and the actual computations.
+  You will notice that the input values in the example are different than what
+  the original property states. Recall that :math:`1500 \leq \rho \leq 1800`,
+  and :math:`-0.06 \leq \theta \leq 0.06`. Training networks on such wide
+  variation range leads to instability, hence the need to normalize the inputs.
+  For this specific benchmark, we refer to the IEEE 754 floating-point
+  representation of the normalized values the original authors provide in their
+  `repository
+  <https://github.com/NeuralNetworkVerification/Marabou/tree/master/resources/properties>`_.
+
+  A future release of CAISAR will provide a way for specifying and perform such
+  a normalization process in order to bridge the gap between the original
+  properties and the actual specifications.

 We must then define the result of the application of ``nn_1_1`` on the inputs.
-The built-in function ``@@`` serves this purpose. Its type, ``nn -> vector 'a -> vector 'a``, describes what it does: given a neural network ``nn`` and an input vector ``x``, return the vector that is the result of the application of ``nn`` on ``x``.
-Note that thanks to type polymorphism, ``@@`` can be used to
-describe a variety of input vectors, including floating points, integers, or strings.
-We can finally define the output constraint
-we want to enforce on the first coordinate of the output vector that we use to
-model the advisory *COC*. We use the WhyML extension
-predicate ``has_length`` to further check that our inputs
+The built-in function ``@@`` serves this purpose. Its type, ``nn -> vector 'a ->
+vector 'a``, describes what it does: given a neural network ``nn`` and an input
+vector ``x``, return the vector that is the result of the application of ``nn``
+on ``x``. Note that thanks to type polymorphism, ``@@`` can be used to describe
+a variety of input vectors, including floating points, integers, or strings. We
+can finally define the output constraint we want to enforce on the first
+coordinate of the output vector that we use to model the advisory *COC*. We use
+the WhyML extension predicate ``has_length`` to further check that our inputs
 are of valid length.

 The final WhyML file looks like this:
@@ -232,11 +238,11 @@ The final WhyML file looks like this:
    constant nn_1_1: nn = read_neural_network "nets/onnx/ACASXU_1_1.onnx" ONNX

    predicate valid_input (i: vector t) =
-    let rho = i[0] in
-    let theta = i[1] in
-    let psi = i[2] in
-    let vown = i[3] in
-    let vint = i[4] in
+      let rho = i[0] in
+      let theta = i[1] in
+      let psi = i[2] in
+      let vown = i[3] in
+      let vint = i[4] in
      (0.5999999999999999777955395074968691915273666381835937500000000000:t) .<= rho .<= (0.6798577687000000313588543576770462095737457275390625000000000000:t)
      /\ (-0.5:t) .<= theta .<= (0.5:t)
      /\ (-0.5:t) .<= psi .<= (0.5:t)
@@ -246,7 +252,7 @@ The final WhyML file looks like this:
 
    goal P1_1_1:
      forall i: vector t. has_length i 5 -> valid_input i ->
-      let coc = (nn_1_1@@i)[0] in
+        let coc = (nn_1_1@@i)[0] in
        coc .<= (3.9911256458999999630066213285317644476890563964843750000000000000:t)
  end

@@ -306,7 +312,7 @@ From the modelling standpoint, the main evident difference concerns the desired
 output property, meaining that *COC* should not be the minimal value. A
 straightforward way to express this property is that the neural network
 output is greater than or equal to at least one of
-the other five outputs. We can write a ``is_min`` predicate
+the other four outputs. We can write a ``is_min`` predicate
 that, for a vector ``o`` and int ``i``, states whether the
 :math:`i`-th coordinate of ``o`` is the minimal value:

@@ -339,11 +345,11 @@ In the end, the WhyML file looks like this:
    constant nn_2_7: nn = read_neural_network "nets/onnx/ACASXU_2_7.onnx" ONNX
  
    predicate valid_input (i: vector t) =
-    let rho = i[0] in
-    let theta = i[1] in
-    let psi = i[2] in
-    let vown = i[3] in
-    let vint = i[4] in
+      let rho = i[0] in
+      let theta = i[1] in
+      let psi = i[2] in
+      let vown = i[3] in
+      let vint = i[4] in
      (-0.3035311560999999769272506000561406835913658142089843750000000000:t) .<= rho .<= (-0.2985528118999999924731980627257144078612327575683593750000000000:t)
      /\ (-0.0095492965999999998572000947660853853449225425720214843750000000:t) .<= theta .<= (0.0095492965999999998572000947660853853449225425720214843750000000:t)
      /\ (0.4933803236000000036476365039561642333865165710449218750000000000:t) .<= psi .<= (0.5:t)
@@ -354,10 +360,16 @@ In the end, the WhyML file looks like this:
      forall j: int. 0 <= j < 5 -> i <> j -> o[i] .<= o[j]
  
    goal P3_1_1:
-      forall i: vector t. has_length i 5 -> valid_input i -> let is_coc_min = (is_min (nn_1_1@@i) 0) in  not is_coc_min
+      forall i: vector t.
+        has_length i 5 -> valid_input i ->
+        let is_coc_min = is_min (nn_1_1@@i) 0 in
+        not is_coc_min
  
    goal P3_2_7:
-      forall i: vector t. has_length i 5 -> valid_input i -> let is_coc_min = (is_min (nn_2_7@@i) 0) in  not is_coc_min
+      forall i: vector t.
+        has_length i 5 -> valid_input i ->
+        let is_coc_min = is_min (nn_2_7@@i) 0 in
+        not is_coc_min
  end



--- a/doc/mnist.rst
+++ b/doc/mnist.rst
@@ -42,25 +42,22 @@ 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. 
-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,
-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)
-= C(x')`. Obviously, such a property must be verified for all elements of a
+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, 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) = C(x')`. Obviously, such a property must be verified for all elements of a
 dataset.

 Modelling the problem using WhyML