We are happy to announce the release of CAISAR 0.2, to celebrate (with one week delay) 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. You may check our website for additional infos.
We added the support of several provers:
- the alpha-beta-CROWNprover; winner of the 2021 and 2022 edition of the VNN-COMP
- the nnenumhttps://github.com/stanleybak/nnenum) prover
- the AIMOS metamorphic testing prover, for now internally developped at CEA
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 our 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.
We are also looking for fixed-term positions, intern and PhD students to work on CAISAR, check our website or the ocaml job board for more infos.