[stdlib] Add metamorphic robust predicate.

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

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

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

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)
 

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 {

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