From 669b6cd31f5afa02b2d25555a4f1fc02701a777a Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Mon, 17 Apr 2023 13:55:23 +0200
Subject: [PATCH] [verification] Early goal split before applying
transformations.
---
src/verification.ml | 39 ++++++----
tests/interpretation_acasxu.t | 137 +--------------------------------
tests/interpretation_dataset.t | 109 +-------------------------
3 files changed, 27 insertions(+), 258 deletions(-)
diff --git a/src/verification.ml b/src/verification.ml
index 4e60bf6..9a52272 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -224,24 +224,29 @@ let answer_dataset limit config env prover config_prover driver dataset task =
(prover_answer, additional_info)
let answer_generic limit config prover config_prover driver task =
- let task = Driver.prepare_task driver task in
- let nn_file =
- match Task.on_meta_excl Utils.meta_nn_filename task with
- | Some [ MAstr nn_file ] -> Unix.realpath nn_file
- | Some _ -> assert false (* By construction of the meta. *)
- | None -> invalid_arg "No neural network model found in task"
- in
- let tasks =
- (* We turn [task] into a list (ie, conjunction) of disjunctions of tasks. *)
- match prover with
- | Prover.Marabou -> Trans.apply Split.split_all task
- | Pyrat | Nnenum -> Trans.apply Split.split_premises task
- | _ -> [ task ]
- in
- let command = Whyconf.get_complete_command ~with_steps:false config_prover in
- let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
+ let tasks = Trans.apply Split_goal.split_goal_full task in
let answers =
- List.map tasks ~f:(call_prover_on_task limit config command driver)
+ List.concat_map tasks ~f:(fun task ->
+ let task = Driver.prepare_task driver task in
+ let nn_file =
+ match Task.on_meta_excl Utils.meta_nn_filename task with
+ | Some [ MAstr nn_file ] -> Unix.realpath nn_file
+ | Some _ -> assert false (* By construction of the meta. *)
+ | None -> invalid_arg "No neural network model found in task"
+ in
+ let tasks =
+ (* Turn [task] into a list (ie, conjunction) of disjunctions of
+ tasks. *)
+ match prover with
+ | Prover.Marabou -> Trans.apply Split.split_all task
+ | Pyrat | Nnenum -> Trans.apply Split.split_premises task
+ | _ -> [ task ]
+ in
+ let command =
+ Whyconf.get_complete_command ~with_steps:false config_prover
+ in
+ let command = Re__Core.replace_string nnet_or_onnx ~by:nn_file command in
+ List.map tasks ~f:(call_prover_on_task limit config command driver))
in
let prover_answer = combine_prover_answers answers in
let additional_info = Generic None in
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index 074f1d1..fb7b297 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -87,137 +87,6 @@ Test interpret on acasxu
> not (advises classifier i clear_of_conflict)
> end
> EOF
- P1 : forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
- ((le (0.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (60760.0:t)) /\
- (le (neg (3.141592999999999857863031138549558818340301513671875:t))
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592999999999857863031138549558818340301513671875:t)) /\
- (le (neg (3.141592999999999857863031138549558818340301513671875:t))
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592999999999857863031138549558818340301513671875:t)) /\
- (le (100.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
- le (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) (1200.0:t)) /\
- le (0.0:t) (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) /\
- le (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) (1200.0:t)) /\
- le (55947.6909999999988940544426441192626953125:t)
- (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
- le (1145.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
- le (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) (60.0:t) ->
- le
- (add RNE
- (mul RNE
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [0] (373.9499200000000200816430151462554931640625:t))
- (7.51888402010059753166615337249822914600372314453125:t))
- (1500.0:t)
- nnet_classifier,
- (Interpretation.Classifier
- NNet: { Language.nn_inputs = 5; nn_outputs = 5; nn_ty_elt = t;
- nn_filename =
- "$TESTCASE_ROOT/TestNetwork.nnet";
- nn_nier = <opaque> })
- vector,
- (Interpretation.Vector 5)
- P2 : forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
- ((le (0.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (60760.0:t)) /\
- (le (neg (3.141592999999999857863031138549558818340301513671875:t))
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592999999999857863031138549558818340301513671875:t)) /\
- (le (neg (3.141592999999999857863031138549558818340301513671875:t))
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (3.141592999999999857863031138549558818340301513671875:t)) /\
- (le (100.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
- le (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) (1200.0:t)) /\
- le (0.0:t) (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) /\
- le (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) (1200.0:t)) /\
- ((le (1500.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\
- le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (1800.0:t)) /\
- le (neg (0.059999999999999997779553950749686919152736663818359375:t))
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le
- (add RNE
- (mul RNE caisar_v1
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t))
- (0.059999999999999997779553950749686919152736663818359375:t)) /\
- le (3.100000000000000088817841970012523233890533447265625:t)
- (add RNE
- (mul RNE caisar_v2
- (6.2831853071800001231395071954466402530670166015625:t))
- (0.0:t)) /\
- le (900.0:t) (add RNE (mul RNE caisar_v3 (1100.0:t)) (650.0:t)) /\
- le (960.0:t) (add RNE (mul RNE caisar_v4 (1200.0:t)) (600.0:t)) ->
- not (((lt
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [0]
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [1] /\
- lt
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [0]
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [2]) /\
- lt
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [0]
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [3]) /\
- lt
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [0]
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [4])
- nnet_classifier,
- (Interpretation.Classifier
- NNet: { Language.nn_inputs = 5; nn_outputs = 5; nn_ty_elt = t;
- nn_filename =
- "$TESTCASE_ROOT/TestNetwork.nnet";
- nn_nier = <opaque> })
- vector,
- (Interpretation.Vector 5)
+ [caisar][ERROR] This expression isn't supported:
+ not (((lt y y1 /\ lt y y2) /\ lt y y3) /\ lt y y4)
+ PyRAT: not a base term
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index f1d9598..bd1b86e 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -4,7 +4,7 @@ Test interpret on dataset
> 0,1.0,0.0,0.019607843,0.776470588,0.784313725
> EOF
- $ caisar verify -L . --format whyml --prover Marabou -vv - 2>&1 <<EOF | ./filter_tmpdir.sh
+ $ caisar verify -L . --format whyml --prover Marabou - 2>&1 <<EOF | ./filter_tmpdir.sh
> theory T
> use ieee_float.Float64
> use bool.Bool
@@ -46,109 +46,4 @@ Test interpret on dataset
> robust classifier dataset eps
> end
> EOF
- G : (forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
- ((((le (0.0:t) caisar_v /\ le caisar_v (1.0:t)) /\
- le (0.0:t) caisar_v1 /\ le caisar_v1 (1.0:t)) /\
- le (0.0:t) caisar_v2 /\ le caisar_v2 (1.0:t)) /\
- le (0.0:t) caisar_v3 /\ le caisar_v3 (1.0:t)) /\
- le (0.0:t) caisar_v4 /\ le caisar_v4 (1.0:t) ->
- ((((le (neg (0.375:t)) (sub RNE caisar_v (0.0:t)) /\
- le (sub RNE caisar_v (0.0:t)) (0.375:t)) /\
- le (neg (0.375:t)) (sub RNE caisar_v1 (1.0:t)) /\
- le (sub RNE caisar_v1 (1.0:t)) (0.375:t)) /\
- le (neg (0.375:t))
- (sub RNE caisar_v2
- (0.78431372499999996161790249971090815961360931396484375:t)) /\
- le
- (sub RNE caisar_v2
- (0.78431372499999996161790249971090815961360931396484375:t))
- (0.375:t)) /\
- le (neg (0.375:t))
- (sub RNE caisar_v3
- (0.01960784299999999980013143385804141871631145477294921875:t)) /\
- le
- (sub RNE caisar_v3
- (0.01960784299999999980013143385804141871631145477294921875:t))
- (0.375:t)) /\
- le (neg (0.375:t))
- (sub RNE caisar_v4
- (0.776470588000000017103729987866245210170745849609375:t)) /\
- le
- (sub RNE caisar_v4
- (0.776470588000000017103729987866245210170745849609375:t))
- (0.375:t) ->
- lt
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [0]
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [1] /\
- lt
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [2]
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [1]) /\
- (forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t.
- ((((le (0.0:t) caisar_v /\ le caisar_v (1.0:t)) /\
- le (0.0:t) caisar_v1 /\ le caisar_v1 (1.0:t)) /\
- le (0.0:t) caisar_v2 /\ le caisar_v2 (1.0:t)) /\
- le (0.0:t) caisar_v3 /\ le caisar_v3 (1.0:t)) /\
- le (0.0:t) caisar_v4 /\ le caisar_v4 (1.0:t) ->
- ((((le (neg (0.375:t)) (sub RNE caisar_v (1.0:t)) /\
- le (sub RNE caisar_v (1.0:t)) (0.375:t)) /\
- le (neg (0.375:t)) (sub RNE caisar_v1 (0.0:t)) /\
- le (sub RNE caisar_v1 (0.0:t)) (0.375:t)) /\
- le (neg (0.375:t))
- (sub RNE caisar_v2
- (0.01960784299999999980013143385804141871631145477294921875:t)) /\
- le
- (sub RNE caisar_v2
- (0.01960784299999999980013143385804141871631145477294921875:t))
- (0.375:t)) /\
- le (neg (0.375:t))
- (sub RNE caisar_v3
- (0.776470588000000017103729987866245210170745849609375:t)) /\
- le
- (sub RNE caisar_v3
- (0.776470588000000017103729987866245210170745849609375:t))
- (0.375:t)) /\
- le (neg (0.375:t))
- (sub RNE caisar_v4
- (0.78431372499999996161790249971090815961360931396484375:t)) /\
- le
- (sub RNE caisar_v4
- (0.78431372499999996161790249971090815961360931396484375:t))
- (0.375:t) ->
- lt
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [1]
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [0] /\
- lt
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [2]
- (nnet_classifier
- %% vector caisar_v caisar_v1 caisar_v2 caisar_v3 caisar_v4)
- [0])
- caisar_op,
- (Interpretation.Data
- (Interpretation.D_csv
- ["1.0"; "0.0"; "0.019607843"; "0.776470588"; "0.784313725"]))
- vector, (Interpretation.Vector 5)
- nnet_classifier,
- (Interpretation.Classifier
- NNet: { Language.nn_inputs = 5; nn_outputs = 5; nn_ty_elt = t;
- nn_filename =
- "$TESTCASE_ROOT/TestNetwork.nnet";
- nn_nier = <opaque> })
- caisar_op1, (Interpretation.Dataset <csv>)
- caisar_op2,
- (Interpretation.Data
- (Interpretation.D_csv
- ["0.0"; "1.0"; "0.784313725"; "0.019607843"; "0.776470588"]))
+ [caisar] Goal G: High failure
--
GitLab