# The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification

arXiv: https://arxiv.org/abs/2506.12084 · HTML: https://mlsanity.com/paper/2506.12084/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 21 of its 44 references that are in the map.
- First posted on arXiv 10 Jun 2025.

## Builds on (most cited first, 21 of 21)

- [XGBoost: A Scalable Tree Boosting System](https://mlsanity.com/paper/1603.02754/) (2016)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Marabou 2.0: A Versatile Formal Analyzer of Neural Networks](https://mlsanity.com/paper/2401.14461/) (2024)
- [First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)](https://mlsanity.com/paper/2301.05815/) (2023)
- [The Fifth International Verification of Neural Networks Competition (VNN-COMP 2024): Summary and Results](https://mlsanity.com/paper/2412.19985/) (2024)
- [Perfectly Parallel Fairness Certification of Neural Networks](https://mlsanity.com/paper/1912.02499/) (2019)
- [Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks](https://mlsanity.com/paper/2210.13915/) (2022)
- [The Fourth International Verification of Neural Networks Competition (VNN-COMP 2023): Summary and Results](https://mlsanity.com/paper/2312.16760/) (2023)
- [Neural Network Robustness as a Verification Property: A Principled Case Study](https://mlsanity.com/paper/2104.01396/) (2021)
- [A Review of Formal Methods applied to Machine Learning](https://mlsanity.com/paper/2104.02466/) (2021)
- [VeriX: Towards Verified Explainability of Deep Neural Networks](https://mlsanity.com/paper/2212.01051/) (2022)
- [Neuro-Symbolic Verification of Deep Neural Networks](https://mlsanity.com/paper/2203.00938/) (2022)
- [Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs](https://mlsanity.com/paper/2401.06379/) (2024)
- [Neural Network Verification is a Programming Language Challenge](https://mlsanity.com/paper/2501.05867/) (2025)
- [Lipschitz Properties for Deep Convolutional Networks](https://mlsanity.com/paper/1701.05217/) (2017)
- [Robustness Verification of Support Vector Machines](https://mlsanity.com/paper/1904.11803/) (2019)
- [CAISAR: A platform for Characterizing Artificial Intelligence Safety and Robustness](https://mlsanity.com/paper/2206.03044/) (2022)
- [Verifying Global Two-Safety Properties in Neural Networks with Confidence](https://mlsanity.com/paper/2405.14400/) (2024)
- [Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers](https://mlsanity.com/paper/2202.05207/) (2022)
- [A Deductive Verification Framework for Circuit-building Quantum Programs](https://mlsanity.com/paper/2003.05841/) (2020)
- [CAMUS: A Framework to Build Formal Specifications for Deep Perception Systems Using Simulators](https://mlsanity.com/paper/1911.10735/) (2019)

## Abstract (arXiv)

The formal specification and verification of machine learning programs saw remarkable progress in less than a decade, leading to a profusion of tools. However, diversity may lead to fragmentation, resulting in tools that are difficult to compare, except for very specific benchmarks. Furthermore, this progress is heavily geared towards the specification and verification of a certain class of property, that is, local robustness properties. But while provers are becoming more and more efficient at solving local robustness properties, even slightly more complex properties, involving multiple neural networks for example, cannot be expressed in the input languages of winners of the International Competition of Verification of Neural Networks VNN-Comp. In this tool paper, we present CAISAR, an open-source platform dedicated to machine learning specification and verification. We present its specification language, suitable for modelling complex properties on neural networks, support vector machines and boosted trees. We show on concrete use-cases how specifications written in this language are automatically translated to queries to state-of-the-art provers, notably by using automated graph editing techniques, making it possible to use their off-the-shelf versions. The artifact to reproduce the paper claims is available at the following DOI: https://doi.org/10.5281/zenodo.15209510