Merge branch 'feature/michele/abcrown-config' into 'master'

Support alpha-beta-CROWN configuration files

See merge request laiser/caisar!88

config/abcrown/acasxu.yaml

+# Configuration file for running the ACASXu benchmark (all properties).
+general:
+  enable_incomplete_verification: False
+  loss_reduction_func: max
+data:
+  num_outputs: 5
+solver:
+  batch_size: 1000  # Number of parallel domains to compute on GPU.
+  bound_prop_method: crown
+  beta-crown:
+    iteration: 10  # Iterations for computing intermediate layer bounds.
+  alpha-crown:
+    iteration: 10
+    share_slopes: True  # This produces slightly looser bounds, but faster.
+bab:
+  branching:
+    method: naive  # Split on input space.
+    candidates: 3
+    sb_coeff_thresh: 0.01
+    input_split:
+      enable: True
+      enhanced_bound_prop_method: alpha-crown
+      enhanced_bound_patience: 20
+      enhanced_branching_method: sb
+      attack_patience: 80
+attack:
+  pgd_order: after

config/caisar-detection-data.conf

@@ -50,7 +50,7 @@ version_switch = "--version"
 version_regexp = "\\([0-9.+]+\\)"
 version_ok  = "1.0.+"
 command = "%e %{nnet-onnx} %f --timeout %t --snc --initial-divides=4 --num-online-divides=4 --initial-timeout=0"
-driver = "caisar_drivers/marabou.drv"
+driver = "%{config}/drivers/marabou.drv"
 use_at_auto_level = 1
 
 [ATP pyrat]
@@ -61,7 +61,7 @@ version_switch = "--version"
 version_regexp = "PyRAT \\([0-9.]+\\)"
 version_ok  = "1.1"
 command = "%e -mp %{nnet-onnx} -pp %f --timeout %t"
-driver = "caisar_drivers/pyrat.drv"
+driver = "%{config}/drivers/pyrat.drv"
 use_at_auto_level = 1
 
 [ATP pyrat-vnnlib]
@@ -73,7 +73,7 @@ version_switch = "--version"
 version_regexp = "PyRAT \\([0-9.]+\\)"
 version_ok  = "1.1"
 command = "%e -mp %{nnet-onnx} -pp %f --timeout %t --domain zono poly --split"
-driver = "caisar_drivers/pyrat_vnnlib.drv"
+driver = "%{config}/drivers/pyrat_vnnlib.drv"
 use_at_auto_level = 1
 
 [ATP pyrat-acas]
@@ -85,7 +85,7 @@ version_switch = "--version"
 version_regexp = "PyRAT \\([0-9.]+\\)"
 version_ok  = "1.1"
 command = "%e -mp %{nnet-onnx} -pp %f --timeout %t --domain zono --split --scorer coef"
-driver = "caisar_drivers/pyrat.drv"
+driver = "%{config}/drivers/pyrat.drv"
 use_at_auto_level = 1
 
 [ATP nnenum]
@@ -95,7 +95,7 @@ version_switch = "--version"
 version_regexp = "\\(dummy-version\\)"
 version_ok  = "dummy-version"
 command = "%e %{nnet-onnx} %f"
-driver = "caisar_drivers/nnenum.drv"
+driver = "%{config}/drivers/nnenum.drv"
 use_at_auto_level = 1
 
 [ATP abcrown]
@@ -105,7 +105,18 @@ version_switch = "--version"
 version_regexp = "\\(dummy-version\\)"
 version_ok  = "dummy-version"
 command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --timeout %t"
-driver = "caisar_drivers/abcrown.drv"
+driver = "%{config}/drivers/abcrown.drv"
+use_at_auto_level = 1
+
+[ATP abcrown]
+name = "alpha-beta-CROWN"
+alternative = "ACAS"
+exec = "abcrown.sh"
+version_switch = "--version"
+version_regexp = "\\(dummy-version\\)"
+version_ok  = "dummy-version"
+command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --config %{config}/abcrown/acasxu.yaml --timeout %t"
+driver = "%{config}/drivers/abcrown.drv"
 use_at_auto_level = 1
 
 [ATP saver]
@@ -115,7 +126,7 @@ version_switch = "--version 2>&1 | head -n1 && (which saver > /dev/null 2>&1)"
 version_regexp = "\\(v[0-9.]+\\)"
 version_ok = "v1.0"
 command = "%e %{svm} %{dataset} %{abstraction} %{distance} %{epsilon}"
-driver = "caisar_drivers/saver.drv"
+driver = "%{config}/drivers/saver.drv"
 use_at_auto_level = 1
 
 [ATP aimos]
@@ -125,5 +136,5 @@ version_switch = "--version"
 version_regexp = "AIMOS \\([0-9.]+\\)"
 version_ok  = "1.0"
 command = "%e --config %{aimos_file} --no-verbose"
-driver = "caisar_drivers/aimos.drv"
+driver = "%{config}/drivers/aimos.drv"
 use_at_auto_level = 1

config/dune

@@ -3,8 +3,9 @@
   (site
    (caisar config)))
  (files
-  custom_transformations.py
   caisar-detection-data.conf
+  custom_transformations.py
+  (abcrown/acasxu.yaml as abcrown/acasxu.yaml)
   (drivers/pyrat.drv as drivers/pyrat.drv)
   (drivers/marabou.drv as drivers/marabou.drv)
   (drivers/saver.drv as drivers/saver.drv)

src/aimos.ml

@@ -23,7 +23,7 @@
 open Why3
 open Base
 
-let aimos_file = Re__Core.(compile (str "%{aimos_file}"))
+let re_aimos_file = Re__Core.(compile (str "%{aimos_file}"))
 
 let write_config inputs_path models_path perturbation perturbation_path out_mode
   amplitude =
@@ -94,7 +94,7 @@ let build_command config_prover
       amplitude
   in
   let command = Whyconf.get_complete_command ~with_steps:false config_prover in
-  Re__Core.replace_string aimos_file ~by:aimos_config command
+  Re__Core.replace_string re_aimos_file ~by:aimos_config command
 
 let re_aimos_output = Re__Pcre.regexp "((,\\s)(\\d+\\.\\d+))"
 

src/saver.ml

@@ -23,21 +23,21 @@
 open Why3
 open Base
 
-let svm = Re__Core.(compile (str "%{svm}"))
-let dataset = Re__Core.(compile (str "%{dataset}"))
-let epsilon = Re__Core.(compile (str "%{epsilon}"))
-let abstraction = Re__Core.(compile (str "%{abstraction}"))
-let distance = Re__Core.(compile (str "%{distance}"))
+let re_svm = Re__Core.(compile (str "%{svm}"))
+let re_dataset = Re__Core.(compile (str "%{dataset}"))
+let re_eps = Re__Core.(compile (str "%{epsilon}"))
+let re_abstraction = Re__Core.(compile (str "%{abstraction}"))
+let re_distance = Re__Core.(compile (str "%{distance}"))
 
 let build_command config_prover svm_filename dataset_filename eps =
   let command = Whyconf.get_complete_command ~with_steps:false config_prover in
   let params =
     [
-      (svm, Unix.realpath svm_filename);
-      (dataset, Unix.realpath dataset_filename);
-      (epsilon, Option.(value (map ~f:Dataset.string_of_eps eps)) ~default:"0");
-      (distance, "l_inf");
-      (abstraction, "hybrid");
+      (re_svm, Unix.realpath svm_filename);
+      (re_dataset, Unix.realpath dataset_filename);
+      (re_eps, Option.(value (map ~f:Dataset.string_of_eps eps)) ~default:"0");
+      (re_distance, "l_inf");
+      (re_abstraction, "hybrid");
     ]
   in
   List.fold params ~init:command ~f:(fun cmd (param, by) ->

src/verification.ml

@@ -149,7 +149,18 @@ let answer_aimos limit config env config_prover dataset task =
   let additional_info = Generic None in
   (answer, additional_info)
 
-let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
+let re_nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
+let re_config = Re__Core.(compile (str "%{config}"))
+let config_site = List.hd_exn Dirs.Sites.config
+
+let build_command config_prover ~nn_filename =
+  let command = Whyconf.get_complete_command ~with_steps:false config_prover in
+  let command =
+    Re__Core.replace_string re_nnet_or_onnx
+      ~by:(Unix.realpath nn_filename)
+      command
+  in
+  Re__Core.replace_string re_config ~by:config_site command
 
 let call_prover_on_task limit config command driver task =
   let prover_call =
@@ -191,10 +202,8 @@ let answer_dataset limit config env prover config_prover driver dataset task =
     Dataset.tasks_of_nn_csv_predicate env dataset_predicate
     |> List.map ~f:(Driver.prepare_task driver)
   in
-  let command = Whyconf.get_complete_command ~with_steps:false config_prover in
   let command =
-    let nn_file = Unix.realpath dataset_predicate.model.filename in
-    Re__Core.replace_string nnet_or_onnx ~by:nn_file command
+    build_command config_prover ~nn_filename:dataset_predicate.model.filename
   in
   let dataset_answers =
     match prover with
@@ -229,9 +238,9 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
   let answers =
     List.concat_map tasks ~f:(fun task ->
       let task = Driver.prepare_task driver task in
-      let nn_file =
+      let nn_filename =
         match Task.on_meta_excl Utils.meta_nn_filename task with
-        | Some [ MAstr nn_file ] -> Unix.realpath nn_file
+        | Some [ MAstr nn_filename ] -> nn_filename
         | Some _ -> assert false (* By construction of the meta. *)
         | None -> invalid_arg "No neural network model found in task"
       in
@@ -243,10 +252,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
         | Pyrat | Nnenum | ABCrown -> 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 command = build_command config_prover ~nn_filename in
       List.map tasks ~f:(call_prover_on_task limit config command driver))
   in
   let prover_answer = combine_prover_answers answers in
@@ -335,15 +341,13 @@ let verify ?(debug = false) ?format ~loadpath ?memlimit ?timelimit ?dataset
            altern)
   in
   let driver =
-    match String.chop_prefix ~prefix:"caisar_drivers/" config_prover.driver with
-    | None -> Driver.load_driver_for_prover main env config_prover
-    | Some file ->
-      let file =
-        Filename.concat
-          (Filename.concat (List.hd_exn Dirs.Sites.config) "drivers")
-          file
-      in
-      Driver.load_driver_file_and_extras main env file
+    Re__Core.replace_string re_config ~by:config_site config_prover.driver
+  in
+  let driver =
+    if String.equal driver config_prover.driver
+    then Driver.load_driver_for_prover main env config_prover
+    else
+      Driver.load_driver_file_and_extras main env driver
         config_prover.extra_drivers
   in
   let cwd, mstr_theory = open_file ?format env file in

tests/autodetect.t

@@ -53,9 +53,10 @@ Test autodetect
   <autodetect>Found prover PyRAT version 1.1 (alternative: ACAS)
   <autodetect>Found prover nnenum version dummy-version, OK.
   <autodetect>Found prover alpha-beta-CROWN version dummy-version, OK.
+  <autodetect>Found prover alpha-beta-CROWN version dummy-version (alternative: ACAS)
   <autodetect>Found prover SAVer version v1.0, OK.
   <autodetect>Found prover AIMOS version 1.0, OK.
-  <autodetect>10 prover(s) added
+  <autodetect>11 prover(s) added
   [caisar] AIMOS 1.0
            Alt-Ergo 2.4.0
            CVC5 1.0.2
@@ -65,4 +66,5 @@ Test autodetect
            PyRAT 1.1 (VNNLIB)
            SAVer v1.0
            alpha-beta-CROWN dummy-version
+           alpha-beta-CROWN dummy-version (ACAS)
            nnenum dummy-version