AI robustness and safety characterization software

AIs cannot be integrated into mission-critical systems without a high level of trust in their safety. Formal verification techniques can be used to provide this trust. Because AIs manipulate large amounts of data in different formats (images, sounds, text), formal methods can be difficult to apply. Another issue is that AIs are built on probabilistic algorithms, resulting in program structures that conventional verification tools cannot effectively address.

CAISAR overcomes these challenges by:

• Enabling a high degree of expressiveness so that the complex specifications of AIs can be translated into verifiable formal properties.
• Using state-of-the-art provers designed specifically for AIs for a scalable verification solution.
• Delivering explainable results.

CEA-List has developed a specification language for CAISAR that allows the necessary modeling flexibility.

A complete user guide and tutorials are available on the CAISAR website. Documentation is available on two CAISAR use cases. The first is for ACAS-Xu, an aircraft anti-collision system (proof of functional properties); the second is for the MNIST (Mixed National Institute of Standards and Technology) handwritten digit database (verification of the robustness of classifiers to visual interference).

CAISAR is constantly being developed and improved upon to respond to increasingly complex and real-world use cases. Moving forward, our researchers will tackle the very real challenges of specifying and verifying heterogeneous artificial intelligence models (neural networks, support vector machines, etc.). This will require the provers in CAISAR to work together, which will represent a major milestone in the formal verification of AI.

Learn more :

• The technology in use : CAISAR was developed as part of the Confiance.ai program on trusted AI. So far it has been deployed in the two use cases mentioned above, plus a weld inspection use case at car maker Renault. It is available under an LGPLv2 open source license.
• Major projects : This research is being leveraged for the DeepGreen program led by CEA, where it will be applied to embedded neural networks. CAISAR already has users at Dortmund Technical University and LAIV (Lab for AI Verification) at the University of Edinburgh.
• Flagship publications : CAISAR has been presented at national and international conferences in the field (such as the IJCAI AISafety workshop).