[new release] caisar (2.0)

[caisar-platform]

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

• Project page: https://git.frama-c.com/pub/caisar
• Documentation: https://git.frama-c.com/pub/caisar

CHANGES:

• [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 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 ABCROWN 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.

[caisar-platform]

Some of the tests are failing because they require a Python3 interpreter and several packages. As they are not strictly necessary for the release, we wonder how it would be suitable to point such an optional Python3 dependency.

[avsm]

@caisar-platform I committed a dependency on "conf-python-3" {with-test}

[avsm]

The tests need py-onnx as well, so it's more than just having a python environment installed. We could just disable the tests for the purpose of opam-repo...

[mseri]

I think adding a conf-pyonnx is probably overkill in this case, and I am sure many systems will not package it or package the wrong one. In this case I think it is better just disabling the tests in the CI

[GirardR1006]

We also believe that this test is not strictly necessary for the user. In future releases, we will add additional dune specification for those tests such that they do not launch if the user's system does not find the correct python onnx package.

The specification for the testing and developing environment is indirectly specified in the manual and in the Nix flake at the root of the source project; it will be made more explicit for the next release :)

[mseri]

Thanks