From 293ef4dbeb6c1587e071cc64017aaa7998f7e0bc Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Fri, 2 Jun 2023 10:57:16 +0200
Subject: [PATCH] [config] Add first support for abcrown config files.
---
config/abcrown/acasxu.yaml | 27 +++++++++++++++++++++++++++
config/caisar-detection-data.conf | 11 +++++++++++
config/dune | 3 ++-
src/verification.ml | 3 +++
tests/autodetect.t | 4 +++-
5 files changed, 46 insertions(+), 2 deletions(-)
create mode 100644 config/abcrown/acasxu.yaml
diff --git a/config/abcrown/acasxu.yaml b/config/abcrown/acasxu.yaml
new file mode 100644
index 0000000..22d1141
--- /dev/null
+++ b/config/abcrown/acasxu.yaml
@@ -0,0 +1,27 @@
+# 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
diff --git a/config/caisar-detection-data.conf b/config/caisar-detection-data.conf
index 47825ee..b762961 100644
--- a/config/caisar-detection-data.conf
+++ b/config/caisar-detection-data.conf
@@ -108,6 +108,17 @@ command = "%e --device cpu --onnx_path %{nnet-onnx} --vnnlib_path %f --timeout %
driver = "caisar_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 = "caisar_drivers/abcrown.drv"
+use_at_auto_level = 1
+
[ATP saver]
name = "SAVer"
exec = "saver"
diff --git a/config/dune b/config/dune
index 3bf2582..5401292 100644
--- a/config/dune
+++ b/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)
diff --git a/src/verification.ml b/src/verification.ml
index ce6f2f7..f7c4914 100644
--- a/src/verification.ml
+++ b/src/verification.ml
@@ -150,6 +150,8 @@ let answer_aimos limit config env config_prover dataset task =
(answer, additional_info)
let nnet_or_onnx = Re__Core.(compile (str "%{nnet-onnx}"))
+let config_re = Re__Core.(compile (str "%{config}"))
+let config_site = List.hd_exn Dirs.Sites.config
let call_prover_on_task limit config command driver task =
let prover_call =
@@ -247,6 +249,7 @@ let answer_generic limit config prover config_prover driver ~proof_strategy task
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 = Re__Core.replace_string config_re ~by:config_site command in
List.map tasks ~f:(call_prover_on_task limit config command driver))
in
let prover_answer = combine_prover_answers answers in
diff --git a/tests/autodetect.t b/tests/autodetect.t
index 6c4a2f4..cd2e8ef 100644
--- a/tests/autodetect.t
+++ b/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
--
GitLab