diff --git a/doc/acas_xu.rst b/doc/acas_xu.rst
index cd183da9d3788655fe3fc6bf46ea73743e943909..eb58bc132fca57cf1275d1a6785cfb4818263f7d 100644
--- a/doc/acas_xu.rst
+++ b/doc/acas_xu.rst
@@ -1,7 +1,7 @@
.. _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
diff --git a/doc/mnist.rst b/doc/mnist.rst
index 96dcb523d5842eac7f51a682932f78f96ef8bb86..0d9c57ed8f243095ce2824df43691967c2fc6af3 100644
--- 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