CAISAR平台让复杂机器学习验证更易实现。
The CAISAR Platform: Extending the Reach of Machine Learning Specification and Verification
- 设计通用验证语言，支持神经网络、支持向量机等模型
- 自动将复杂属性转为先进求解器可处理的查询
- 适合研究者与工程师验证多模型协同的复杂属性
过去十年间，机器学习程序的形式化规范与验证取得了显著进展，催生了大量工具。然而多样性导致碎片化，多数工具难以比较，仅能针对特定基准测试。此外，现有工作主要聚焦局部鲁棒性性质，而对涉及多个神经网络等更复杂性质，当前主流验证竞赛VNN-Comp参赛工具的语言无法表达。本文介绍CAISAR——一个开源的机器学习规范与验证平台。其支持对神经网络、支持向量机和提升树等模型进行复杂属性建模；通过自动化图编辑技术，将规范自动转换为前沿求解器可执行的查询，可直接使用现成求解器。实验展示多个实际案例的可行性。论文附带可复现的代码与数据集，可通过以下DOI获取：10.5281/zenodo.15209510。
原文摘要 · Abstract (English)
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
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。