CHANGES:
- [interpretation] Add transformations that allow the verification of several
neural network at once. Within particular patterns, CAISAR will generate
an ONNX file that preserve the semantic of the neural networks
while encapsulating parts of the
specification directly in the control flow of the neural network.
This feature allow the verification of properties with multiple neural
networks, including their composition.
- [interpretation] 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.
- [interpretation] Add support for addition between vectors.
- [interpretation] Add better error reporting for interpretation errors. Users
now get better guidance on how to write their specification. For instance,
CAISAR now explicitly asks for a predicate constraining the length of a vector
after a universal quantifier.
- [language] Unified Support Vector Machines (SVMs) theories.
Previously, there was a separate theory for neural networks and SVMs datasets
and models. They are now accessible under a single theory.
- [language] Add additional abstraction support for SVMs.
- [language] Simplify CAISAR Neural Intermediate Representation (NIR) and
perform automatic shape inference when creating a new NIR node.
- [language] Add support for the following ONNX operators: Gather, Log, Abs,
RandomNormal, ReduceSum.
- [language] Neural networks in NNet format are now parsed into a NIR.
- [examples] Rework ACAS-Xu specification with a formulation that is closer to
the original. In particular, provide explicit normalization and
denormalization functions in the test file. Also define explicit function
contracts using Why3 pre and post-conditions.
- [examples] Add more examples displaying CAISAR ability to handle several
neural networks at once.
- [cmdline] Add command line option --onnx-out-dir
to output the NIR generated by CAISAR as an ONNX file.
- [logging] Add command line option --ltag for fine-grained logging.
By providing a logging tag (ltag), users can control which part of CAISAR
will log its outputs.
- [prover] Add support for Marabou 2.0 via its Python API. Autodetection of
Marabou installed through maraboupy is now supported.
- [prover] Update AIMOS configuration to match upstream.
- [prover] Update $\alpha-\beta-$CROWN configuration to match upstream.
- [doc] Clarify the supported ONNX operator set: the ONNX Intermediate
Representation is version 8, the supported operator set is version 13.