diff --git a/src/interpretation.ml b/src/interpretation.ml
index bb35079baf0e14f0728747252f28456a83e57fcd..791571a7c2bdf0f0309c88112217dcadbd1b24f8 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -24,19 +24,19 @@ module CRE = Reduction_engine (* CAISAR Reduction Engine *)
open Why3
open Base
-type classifier =
+type nn =
| NNet of Term.lsymbol
[@printer
fun fmt nn ->
Fmt.pf fmt "NNet: %a"
Fmt.(option Language.pp_nn)
- (Language.lookup_nn_classifier nn)]
+ (Language.lookup_nn nn)]
| ONNX of Term.lsymbol
[@printer
fun fmt nn ->
Fmt.pf fmt "ONNX: %a"
Fmt.(option Language.pp_nn)
- (Language.lookup_nn_classifier nn)]
+ (Language.lookup_nn nn)]
[@@deriving show]
type dataset = DS_csv of Csv.t [@printer fun fmt _ -> Fmt.pf fmt "<csv>"]
@@ -52,7 +52,7 @@ type vector =
[@@deriving show]
type caisar_op =
- | Classifier of classifier
+ | NeuralNetwork of nn
| Dataset of dataset
| Data of data
| Vector of vector
@@ -73,7 +73,7 @@ let ls_of_caisar_op engine caisar_op ty_args ty =
let id = Ident.id_fresh "caisar_op" in
let ls =
match caisar_op with
- | Classifier (NNet c | ONNX c) -> c
+ | NeuralNetwork (NNet n | ONNX n) -> n
| Vector v -> v
| _ -> Term.create_lsymbol id ty_args ty
in
@@ -159,7 +159,7 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
let n = Option.value_exn (Language.lookup_vector v) in
assert (List.length tl1 = n && i <= n);
term (List.nth_exn tl1 i)
- | Data _ | Classifier _ -> assert false)
+ | Data _ | NeuralNetwork _ -> assert false)
| [ Term t1; Term t2 ] ->
(* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
term (Term.t_app_infer ls [ t1; t2 ])
@@ -177,14 +177,14 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
| Vector v ->
int (BigInt.of_int (Option.value_exn (Language.lookup_vector v)))
| Data (D_csv data) -> int (BigInt.of_int (List.length data))
- | Classifier _ -> assert false)
+ | NeuralNetwork _ -> assert false)
| [ Term { t_node = Tapp (ls, tl); _ } ] -> (
match caisar_op_of_ls engine ls with
| Vector v ->
let n = Option.value_exn (Language.lookup_vector v) in
assert (List.length tl = n);
int (BigInt.of_int n)
- | Dataset _ | Data _ | Classifier _ -> assert false)
+ | Dataset _ | Data _ | NeuralNetwork _ -> assert false)
| [ Term t ] ->
(* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
term (Term.t_app_infer ls [ t ])
@@ -260,40 +260,42 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
in
Eval (term_of_caisar_op ~args engine caisar_op ty)
| Dataset (DS_csv csv) -> int (BigInt.of_int (Csv.lines csv))
- | Data _ | Classifier _ -> assert false)
+ | Data _ | NeuralNetwork _ -> assert false)
| [ Term t1; Term t2 ] ->
(* Fmt.pr "Terms: %a , %a@." Pretty.print_term t1 Pretty.print_term t2; *)
term (Term.t_app_infer ls [ t1; t2 ])
| _ -> invalid_arg (error_message ls)
in
- (* Classifier *)
- let read_classifier : _ CRE.builtin =
+ (* Neural Network *)
+ let read_neural_network : _ CRE.builtin =
fun engine ls vl ty ->
- (* Fmt.pr "--@.read_classifier: ls:%a , ty:%a@." Pretty.print_ls ls *)
+ (* Fmt.pr "--@.read_neural_network: ls:%a , ty:%a@." Pretty.print_ls ls *)
(* Fmt.(option ~none:nop Pretty.print_ty) *)
(* ty; *)
match vl with
| [
- Term { t_node = Tconst (ConstStr classifier); _ };
+ Term { t_node = Tconst (ConstStr neural_network); _ };
Term { t_node = Tapp ({ ls_name = { id_string; _ }; _ }, []); _ };
] ->
let { env; cwd; _ } = CRE.user_env engine in
let caisar_op =
- let filename = Caml.Filename.concat cwd classifier in
- let classifier =
- if String.equal id_string "NNet"
- then NNet (Language.create_nnet_classifier env filename)
- else ONNX (Language.create_onnx_classifier env filename)
+ let filename = Caml.Filename.concat cwd neural_network in
+ let nn =
+ match id_string with
+ | "NNet" -> NNet (Language.create_nnet_nn env filename)
+ | "ONNX" -> ONNX (Language.create_onnx_nn env filename)
+ | _ ->
+ failwith (Fmt.str "Unrecognized neural network format %s" id_string)
in
- Classifier classifier
+ NeuralNetwork nn
in
term (term_of_caisar_op engine caisar_op ty)
| _ -> invalid_arg (error_message ls)
in
- let apply_classifier : _ CRE.builtin =
+ let apply_neural_network : _ CRE.builtin =
fun _engine ls vl _ty ->
- (* Fmt.pr "--@.apply_classifier: ls:%a , ty:%a@." Pretty.print_ls ls *)
+ (* Fmt.pr "--@.apply_neural_network: ls:%a , ty:%a@." Pretty.print_ls ls *)
(* Fmt.(option ~none:nop Pretty.print_ty) *)
(* ty; *)
match vl with
@@ -335,11 +337,11 @@ let builtin_caisar : caisar_env CRE.built_in_theories list =
([ "L"; "mapi" ], None, mapi);
] );
( [ "interpretation" ],
- "Classifier",
+ "NeuralNetwork",
[],
[
- ([ "read_classifier" ], None, read_classifier);
- ([ Ident.op_infix "%%" ], None, apply_classifier);
+ ([ "read_neural_network" ], None, read_neural_network);
+ ([ Ident.op_infix "%%" ], None, apply_neural_network);
] );
( [ "interpretation" ],
"Dataset",
@@ -383,10 +385,10 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
| _ -> None
let declare_language_lsymbols caisar_env task =
- (* Declare [Language] logic symbols for classifiers and vectors only. *)
+ (* Declare [Language] logic symbols for neural networks and vectors only. *)
Term.Hls.fold
(fun ls _ task ->
- if Language.mem_vector ls || Language.mem_nn_classifier ls
+ if Language.mem_vector ls || Language.mem_nn ls
then
let decl = Decl.create_param_decl ls in
Task.add_decl task decl
diff --git a/src/language.ml b/src/language.ml
index 3c7db414e837f38dfb5e357c4e8c6baef98ae42a..d525b1f8602c0e17e9327574c3a16d7e0fc244e3 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -194,17 +194,17 @@ type nn = {
}
[@@deriving show]
-let nn_classifiers = Term.Hls.create 10
+let nets = Term.Hls.create 10
-let fresh_classifier_ls env name =
+let fresh_nn_ls env name =
let ty =
- let th = Env.read_theory env [ "interpretation" ] "Classifier" in
- Ty.ty_app (Theory.ns_find_ts th.th_export [ "classifier" ]) []
+ let th = Env.read_theory env [ "interpretation" ] "NeuralNetwork" in
+ Ty.ty_app (Theory.ns_find_ts th.th_export [ "nn" ]) []
in
let id = Ident.id_fresh name in
Term.create_fsymbol id [] ty
-let create_nnet_classifier =
+let create_nnet_nn =
Env.Wenv.memoize 13 (fun env ->
let h = Hashtbl.create (module String) in
let ty_elt =
@@ -212,7 +212,7 @@ let create_nnet_classifier =
Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) []
in
Hashtbl.findi_or_add h ~default:(fun filename ->
- let ls = fresh_classifier_ls env "nnet_classifier" in
+ let ls = fresh_nn_ls env "nnet_nn" in
let nn =
let model = Nnet.parse ~permissive:true filename in
match model with
@@ -226,15 +226,15 @@ let create_nnet_classifier =
nn_nier = None;
}
in
- Term.Hls.add nn_classifiers ls nn;
+ Term.Hls.add nets ls nn;
ls))
-let create_onnx_classifier =
+let create_onnx_nn =
Env.Wenv.memoize 13 (fun env ->
let h = Hashtbl.create (module String) in
let ty_elt = vector_elt_ty env in
Hashtbl.findi_or_add h ~default:(fun filename ->
- let ls = fresh_classifier_ls env "onnx_classifier" in
+ let ls = fresh_nn_ls env "onnx_nn" in
let onnx =
let model = Onnx.parse filename in
match model with
@@ -256,8 +256,8 @@ let create_onnx_classifier =
nn_nier = nier;
}
in
- Term.Hls.add nn_classifiers ls onnx;
+ Term.Hls.add nets ls onnx;
ls))
-let lookup_nn_classifier = Term.Hls.find_opt nn_classifiers
-let mem_nn_classifier = Term.Hls.mem nn_classifiers
+let lookup_nn = Term.Hls.find_opt nets
+let mem_nn = Term.Hls.mem nets
diff --git a/src/language.mli b/src/language.mli
index 4ac58bcf338eb7d45106590697eed67a3332b33c..380465783b7c74eef609ec0f715de98c68dad43c 100644
--- a/src/language.mli
+++ b/src/language.mli
@@ -69,7 +69,7 @@ val create_vector : Env.env -> int -> Term.lsymbol
val lookup_vector : Term.lsymbol -> int option
val mem_vector : Term.lsymbol -> bool
-(** -- Classifier *)
+(** -- Neural Network *)
type nn = private {
nn_inputs : int;
@@ -80,7 +80,7 @@ type nn = private {
}
[@@deriving show]
-val create_nnet_classifier : Env.env -> string -> Term.lsymbol
-val create_onnx_classifier : Env.env -> string -> Term.lsymbol
-val lookup_nn_classifier : Term.lsymbol -> nn option
-val mem_nn_classifier : Term.lsymbol -> bool
+val create_nnet_nn : Env.env -> string -> Term.lsymbol
+val create_onnx_nn : Env.env -> string -> Term.lsymbol
+val lookup_nn : Term.lsymbol -> nn option
+val mem_nn : Term.lsymbol -> bool
diff --git a/src/proof_strategy.ml b/src/proof_strategy.ml
index f4bccd141448405e923bda16e75005b2cd287cf8..6bf8cf1df1cc711d511204c08be2db1998f323fa 100644
--- a/src/proof_strategy.ml
+++ b/src/proof_strategy.ml
@@ -32,8 +32,8 @@ let apply_classic_prover env task =
let apply_native_nn_prover env task =
let nb_nn_apply = Trans.apply Utils.count_nn_apply task in
- let nb_nn_classifiers = Trans.apply Utils.count_nn_classifiers task in
- match (nb_nn_apply, nb_nn_classifiers) with
+ let nb_nn_applications = Trans.apply Utils.count_nn_applications task in
+ match (nb_nn_apply, nb_nn_applications) with
| 0, 0 -> task
| 1, 0 ->
Trans.(
@@ -50,7 +50,7 @@ let apply_native_nn_prover env task =
(seq
[
Introduction.introduce_premises;
- Native_nn_prover.trans_nn_classifier env;
+ Native_nn_prover.trans_nn_application env;
]))
task
| _ ->
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index 9bb96dd31c1ae22eb8e76203e4ba47d5e1bd67e4..d3b79df98168f8133f953a6f6878cc4886e6198c 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -108,7 +108,7 @@ let get_input_variables =
( { ls_name; _ },
[ { t_node = Tapp (ls1, _); _ }; { t_node = Tapp (ls2, args); _ } ] )
when String.equal ls_name.id_string (Ident.op_infix "%%") -> (
- match (Language.lookup_nn_classifier ls1, Language.lookup_vector ls2) with
+ match (Language.lookup_nn ls1, Language.lookup_vector ls2) with
| Some { nn_inputs; _ }, Some n ->
assert (nn_inputs = n && n = List.length args);
List.foldi ~init:acc ~f:add args
@@ -127,9 +127,9 @@ let simplify_goal _env input_variables =
({
t_node =
Tapp
- ( ls_apply_classifier,
+ ( ls_apply_nn,
[
- { t_node = Tapp (ls_nn_classifier, _); _ };
+ { t_node = Tapp (ls_nn, _); _ };
{ t_node = Tapp (ls_vector, _); _ };
] );
_;
@@ -137,12 +137,9 @@ let simplify_goal _env input_variables =
({ t_node = Tconst (ConstInt i); _ } as _t2);
] )
when String.equal ls_vget.ls_name.id_string (Ident.op_get "")
- && String.equal ls_apply_classifier.ls_name.id_string
- (Ident.op_infix "%%") -> (
- match
- ( Language.lookup_nn_classifier ls_nn_classifier,
- Language.lookup_vector ls_vector )
- with
+ && String.equal ls_apply_nn.ls_name.id_string (Ident.op_infix "%%")
+ -> (
+ match (Language.lookup_nn ls_nn, Language.lookup_vector ls_vector) with
| Some nn, Some _ ->
let index = Number.to_small_integer i in
let hout =
@@ -198,4 +195,5 @@ let simplify_goal _env input_variables =
Task.add_decl acc decl)
None
-let trans_nn_classifier env = Trans.bind get_input_variables (simplify_goal env)
+let trans_nn_application env =
+ Trans.bind get_input_variables (simplify_goal env)
diff --git a/src/transformations/native_nn_prover.mli b/src/transformations/native_nn_prover.mli
index 84ea9445a90334e98d54c09d69bec8759f982585..eaebc8b2e3393b64f5e3777dfe068cfe723eabe2 100644
--- a/src/transformations/native_nn_prover.mli
+++ b/src/transformations/native_nn_prover.mli
@@ -23,4 +23,4 @@
open Why3
val trans_nn_apply : Env.env -> Task.task Trans.trans
-val trans_nn_classifier : Env.env -> Task.task Trans.trans
+val trans_nn_application : Env.env -> Task.task Trans.trans
diff --git a/src/transformations/utils.ml b/src/transformations/utils.ml
index 892ad38e3ad8c6876d12bc05a132e40e003c710b..a8d9046dfcd72c836b22488740e0d012e5565f90 100644
--- a/src/transformations/utils.ml
+++ b/src/transformations/utils.ml
@@ -35,12 +35,12 @@ let count_nn_apply =
in
Trans.fold_decl (fun decl acc -> Decl.decl_fold aux acc decl) 0
-let count_nn_classifiers =
+let count_nn_applications =
let rec aux acc (term : Term.term) =
let acc = Term.t_fold aux acc term in
match term.t_node with
| Term.Tapp (ls, _) -> (
- match Language.lookup_nn_classifier ls with
+ match Language.lookup_nn ls with
| None -> acc
| Some _ -> Term.Sls.add ls acc)
| _ -> acc
diff --git a/src/transformations/utils.mli b/src/transformations/utils.mli
index 8d54c046ef0ace740245a239e8933c6d0b000e52..5eb81e3252b539941ea2a3395d8eadee14ec3477 100644
--- a/src/transformations/utils.mli
+++ b/src/transformations/utils.mli
@@ -25,12 +25,12 @@ open Why3
val count_nn_apply : int Trans.trans
(** Count the number of applications of [nn_apply]. *)
-val count_nn_classifiers : int Trans.trans
-(** Count the number of applications of a NN classifier. *)
+val count_nn_applications : int Trans.trans
+(** Count the number of applications of a neural network. *)
val get_input_variables : int Term.Mls.t Trans.trans
-(** Retrieve the input variables appearing as arguments of [nn_apply] or a NN
- classifier. *)
+(** Retrieve the input variables appearing as arguments of [nn_apply] or a
+ neural network. *)
val meta_input : Theory.meta
(** Indicate the input position. *)
diff --git a/stdlib/interpretation.mlw b/stdlib/interpretation.mlw
index f5c850372124c3f764130401cef47b64b081c654..28ecc34a8da73b2f0fe5899a041d854d2029184f 100644
--- a/stdlib/interpretation.mlw
+++ b/stdlib/interpretation.mlw
@@ -52,14 +52,14 @@ theory Vector
end
end
-theory Classifier
+theory NeuralNetwork
use Vector
- type classifier
- type kind = ONNX | NNet | OVO
+ type nn
+ type format = ONNX | NNet
- function read_classifier (f: string) (k: kind) : classifier
- function (%%) (c: classifier) (v: vector 'a) : vector 'a
+ function read_neural_network (n: string) (f: format) : nn
+ function (%%) (n: nn) (v: vector 'a) : vector 'a
end
theory Dataset
diff --git a/tests/interpretation_acasxu.t b/tests/interpretation_acasxu.t
index daac6bfda65083218cc825d9bb29455f745eaebb..6f3171d857a2d73434733da105526e515600b44b 100644
--- a/tests/interpretation_acasxu.t
+++ b/tests/interpretation_acasxu.t
@@ -13,9 +13,9 @@ Test interpret on acasxu
> use bool.Bool
> use int.Int
> use interpretation.Vector
- > use interpretation.Classifier
+ > use interpretation.NeuralNetwork
>
- > constant classifier: classifier = read_classifier "TestNetwork.nnet" NNet
+ > constant nn: nn = read_neural_network "TestNetwork.nnet" NNet
>
> type input = vector t
>
@@ -44,10 +44,10 @@ Test interpret on acasxu
>
> predicate valid_action (a: action) = clear_of_conflict <= a <= strong_right
>
- > predicate advises (c: classifier) (i: input) (a: action) =
+ > predicate advises (n: nn) (i: input) (a: action) =
> valid_action a ->
> forall b: action.
- > valid_action b -> a <> b -> (c%%i)[a] .< (c%%i)[b]
+ > valid_action b -> a <> b -> (n%%i)[a] .< (n%%i)[b]
>
> predicate intruder_distant_and_slow (i: input) =
> i[distance_to_intruder] .>= (55947.6909999999988940544426441192626953125:t)
@@ -75,7 +75,7 @@ Test interpret on acasxu
> has_length i 5 ->
> let j = denormalize_input i in
> valid_input j /\ intruder_distant_and_slow j ->
- > let o = (classifier%%i)[clear_of_conflict] in
+ > let o = (nn%%i)[clear_of_conflict] in
> (denormalize_output o) .<= (1500.0:t)
>
> predicate directly_ahead (i: input) =
@@ -92,7 +92,7 @@ Test interpret on acasxu
> has_length i 5 ->
> let j = denormalize_input i in
> valid_input j /\ directly_ahead j /\ moving_towards j ->
- > not (advises classifier i clear_of_conflict)
+ > not (advises nn i clear_of_conflict)
> end
> EOF
[caisar] Goal P1: Unknown ()
diff --git a/tests/interpretation_dataset.t b/tests/interpretation_dataset.t
index 0dd6f08893880fa641e540d05b6cfd0a2e61c0a3..2af01dbfb95a31dc16fb5c5b7c2d3cf591961b6e 100644
--- a/tests/interpretation_dataset.t
+++ b/tests/interpretation_dataset.t
@@ -17,7 +17,7 @@ Test interpret on dataset
> use bool.Bool
> use int.Int
> use interpretation.Vector
- > use interpretation.Classifier
+ > use interpretation.NeuralNetwork
> use interpretation.Dataset
>
> type image = vector t
@@ -28,29 +28,29 @@ Test interpret on dataset
>
> predicate valid_label (l: label_) = 0 <= l <= 2
>
- > predicate advises (c: classifier) (i: image) (l: label_) =
+ > predicate advises (n: nn) (i: image) (l: label_) =
> valid_label l ->
- > forall j: int. valid_label j -> j <> l -> (c%%i)[l] .> (c%%i)[j]
+ > forall j: int. valid_label j -> j <> l -> (n%%i)[l] .> (n%%i)[j]
>
> predicate bounded_by_epsilon (i: image) (eps: t) =
> forall v: index. valid_index i v -> .- eps .<= i[v] .<= eps
>
- > predicate robust_around (c: classifier) (eps: t) (i: image) (l: label_) =
+ > predicate robust_around (n: nn) (eps: t) (i: image) (l: label_) =
> forall perturbed_image: image.
> has_length perturbed_image (length i) ->
> valid_image perturbed_image ->
> let perturbation = perturbed_image - i in
> bounded_by_epsilon perturbation eps ->
- > advises c perturbed_image l
+ > advises n perturbed_image l
>
- > predicate robust (c: classifier) (d: dataset image label_) (eps: t) =
- > Dataset.L.forall_ d (robust_around c eps)
+ > predicate robust (n: nn) (d: dataset image label_) (eps: t) =
+ > Dataset.L.forall_ d (robust_around n eps)
>
> goal G:
- > let classifier = read_classifier "TestNetwork.nnet" NNet in
+ > let nn = read_neural_network "TestNetwork.nnet" NNet in
> let dataset = read_dataset "dataset.csv" CSV in
> let eps = (0.375:t) in
- > robust classifier dataset eps
+ > robust nn dataset eps
> end
> EOF
[caisar] Goal G: Unknown ()