From 84eff242a952af2e07eba29b42226cd8d29b6112 Mon Sep 17 00:00:00 2001
From: Aymeric Varasse <aymeric.varasse@cea.fr>
Date: Fri, 20 Jan 2023 18:24:18 +0100
Subject: [PATCH] [stdlib] Add metamorphic robust predicate.
---
src/AIMOS.ml | 2 +-
src/JSON.ml | 2 +-
src/SAVer.ml | 3 +++
src/dataset.ml | 10 ++++++++++
src/dataset.mli | 5 +++++
stdlib/caisar.mlw | 2 ++
6 files changed, 22 insertions(+), 2 deletions(-)
diff --git a/src/AIMOS.ml b/src/AIMOS.ml
index f4e0c73..1588dd3 100644
--- a/src/AIMOS.ml
+++ b/src/AIMOS.ml
@@ -34,7 +34,7 @@ let re_aimos_output = Re__Pcre.regexp "((,\\s)(\\d+\\.\\d+))"
let build_answer predicate_kind prover_result =
let threshold =
match predicate_kind with
- | Dataset.MetaRobust f -> Float.of_string (Dataset.string_of_eps f)
+ | Dataset.MetaRobust f -> Float.of_string (Dataset.string_of_threshold f)
| _ -> failwith "Unsupported property"
in
match prover_result.Call_provers.pr_answer with
diff --git a/src/JSON.ml b/src/JSON.ml
index 26b9a7c..502f4be 100644
--- a/src/JSON.ml
+++ b/src/JSON.ml
@@ -120,7 +120,7 @@ let theory_of_input env input =
in
let t_eps = Dataset.term_of_eps env eps in
Term.t_app_infer ls_robust [ t_model; t_dataset; t_eps ]
- | CondRobust _ -> invalid_arg "Not yet supported property"
+ | CondRobust _ | MetaRobust _ -> invalid_arg "Not yet supported property"
in
let prsymbol = Decl.create_prsymbol (Ident.id_fresh "property") in
Theory.add_prop_decl th_uc Decl.Pgoal prsymbol t_property
diff --git a/src/SAVer.ml b/src/SAVer.ml
index f5347ec..40511c6 100644
--- a/src/SAVer.ml
+++ b/src/SAVer.ml
@@ -74,12 +74,14 @@ let re_group_number_of_predicate = function
| Dataset.Correct -> 2
| Robust _ -> 3
| CondRobust _ -> 4
+ | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"
let negative_answer = function
| Dataset.Correct ->
(* SAVer is complete wrt [Correct] predicate. *)
Call_provers.Invalid
| Robust _ | CondRobust _ -> Call_provers.Unknown ""
+ | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"
let build_answer predicate_kind prover_result =
match prover_result.Call_provers.pr_answer with
@@ -114,6 +116,7 @@ let call_prover limit config config_prover predicate =
match predicate.property with
| Dataset.Correct -> None
| Robust e | CondRobust e -> Some e
+ | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"
in
build_command config_prover svm dataset eps
in
diff --git a/src/dataset.ml b/src/dataset.ml
index e46e698..5221dd9 100644
--- a/src/dataset.ml
+++ b/src/dataset.ml
@@ -49,10 +49,15 @@ let term_of_eps env eps =
let ty = Ty.ty_app (Theory.ns_find_ts th.th_export [ "t" ]) [] in
Term.t_const (real_constant_of_float eps) ty
+type threshold = float [@@deriving yojson, show]
+
+let string_of_threshold threshold = Float.to_string threshold
+
type property =
| Correct
| Robust of eps
| CondRobust of eps
+ | MetaRobust of threshold
[@@deriving yojson, show]
type ('a, 'b) predicate = {
@@ -65,6 +70,7 @@ let string_of_predicate_kind = function
| Correct -> "correct"
| Robust _ -> "robust"
| CondRobust _ -> "condrobust"
+ | MetaRobust _ -> "meta_robust"
let find_predicate_ls env p =
let th = Pmodule.read_module env [ "caisar" ] "DatasetClassificationProps" in
@@ -95,11 +101,14 @@ let interpret_predicate env ~on_model ~on_dataset task =
| [ { t_node = Tconst (Constant.ConstReal e); _ } ] ->
let robust_predicate = find_predicate_ls env "robust" in
let cond_robust_predicate = find_predicate_ls env "cond_robust" in
+ let meta_robust_predicate = find_predicate_ls env "meta_robust" in
let f = float_of_real_constant e in
if Term.ls_equal ls robust_predicate
then Robust f
else if Term.ls_equal ls cond_robust_predicate
then CondRobust f
+ else if Term.ls_equal ls meta_robust_predicate
+ then MetaRobust f
else failwith_unsupported_ls ls
| _ -> failwith_unsupported_term term
in
@@ -150,6 +159,7 @@ let add_input_decls predicate_kind ~inputs ~record th task =
| Correct -> None
| Robust eps -> Some (string_of_eps eps)
| CondRobust _ -> failwith "Unsupported conditional robustness predicate"
+ | MetaRobust _ -> failwith "Unsupported metamorphic robustness predicate"
in
List.fold2_exn inputs features ~init:task ~f:(add_axioms ?eps th)
diff --git a/src/dataset.mli b/src/dataset.mli
index ef90caf..a9fcef6 100644
--- a/src/dataset.mli
+++ b/src/dataset.mli
@@ -27,10 +27,15 @@ type eps [@@deriving yojson, show]
val string_of_eps : eps -> string
val term_of_eps : Env.env -> eps -> Term.term
+type threshold [@@deriving yojson, show]
+
+val string_of_threshold : threshold -> string
+
type property = private
| Correct
| Robust of eps
| CondRobust of eps
+ | MetaRobust of threshold
[@@deriving yojson, show]
type ('model, 'dataset) predicate = private {
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 8842266..aeea709 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -68,6 +68,8 @@ theory DatasetClassificationProps
predicate cond_robust (m: model) (d: dataset) (eps: t) =
correct m d /\ robust m d eps
+
+ predicate meta_robust (m: model) (d: dataset) (threshold: t)
end
theory NN
--
GitLab