3. Using CAISAR

3.1. Commands summary

The CAISAR executable provide several subcommands, called using caisar [COMMAND]. caisar --help provides a list of all available commands. Additionally, caisar [COMMAND] --help gives a synopsis for each available command.

3.2. Command line options

caisar verify have the following specific command line options:

  • -D name:value or --define=name:value: define a declared constant name with the given value value. Constant must be declared in the theory file.

  • --dataset=FILE: Path of a dataset file. To be deprecated.

  • -g [theory]:goal,..,goal or --goal [theory]:goal,...,goal: Verify only the goal in the theory. Theory must already be defined in the specification file. When no theory is provided, verify the specified goals for all theories.

  • -T theory or --theory=theory: Verify all goals in theory.

  • -m MEM or --memlimit=MEM: Memory limit. MEM is intended in megabytes (MB); (GB) and (TB) can also be specified. Default: 4000MB.

  • -t TIME or --timelimit=TIME: Time limit. TIME is intended in seconds (s); minutes (m) and hours (h) can also be specified. (MB), (GB) and (TB) can also be specified. Default: 20s.

  • -p PROVER or --prover=PROVER. Prover to use. Support is provided for the following: Marabou, PyRAT, SAVer, AIMOS, CVC5, nnenum, alpha-beta-CROWN. See Supported provers for a detailed description of each prover capacity.

  • --prover-altern=VAL: alternative prover alternatives to use. Prover alternatives are prover-specific configurations that help provers to better perform on specific problems. Supported prover alternative are ACAS for alpha-beta-CROWN and PyRAT.

3.2.1. Logging

CAISAR provides different log verbosity levels. To change the log verbosity level, provide the option --verbosity to the verify command. Available levels are quiet, error, warning, info and debug (defaults to warning).

CAISAR also provides log tags. Each tag adds additional information in the log, independently of the log verbosity level. However, note that the debug verbosity level allows logging with all tags enabled. To enable a particular tag, use the option --ltag=TAG, with TAG one of the following:

  • Autodetect: display the output of the autodetect routine of CAISAR described in Prover registration

  • ProverSpec: display the actual specification provided to the prover

  • ProverCall: display the actual command used to call the prover

  • InterpretGoal: display the goal interpretation

  • StackTrace: display the stack trace upon a CAISAR error

3.3. Prover registration

CAISAR relies on external provers to work. You must install them first, then point CAISAR to their location. Please refer to each prover documentation to install them.

CAISAR already supports several provers, listed in Supported provers. Assuming you have installed a prover with an entry in the caisar-detection.conf file, you can register the prover to CAISAR using the following command: PATH=$PATH:/path/to/solver/executable caisar config -d. Your prover should be displayed with its relevant version.

3.4. Property verification

A prominent use case of CAISAR is to model a specification for an artificial intelligence system, and to verify its validity for a given system.

The modelling uses WhyML, a typed first-order logic language. Example of WhyML are in the source code. You may also read the CAISAR by Examples section of this documentation to get a first grasp on using WhyML.

Provided a file trust.why containing a goal to verify, the command caisar verify --prover=PROVER trust.why will verify the goals using the specified prover. A list of supported provers is available in Supported provers. The prover must already be registered by CAISAR. Currently, only one prover can be selected at a time; future work will allow selecting multiple provers and orchestrate verification strategies. Internally, CAISAR will translate the goals into a form that is acceptable by the targeted prover, generating a file (the %f defined in the previous section).

3.5. Built-in properties

In addition to all the theories provided by Why3, CAISAR provide additional theories that model commonly desirable properties for machine learning programs. All those predicates are located in the file stdlib/caisar.mlw. Among them are theories to describe classification datasets, local and global robustness around a neighborhood.

3.6. Advanced usage: registering a new prover

Provers tend to be complex programs with multiple options. Some combination of options may be suited for one verification problem, while inefficient for another. As they also have different interface, it is also necessary to register their call in a way CAISAR can understand.

3.6.1. Registering for autodetection

The first step is to register provers inside the config/caisar-detection-data.conf file. Each supported prover is registered by specifying the following fields:

  • name: the name under which CAISAR will know the prover

  • exec: the prover’s executable name

  • alternative (optional): an alternative configuration for the prover. To use it with CAISAR, use the option --prover-altern. Useful when you want to use the same prover on different problems.

  • version_switch: the command used to output the prover’s version

  • version_regexp: a regular expression parsing the output of version_switch

  • version_ok: CAISAR supported version of the prover. Provers should only be used with their supported version.

  • command: the actual command CAISAR will send to the prover executable. There are a few builtin expressions provided by CAISAR:

    • %f: the generated property file sent to the prover

    • %t: the timelimit value

    • %{nnet-onnx}: the name of the neural network file

  • driver: location of the CAISAR driver for the prover, if any

3.6.2. Building the specification for the prover

It is necessary to convert the WhyML specification into an input that is understandable by the prover. CAISAR provide built-in translation from WhyML to the VNN-Lib and SMTLIB2 specification input formats. If your prover support those abovementioned input formats, adding support to your prover requires adding it in the files src/provers.ml, src/provers.mli and the function call_prover in src/verification.ml. For other input formats, it is necessary to write custom OCaml code in the src/printers/ folder as well.

3.6.3. Parsing the output of the prover

CAISAR rely on Why3’s drivers to parse the output of the prover.

If you add support for a new prover, consider opening a merge request on our forge!