The redesign of the v2 API constitutes a new approach and basically no code is in place/tested yet, that was used to solve Shai's previous instances. These are the options from the v1 solver src/prove-nn.py as of fb3ca2a0065721e93555b7fc6fb7f19384f879fd:
usage: src/prove-nn.py [-h] [-b [BOUNDS]] [-B DBOUNDS] [-C CHECK_SAFE] [-d DATA] [-D DELTA] -g MODEL_GEN [-G GRID] [-n N] [-N] [-o OUTPUT] [-O OBJECTIVE] [-P PARTIAL_GRID]
[-r RESPONSE_BOUNDS] -s SPEC [-S SAFE] [-t THRESHOLD] [-T SAFE_THRESHOLD] [-U CENTER_OFFSET] [-v] [-x TRACE] [-X] [-z BO_CEX] [-Z BO_CAD]
NN_MODEL
positional arguments:
NN_MODEL Path to NN model in .h5 format
optional arguments:
-h, --help show this help message and exit
-b [BOUNDS], --bounds [BOUNDS]
bound variables [default: none; otherwise, if BOUNDS is missing, 0]
-B DBOUNDS, --data-bounds DBOUNDS
path to data_bounds file to amend the bounds determined from SPEC
-C CHECK_SAFE, --check-safe CHECK_SAFE
Number of random samples to check for each SAFE config found [default: 0]
-d DATA, --data DATA path to DATA.csv; check DATA for counter-examples to found regions
-D DELTA, --delta DELTA
exclude (1+DELTA)*radius region for non-grid components
-g MODEL_GEN, --model-gen MODEL_GEN
the model_gen*.json file containing the training / preprocessing parameters
-G GRID, --grid GRID Path to grid.istar file
-n N number of safe regions to generate in total (that is, including those already in SAFE) [default: 1]
-N, --no-exists only check GRID, no solving of existential part
-o OUTPUT, --output OUTPUT
Path to output .smt2 instance [default: none]
-O OBJECTIVE, --objective OBJECTIVE
Objective function in terms of labelled outputs [default: "delta"]
-P PARTIAL_GRID, --partial-grid PARTIAL_GRID
Path to partial grid CSV
-r RESPONSE_BOUNDS, --response-bounds RESPONSE_BOUNDS
Path to bounds.csv for response bounds to interpret T and ST in [default: use DATA_BOUNDS]
-s SPEC, --spec SPEC Path to JSON spec of input features
-S SAFE, --safe SAFE Path to output found safe configurations to as CSV
-t THRESHOLD, --threshold THRESHOLD
Threshold to restrict output feature to be larger-equal than [default: search in 0.05 grid between 0 and 0.95]
-T SAFE_THRESHOLD, --safe_threshold SAFE_THRESHOLD
Center threshold [default: THRESHOLD+SAFE_OFFSET]. Overrides any SAFE_OFFSET.
-U CENTER_OFFSET, --center_offset CENTER_OFFSET
Center threshold offset of threshold [default: 0]
-v, --verbose Increase verbosity
-x TRACE, --trace-exclude TRACE
exclude all unsafe i* from trace file
-X, --trace-exclude-safe
exclude also found safe i* from the trace file
-z BO_CEX, --bo-cex BO_CEX
use BO_CEX >= 10 iterations of BO to find counter-examples [default: no]
-Z BO_CAD, --bo-cad BO_CAD
use BO_CAD iterations of BO to find a candidate prior to falling back to Z3 [default: no]
For the latest runs, the following were required and, in addition to Pareto, probably are for v2 as well:
[ ] -s SPEC: related: #4
[ ] -b, -B DBOUNDS: bounds on variables from the dataset
[ ] -r RESPONSE_BOUNDS: bounds on objectives shared across a channel
[ ] -d DATA
[ ] -g MODEL_GEN: which normalizations to apply to which features for evaluating the NN / encoding it into constraints
[ ] -t THRESHOLD: list of thresholds to search, e.g., [0.00,0.05,0.10,0.15,0.20,0.25,0.30,0.35,0.40,0.45,0.50,0.55,0.60,0.65,0.70,0.75,0.80,0.85,0.90,0.95]
[ ] -x TRACE: record/re-use previous solutions in a structured manner
These should be implemented in some suitable manner (reusing existing code if possible, obviously) ontop of the v2 API.
The redesign of the v2 API constitutes a new approach and basically no code is in place/tested yet, that was used to solve Shai's previous instances. These are the options from the v1 solver
src/prove-nn.pyas of fb3ca2a0065721e93555b7fc6fb7f19384f879fd:For the latest runs, the following were required and, in addition to Pareto, probably are for v2 as well:
-s SPEC: related: #4-b,-B DBOUNDS: bounds on variables from the dataset-r RESPONSE_BOUNDS: bounds on objectives shared across a channel-d DATA-g MODEL_GEN: which normalizations to apply to which features for evaluating the NN / encoding it into constraints-t THRESHOLD: list of thresholds to search, e.g.,[0.00,0.05,0.10,0.15,0.20,0.25,0.30,0.35,0.40,0.45,0.50,0.55,0.60,0.65,0.70,0.75,0.80,0.85,0.90,0.95]-x TRACE: record/re-use previous solutions in a structured mannerThese should be implemented in some suitable manner (reusing existing code if possible, obviously) ontop of the v2 API.