On the occasion of the 34th birthday of the abolition of the apartheid laws, we are honoured to release CAISAR version 2.0.
The release source is available at our public forge. As our last releases, CAISAR will soon be available on opam and on Dockerhub.
A nix flake is available for building CAISAR directly in the repository. Try CAISAR with nix build git+https://git.frama-c.com/pub/caisar !
Here are the prominent features for this 2.0 release:
Specification and verification of several neural networks at once
CAISAR specification language already allowed to write specifications that involved several neural networks at once. However, translating such specifications to actual prover queries was not possible. We added automated graph editing techniques to allow such verification to take place. Within particular patterns, CAISAR will generate an ONNX file that preserve the semantic of the different neural networks while encapsulating parts of the specification directly in the control flow of the new neural network. This feature allow the verification of properties with multiple neural networks, including their composition.
This is quite a step forward, as it enables machine-learning dedicated verifiers to tackle a much wider range of properties.
SVM as first-class citizens for interpretation
CAISAR now fully 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.
We also unified the theory of machine learning models. Now, SVMs and neural networks can be specified with only the model type. In the near future, SVMs will be parsed directly into CAISAR’s Neural Intermediate Representations, which will simplify the verification of systems with heterogeneous AI components.