CAISAR 平台：扩展机器学习规范化与验证的范围
软件工程
2026-01-21 v2 人工智能
计算与语言
形式语言与自动机理论
神经与进化计算
摘要
机器学习程序的形式化规范化与验证在不到十年的时间内取得了显著进展，催生了大量工具。然而，多样性可能导致碎片化，使得工具难以进行比较，除非针对非常特定的基准。此外，这些进展主要致力于某一类属性的规范化与验证，即局部鲁棒性属性。尽管证明器在解决局部鲁棒性属性方面日益高效，但 even 稍微复杂的属性（例如涉及多个神经网络的属性）无法在国际神经网络验证竞赛（VNN-Comp）获奖者的输入语言中表达。本工具论文中，我们提出了 CAISAR，一款专为机器学习规范化与验证而开发的开源平台。我们介绍了其规范化语言，适用于神经网络、支持向量机和提升树的复杂属性建模。我们通过具体案例展示，说明使用该语言编写的规范会自动翻译为针对最先进证明器的查询，尤其是通过自动图编辑技术，使得能够使用其即插即用版本。可复现论文实验的工件已提供以下 DOI：https://doi.org/10.5281/zenodo.15209510
引用
@article{arxiv.2506.12084,
title = {The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification},
author = {Michele Alberti and François Bobot and Julien Girard-Satabin and Alban Grastien and Aymeric Varasse and Zakaria Chihani},
journal= {arXiv preprint arXiv:2506.12084},
year = {2026}
}