7. Supported provers

The supported provers are the following:

7.1. PyRAT

PyRAT is a neural network prover based on abstract interpretation,

7.2. Marabou

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

7.3. SAVer

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

7.4. nnenum

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

7.5. alpha-beta-CROWN

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

7.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.