Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
caisar
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Deploy
Releases
Package Registry
Container Registry
Model registry
Operate
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
caisar
Commits
67f51fa6
Commit
67f51fa6
authored
1 year ago
by
Michele Alberti
Committed by
Julien Girard-Satabin
1 year ago
Browse files
Options
Downloads
Patches
Plain Diff
[examples] Use original eps value for MNIST robustness.
parent
324eddc1
No related branches found
No related tags found
No related merge requests found
Changes
2
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
doc/mnist.rst
+1
-1
1 addition, 1 deletion
doc/mnist.rst
examples/mnist/property.why
+1
-1
1 addition, 1 deletion
examples/mnist/property.why
with
2 additions
and
2 deletions
doc/mnist.rst
+
1
−
1
View file @
67f51fa6
...
@@ -75,7 +75,7 @@ The CAISAR interpretation language `caisar.mlw
...
@@ -75,7 +75,7 @@ The CAISAR interpretation language `caisar.mlw
We will import the relevant theories with the ``use`` keyword.
We will import the relevant theories with the ``use`` keyword.
As described in :ref:`interpretation`, the ``Vector`` theory provides
As described in :ref:`interpretation`, the ``Vector`` theory provides
a vector type, a getter (``[]``) operation and a ``valid_index`` predicate
a vector type, a getter (``[]``) operation and a ``valid_index`` predicate
that determine whether the get operation is within the range of the vector length.
that determine
s
whether the get operation is within the range of the vector length.
``NeuralNetwork`` defines a type and an application function (``@@``).
``NeuralNetwork`` defines a type and an application function (``@@``).
We will also need integers and floating point numbers
We will also need integers and floating point numbers
to declare and define :math:`\epsilon`.
to declare and define :math:`\epsilon`.
...
...
This diff is collapsed.
Click to expand it.
examples/mnist/property.why
+
1
−
1
View file @
67f51fa6
...
@@ -34,6 +34,6 @@ theory MNIST
...
@@ -34,6 +34,6 @@ theory MNIST
goal robustness:
goal robustness:
let nn = read_neural_network "nets/MNIST_256_2.onnx" ONNX in
let nn = read_neural_network "nets/MNIST_256_2.onnx" ONNX in
let dataset = read_dataset "csv/mnist_test.csv" CSV in
let dataset = read_dataset "csv/mnist_test.csv" CSV in
let eps = (0.
375
:t) in
let eps = (0.
0100000000000000002081668171172168513294309377670288085937500000
:t) in
robust nn dataset eps
robust nn dataset eps
end
end
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment