package caisar

You can search for identifiers within the package.

in-package search v0.2.0

A platform for characterizing the safety and robustness of artificial intelligence based software

Install

sha256=cd24b647565aaa4bb82d46c195c692d56ba0ad4b39bc86ef6baaf2d7a08c92a5

sha512=073761d95d6d8f6eb6f687643054297eb47db5d5bdc3a72ba42bf1509ab76415d485f536e5e42c11bd59c972ab7ad72e398d19af6e74c4f0778f28ef5bf4935e

[language] Extended WhyML for AI systems. It is now possible to model with CAISAR computations on vectors, datasets and the application of machine learning programs. Added an interpretation engine that allow direct evaluation on some predicates and functions related to those extensions.
[doc] Update the documentation to cover the new interpretation language. Add contribution guide.
[cmdline] Add command line option --goal (or, -g) to verify only the provided list of goals, either from all theories or from the specified ones.
[cmdline] Add command line option --theory (or, -T) to verify only the provided list of theories (ie, all their goals).
[cmdline] Add command line option --define (or -D) to define the value of a declared constant in any specification file to verify.
[build] Make CAISAR available as a Nix Flake.
[prover] Better integration of the AIMOS metamorphic testing prover.
[docker] Add the $\alpha-\beta-$CROWN prover to the docker image.

[packaging] Simplify CAISAR packaging structure by merging onnx, ovo, csv and onnx libraries into the main repo.

[prover] Integration of the nnenum prover.
[prover] Integration of the $\alpha-\beta-$CROWN prover.
[prover] Integration of the AIMOS metamorphic testing prover.
[prover] Add printer for VNN-LIB format for property specification as supported by nnenum and $\alpha-\beta-$CROWN provers.
[prover] Support for multiple configurations of provers, using the prover-altern command line option. An example of registering an alternate configuration is available under config/caisar-detection.conf
[prover] Add transformation to translate ONNX format into SMTLIB format for allowing SMTLIB2 compliant provers to work on neural networks.
[doc] The first version of the CAISAR manual is publicly available on our website. It includes detailed installation instructions, examples on the ACAS-Xu and MNIST local robustness benchmarks. Those examples use an experimental interpretation language that is not fully documented yet.
[deps] Upgraded Why3 to 1.6.0 version.
Add verify-json command for verifying a robustness property via a JSON configuration file.
Add verification of datasets for classification tasks in terms of a specific CSV format: each line provides the label in 1st column, and data features in the other columns.
Add support for memory and time limits.
Add debug logging options.