CAISAR 2.0 released

On the occasion of the 34th birthday of the abolition of apartheid laws in South Africa, 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.

Here are some of the most prominent features we added.

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.

More formally, suppose that you have two neural networks \(nn_1\) and \(nn_2\) with 1 (resp. 2) inputs, and one output, and let \(H\) be a formula that defines bounds to said inputs. Let us consider a computation where \(nn_2\) takes a linear combination of \(nn_1\) evaluations with different inputs, for instance \(nn_2 \circ (nn_1 (x_1), x_1 + \varepsilon) + nn_1(x_0)\).

The specification is thus the following:

\[S: \forall x_0,x_1,\epsilon. H(x_0,x_1,\epsilon) \implies nn_2@@(nn_1@@(x_1),x_1+\epsilon) + nn_1@@(x_0) > 0\]

CAISAR is now able to create a new neural network, \(nn_3\), that performs the computations of the previous formula, and edit \(S\) to obtain the following:

\[S^{'}: \forall x_0,x_1,\epsilon. H(x_0,x_1,\epsilon) \implies nn_3@@(x_0,x_1,\epsilon) > 0\]

This represents a vast improvement in CAISAR’s ability to handle complex properties. We hope that the community of neural network verifiers will soon tackle the new properties CAISAR made possible to express.

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.