Skip to content
Snippets Groups Projects
Commit 669b6cd3 authored by Michele Alberti's avatar Michele Alberti
Browse files

[verification] Early goal split before applying transformations.

parent 03794fb2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/verification.ml
+ 22
− 17
View file @ 669b6cd3
...@@ -224,24 +224,29 @@ let answer_dataset limit config env prover config_prover driver dataset task = ...@@ -224,24 +224,29 @@ let answer_dataset limit config env prover config_prover driver dataset task =
(prover_answer, additional_info) (prover_answer, additional_info)
let answer_generic limit config prover config_prover driver task = let answer_generic limit config prover config_prover driver task =
let task = Driver.prepare_task driver task in let tasks = Trans.apply Split_goal.split_goal_full 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 answers = 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 in
let prover_answer = combine_prover_answers answers in let prover_answer = combine_prover_answers answers in
let additional_info = Generic None in let additional_info = Generic None in
......
tests/interpretation_acasxu.t
+ 3
− 134
View file @ 669b6cd3
...@@ -87,137 +87,6 @@ Test interpret on acasxu ...@@ -87,137 +87,6 @@ Test interpret on acasxu
> not (advises classifier i clear_of_conflict) > not (advises classifier i clear_of_conflict)
> end > end
> EOF > EOF
P1 : forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t. [caisar][ERROR] This expression isn't supported:
((le (0.0:t) (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) /\ not (((lt y y1 /\ lt y y2) /\ lt y y3) /\ lt y y4)
le (add RNE (mul RNE caisar_v (60261.0:t)) (19791.0:t)) (60760.0:t)) /\ PyRAT: not a base term
(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)
tests/interpretation_dataset.t
+ 2
− 107
View file @ 669b6cd3
...@@ -4,7 +4,7 @@ Test interpret on dataset ...@@ -4,7 +4,7 @@ Test interpret on dataset
> 0,1.0,0.0,0.019607843,0.776470588,0.784313725 > 0,1.0,0.0,0.019607843,0.776470588,0.784313725
> EOF > 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 > theory T
> use ieee_float.Float64 > use ieee_float.Float64
> use bool.Bool > use bool.Bool
...@@ -46,109 +46,4 @@ Test interpret on dataset ...@@ -46,109 +46,4 @@ Test interpret on dataset
> robust classifier dataset eps > robust classifier dataset eps
> end > end
> EOF > EOF
G : (forall caisar_v:t, caisar_v1:t, caisar_v2:t, caisar_v3:t, caisar_v4:t. [caisar] Goal G: High failure
((((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"]))
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment