[stdlib] Rework csv dataset robust predicate to consider all possible labels.

stdlib/dune

@@ -2,5 +2,5 @@
  (section
   (site
    (caisar stdlib)))
- (files caisar.mlw robustness.mlw vector.mlw nn.mlw dataset.mlw)
+ (files caisar.mlw robust.mlw vector.mlw nn.mlw dataset.mlw)
  (package caisar))

stdlib/robustness.mlw → stdlib/robust.mlw

@@ -43,22 +43,22 @@ theory RobustDatasetCSV
    predicate bounded_by_epsilon (e: elt) (eps: t) =
      forall v: index. valid_index e v -> .- eps .<= e[v] .<= eps
 
-   predicate robust_around (advises: elt -> label_ -> bool) (eps: t) (l: label_) (e: elt) =
+   predicate advises (valid_label: label_ -> bool)
+                     (nn: nn) (e: elt) (l: label_) =
+     valid_label l ->
+     forall j: int. valid_label j -> j <> l -> (nn @@ e)[l] .>= (nn @@ e)[j]
+
+   predicate robust_around (valid_label: label_ -> bool)
+                           (nn: nn) (eps: t) (l: label_) (e: elt) =
      forall perturbed_elt: elt.
        has_length perturbed_elt (length e) ->
        valid_elt perturbed_elt ->
        let perturbation = perturbed_elt - e in
        bounded_by_epsilon perturbation eps ->
-       advises perturbed_elt l
-
-  predicate advises (valid_label: label_ -> bool) (nn: nn) (e: elt) (l: label_) =
-     valid_label l ->
-     forall j: int. valid_label j -> j <> l -> (nn @@ e)[l] .>= (nn @@ e)[j]
+       advises valid_label nn perturbed_elt l
 
-   predicate robust (nn: nn) (d: dataset t) (eps: t) =
-     let min_label = DatasetCSV.min_label d in
-     let max_label = DatasetCSV.max_label d in
-     let advises = advises (valid_label min_label max_label) nn in
-     DatasetCSV.forall_ d (robust_around advises eps)
+   predicate robust (valid_label: label_ -> bool)
+                    (nn: nn) (d: dataset t) (eps: t) =
+     DatasetCSV.forall_ d (robust_around valid_label nn eps)
 
 end
\ No newline at end of file

tests/interpretation_acasxu.t → tests/acasxu.t

-Test interpret on acasxu
+Test verify on acasxu
   $ . ./setup_env.sh
 
   $ bin/pyrat.py --version

tests/interpretation_dataset.t

-Test interpret on dataset
-  $ cat - > dataset.csv << EOF
-  > 2,0.0,1.0,0.784313725,0.019607843,0.776470588
-  > 0,0.941176471,0,0,0.011764706,0.039215686
-  > EOF
-
-  $ . ./setup_env.sh
-
-  $ bin/Marabou --version
-  1.0.+
-
-  $ caisar verify -L . --format whyml --ltag=ProverSpec --prover=Marabou - 2>&1 <<EOF | ./filter_tmpdir.sh
-  > theory T
-  >   use ieee_float.Float64
-  >   use int.Int
-  >   use nn.NeuralNetwork
-  >   use dataset.DatasetCSV
-  >   use robustness.RobustDatasetCSV
-  > 
-  >   goal G:
-  >     let nn = read_neural_network "TestNetwork.nnet" NNet in
-  >     let dataset = read_dataset_csv "dataset.csv" in
-  >     let eps = (0.0100000000000000002081668171172168513294309377670288085937500000:t) in
-  >     robust nn dataset eps
-  > end
-  > EOF
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 1.0
-  x1 >= 0.0
-  x1 <= 1.0
-  x2 >= 0.0
-  x2 <= 1.0
-  x3 >= 0.0
-  x3 <= 1.0
-  x4 >= 0.0
-  x4 <= 1.0
-  x0 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x0 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x1 >= 0.9899999999999999911182158029987476766109466552734375
-  x1 <= 1.0100000000000000088817841970012523233890533447265625
-  x2 >= 0.77431372499999995273611830270965583622455596923828125
-  x2 <= 0.79431372499999997049968669671216048300266265869140625
-  x3 >= 0.00960784299999999959196461674082456738688051700592041015625
-  x3 <= 0.029607843000000001743021726952065364457666873931884765625
-  x4 >= 0.7664705880000000082219457908649928867816925048828125
-  x4 <= 0.7864705880000000259855141848674975335597991943359375
-  +y0 -y2 >= 0
-  
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 1.0
-  x1 >= 0.0
-  x1 <= 1.0
-  x2 >= 0.0
-  x2 <= 1.0
-  x3 >= 0.0
-  x3 <= 1.0
-  x4 >= 0.0
-  x4 <= 1.0
-  x0 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x0 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x1 >= 0.9899999999999999911182158029987476766109466552734375
-  x1 <= 1.0100000000000000088817841970012523233890533447265625
-  x2 >= 0.77431372499999995273611830270965583622455596923828125
-  x2 <= 0.79431372499999997049968669671216048300266265869140625
-  x3 >= 0.00960784299999999959196461674082456738688051700592041015625
-  x3 <= 0.029607843000000001743021726952065364457666873931884765625
-  x4 >= 0.7664705880000000082219457908649928867816925048828125
-  x4 <= 0.7864705880000000259855141848674975335597991943359375
-  +y1 -y2 >= 0
-  
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 1.0
-  x1 >= 0.0
-  x1 <= 1.0
-  x2 >= 0.0
-  x2 <= 1.0
-  x3 >= 0.0
-  x3 <= 1.0
-  x4 >= 0.0
-  x4 <= 1.0
-  x0 >= 0.93117647100000000559560930923908017575740814208984375
-  x0 <= 0.95117647100000002335917770324158482253551483154296875
-  x1 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x1 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x2 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x2 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x3 >= 0.00176470599999999956664087363833459676243364810943603515625
-  x3 <= 0.021764706000000001717697983849575393833220005035400390625
-  x4 >= 0.029215685999999997657372574622058891691267490386962890625
-  x4 <= 0.049215686000000001543153160810106783173978328704833984375
-  +y1 -y0 >= 0
-  
-  [DEBUG]{ProverSpec} Prover-tailored specification:
-  x0 >= 0.0
-  x0 <= 1.0
-  x1 >= 0.0
-  x1 <= 1.0
-  x2 >= 0.0
-  x2 <= 1.0
-  x3 >= 0.0
-  x3 <= 1.0
-  x4 >= 0.0
-  x4 <= 1.0
-  x0 >= 0.93117647100000000559560930923908017575740814208984375
-  x0 <= 0.95117647100000002335917770324158482253551483154296875
-  x1 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x1 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x2 >= -0.01000000000000000020816681711721685132943093776702880859375
-  x2 <= 0.01000000000000000020816681711721685132943093776702880859375
-  x3 >= 0.00176470599999999956664087363833459676243364810943603515625
-  x3 <= 0.021764706000000001717697983849575393833220005035400390625
-  x4 >= 0.029215685999999997657372574622058891691267490386962890625
-  x4 <= 0.049215686000000001543153160810106783173978328704833984375
-  +y2 -y0 >= 0
-  
-  Goal G: Unknown ()