The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification
Fuente:
arXiv
Guardado en:
| Autores principales: | , , , , , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2025
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866917210651361280 |
|---|---|
| author | Alberti, Michele Bobot, François Girard-Satabin, Julien Grastien, Alban Varasse, Aymeric Chihani, Zakaria |
| author_facet | Alberti, Michele Bobot, François Girard-Satabin, Julien Grastien, Alban Varasse, Aymeric Chihani, Zakaria |
| contents | 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 |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_12084 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification Alberti, Michele Bobot, François Girard-Satabin, Julien Grastien, Alban Varasse, Aymeric Chihani, Zakaria Software Engineering Artificial Intelligence Computation and Language Formal Languages and Automata Theory Neural and Evolutionary Computing 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 |
| title | The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification |
| topic | Software Engineering Artificial Intelligence Computation and Language Formal Languages and Automata Theory Neural and Evolutionary Computing |
| url | https://arxiv.org/abs/2506.12084 |