[dependencies] Updated dependencies (Why3 and Base).
2.0 (19-06-2024)
[interpretation] Add transformations that allow the verification of several neural network at once. Within particular patterns, CAISAR will generate an ONNX file that preserve the semantic of the neural networks while encapsulating parts of the specification directly in the control flow of the neural network. This feature allow the verification of properties with multiple neural networks, including their composition.
[interpretation] Integrate SVMs into the interpretation engine. Users can expect vector computations and applications on SVMs to be computed similarly as what exists already for neural networks.
[interpretation] Add support for addition between vectors.
[interpretation] Add better error reporting for interpretation errors. Users now get better guidance on how to write their specification. For instance, CAISAR now explicitly asks for a predicate constraining the length of a vector after a universal quantifier.
[language] Unified Support Vector Machines (SVMs) theories. Previously, there was a separate theory for neural networks and SVMs datasets and models. They are now accessible under a single theory.
[language] Add additional abstraction support for SVMs.
[language] Simplify CAISAR's Neural Intermediate Representation (NIR) and perform automatic shape inference when creating a new NIR node.
[language] Add support for the following ONNX operators: Gather, Log, Abs, RandomNormal, ReduceSum.
[language] Neural networks in NNet format are now parsed into a NIR.
[examples] Rework ACAS-Xu specification with a formulation that is closer to the original. In particular, provide explicit normalization and denormalization functions in the test file. Also define explicit function contracts using Why3 pre and post-conditions.
[examples] Add more examples displaying CAISAR ability to handle several neural networks at once.
[cmdline] Add command line option --onnx-out-dir to output the NIR generated by CAISAR as an ONNX file.
[logging] Add command line option --ltag for fine-grained logging. By providing a logging tag (ltag), users can control which part of CAISAR will log its outputs.
[prover] Add support for Marabou 2.0 via its Python API. Autodetection of Marabou installed through maraboupy is now supported.
[prover] Update AIMOS configuration to match upstream.
[prover] Update \alpha-\beta-CROWN configuration to match upstream.
[doc] Clarify the supported ONNX operator set: the ONNX Intermediate Representation is version 8, the supported operator set is version 13.
1.0 (08-12-2023)
[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.
0.2.1 (19-09-2023)
[packaging] Simplify CAISAR packaging structure by merging onnx, ovo, csv and onnx libraries into the main repo.
[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.