v2: Shai

[fbrausse]

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 fb3ca2a:

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: Generalize .spec to allow optimization over stability radii #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.