The verification of DNNs has garnered significant attention recently, especially with the growing willingness of their utilization in safety and security-critical applications. Due to the complexity and large size of such networks, ensuring guarantees about their behavior in an automated way remains a challenging task. Despite the challenges, achieving automated formal verification would represent an important step towards their wider adoption. In this paper, we consider the problem of formally verifying DNNs based on an optimized strategy that enables the combination and parallel invocation of a set of existing verification techniques. Our approach involves computing interval over-approximations of the output set for feed-forward neural networks with input uncertainty. We achieve such an over-approximation by leveraging various existing approaches and adapting bound reduction methods for the verification of some desired properties, e.g., robustness. In particular, we propose an automated approach that supports the formal verification of various types of DNN specifications with arbitrary, bounded, multivariate, linear, and non-linear activation functions.  We report on the workflow of our approach process, its implementation in a framework, and provide an illustration of the technique using the DNN of the ACAS Xu benchmark pertaining to an Airborne Collision Avoidance System.

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

A High Parallelization Method for Automated Formal Verification of Deep Neural Networks

  • Imene Ben Hafaiedh,
  • Amira Chouchane,
  • Amani Elaoud,
  • Linda Lamouchi,
  • Mohamed Ghazel

摘要

The verification of DNNs has garnered significant attention recently, especially with the growing willingness of their utilization in safety and security-critical applications. Due to the complexity and large size of such networks, ensuring guarantees about their behavior in an automated way remains a challenging task. Despite the challenges, achieving automated formal verification would represent an important step towards their wider adoption. In this paper, we consider the problem of formally verifying DNNs based on an optimized strategy that enables the combination and parallel invocation of a set of existing verification techniques. Our approach involves computing interval over-approximations of the output set for feed-forward neural networks with input uncertainty. We achieve such an over-approximation by leveraging various existing approaches and adapting bound reduction methods for the verification of some desired properties, e.g., robustness. In particular, we propose an automated approach that supports the formal verification of various types of DNN specifications with arbitrary, bounded, multivariate, linear, and non-linear activation functions.  We report on the workflow of our approach process, its implementation in a framework, and provide an illustration of the technique using the DNN of the ACAS Xu benchmark pertaining to an Airborne Collision Avoidance System.