# 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.