The formal specification and verification of machine learning models have advanced remarkably in less than a decade, leading to a profusion of verification tools that provide mathematical guarantees about model properties. However, this growing diversity risks ecosystem fragmentation, making it difficult to compare tools beyond narrowly defined benchmarks. Moreover, much of the progress to date has focused on a limited class of properties, particularly local robustness. While existing tools are increasingly effective at verifying such properties, more complex ones, such as those involving multiple neural networks, remain beyond their capabilities: these properties cannot currently be expressed in their specification languages, nor can they be directly verified. This applies even to the winning verification tools of the International Verification of Neural Networks Competition (VNN-Comp). In this tool paper, we present CAISAR, an open-source platform for specifying and verifying properties of machine learning models, with particular focus on neural networks and support vector machines. CAISAR provides a high-level language for specifying complex properties and integrates several state-of-the-art verifiers for their automatic verification. Through concrete use cases, we show how CAISAR leverages automated graph-editing techniques to translate high-level specifications into queries for the supported verifiers, bridging the (embedding) gap between user specifications and the corresponding ones that are actually verified.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

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

  • Michele Alberti,
  • François Bobot,
  • Julien Girard-Satabin,
  • Alban Grastien,
  • Aymeric Varasse,
  • Zakaria Chihani

摘要

The formal specification and verification of machine learning models have advanced remarkably in less than a decade, leading to a profusion of verification tools that provide mathematical guarantees about model properties. However, this growing diversity risks ecosystem fragmentation, making it difficult to compare tools beyond narrowly defined benchmarks. Moreover, much of the progress to date has focused on a limited class of properties, particularly local robustness. While existing tools are increasingly effective at verifying such properties, more complex ones, such as those involving multiple neural networks, remain beyond their capabilities: these properties cannot currently be expressed in their specification languages, nor can they be directly verified. This applies even to the winning verification tools of the International Verification of Neural Networks Competition (VNN-Comp). In this tool paper, we present CAISAR, an open-source platform for specifying and verifying properties of machine learning models, with particular focus on neural networks and support vector machines. CAISAR provides a high-level language for specifying complex properties and integrates several state-of-the-art verifiers for their automatic verification. Through concrete use cases, we show how CAISAR leverages automated graph-editing techniques to translate high-level specifications into queries for the supported verifiers, bridging the (embedding) gap between user specifications and the corresponding ones that are actually verified.