diff --git a/doc/mnist.rst b/doc/mnist.rst index 1e7fd36b1ae5430c76c46e9f6dc5d090cdaeced1..0b9b0b0e008d12aefbb44f2ec0d78ac0acdbffc2 100644 --- a/doc/mnist.rst +++ b/doc/mnist.rst @@ -165,6 +165,16 @@ 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. +For more flexibility, it is possible to define the concrete values from the +command line. See the ``--define`` option. For instane, to verify the aforementioned `mnist.why +<https://git.frama-c.com/pub/caisar/-/blob/master/examples/mnist/mnist.why>`_ +file, the command line is the following: + +.. code-block:: console + + $ caisar verify -p nnenum --define model_filename:nets/MNIST_256_2.onnx --define dataset_filename:csv/mnist_test.csv examples/mnist/mnist.why + [caisar] Goal robustness: Invalid + .. [LiDeng2012] Li Deng, *The MNIST Database of Handwritten Digit Images for Machine Learning Research*, IEEE Signal Process. Mag., 2012, pp.