5. Supported provers

The supported provers are the following:

5.1. PyRAT

PyRAT is a neural network prover based on abstract interpretation,

5.2. Marabou

Marabou is a Satisfiability Modulo Theory (SMT) solver specialized in neural network verification.

5.3. SAVer

SAVer is a support vector machine prover based on abstract interpretation.

5.4. nnenum

nnenum is a neural network prover that combines abstract interpretation, linear programming techniques and input split heuristics.

5.5. alpha-beta-CROWN

alpha-beta-CROWN is a neural network prover, winner of the VNN-COMP 2021 and 2022.

5.6. SMT solvers

Standard SAT/SMT solvers that support the SMT-LIBv2 input language. As of now, only cvc5 had been tested.

Warning

Marabou and VNN-LIB provers (nnenum, alpha-beta-CROWN) do not accept strict inequalities. Thus CAISAR treats strict inequalities as non-strict ones. We are aware that this is not correct in general, but it is the current common practice in the community.

5.7. Adapting neural networks for provers

Provers only support a limited set of ONNX operators. It often happens that a verification query cannot be processed by the prover, because the neural network contains unsupported operators.

CAISAR offers a way to circumvent this by replacing some operators by others. This is done by specifying a transformation to apply in the prover driver. See Transformations in CAISAR for more details.