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

翻译：机器学习程序的形式化规约与验证在不到十年间取得了显著进展，催生了大量工具。然而，多样性可能导致碎片化，使得工具难以相互比较，仅能在特定基准测试中进行评估。此外，当前进展主要集中于某类特定性质的规约与验证，即局部鲁棒性性质。尽管证明器在解决局部鲁棒性性质方面效率日益提升，但即使涉及多个神经网络等稍复杂的性质，也无法在国际神经网络验证竞赛VNN-Comp优胜工具的输入语言中表达。本文作为工具论文，介绍专用于机器学习规约与验证的开源平台CAISAR。我们阐述其规约语言，该语言适用于对神经网络、支持向量机和提升树等模型建立复杂性质规约。通过具体用例，展示如何通过自动化图编辑技术将该语言编写的规约自动转换为对前沿证明器的查询，从而直接使用其现成版本。重现论文声明的实验材料可通过以下DOI获取：https://doi.org/10.5281/zenodo.15209510