On the occasion of the 149th birthday of the first commercial telephone service and the 129th birthday of Jean Moulin’s birth, we are happy to release CAISAR version 4.0.
We further take the opportunity to celebrate the pride month. The rise of facism that threatens queer people also constitues a menace for science, as recent events showed. We want to reaffirm that LGBTQ+ will always be welcome within our team.
The release source is available at our public forge. As our last releases, CAISAR will soon be available on opam. We are temporarily dropping support for Docker releases as we are aiming to reduce the Docker image size. A release of CAISAR bundling some supported solvers is available under the Nix installation method.
This release provided the following enhancements
Quantized neural networks are often deployed on-edge devices for their low energy consumption. They are usually obtained through quantization from an already existing neural network. One may want to check whether this process preserves the performance of the original model.
CAISAR added support for experimental quantized operators in ONNX, allowing to write specifications including quantized neural networks. Current work with some specialized provers is undergoing to allow the formal verification of quantized neural networks.
Previously, CAISAR relied on a separate pipeline to handle SVMs. This limited severely the applicability of other provers. With this release, CAISAR unified SVM representation under its Neural Intermediate Representation (NIR), allowing to verify a specification including a SVM with any solver supported by CAISAR (including PyRAT).
As to increase useability, it is crucial for CAISAR to be able to communicate with the external world, without requiring users to install and configure CAISAR locally. This release provides a first step: by providing a JSON API for verification queries. This permits for CAISAR to receive verification queries from any source and emits verification results.