We are happy to announce the release of CAISAR 0.2, to celebrate the 234th birthday of the Serment du jeu de Paume. On this day, courageous people took a vow to abolish autocracy and fight for their rights. This release is the result of more than one year of work. Here are some of the most prominent changes that we are happy to share. The release is available under our gitlab, on opam and on Dockerhub.
We added the support of several provers:
We also added support to the VNNLib standard. In the future, adding a VNNLib compliant prover to CAISAR would only require to edit two small files, which is a huge step towards integrating more provers. This also results in supporting all solvers that support the SMTLIB2 language (which VNNLib is a subset of). We implemented a custom transformation in CAISAR that automatically translates the neural network control flow into a SMT formula. This custom transformation had been tested for the CVC5 solver.
The first version of the CAISAR manual is available under the documentation section of the website. It includes detailed installation instructions, a synopsis of common commands and two tutorials on classical benchmarks. The current version of those tutorials make use of experimental features that we plan to document in a future release. We hope this manual will provide a good entry point to CAISAR, and formal verification of machine learning programs at large.
We added various utilities to make CAISAR slicker to use, such as several logging options, verification through a JSON file, and reworked help messages.