Verifying the safety properties of neural network controlled systems (NNCSs) is essential before their deployment in safety-critical scenarios. NNCSs face significant verification challenges due to the complex nonlinear interactions between neural network controllers and dynamic systems. While Taylor models (TMs) excel in capturing nonlinear dynamics of the system and linear abstract domains efficiently verify neural networks, their isolated use faces two limitations: TMs struggle with neural network scalability, while linear abstract domains cannot precisely represent nonlinear system states. To overcome these limitations, we present a verification approach that synergistically integrates TMs with linear abstract domains. Since naive interval-based approximations often destroy variable dependencies between TMs and linear abstract domains, we further propose a parity-characteristic-driven linearization method to construct interval linear abstraction of TMs, preserving variable dependencies by extracting relationships in nonlinear terms and incorporating them into linear terms. Based on the interval linear abstraction of TMs, our approach enables bidirectional conversion between TMs and different linear abstract domains while reducing precision loss during abstraction conversion. We implemented a prototype named TTLA. Experimental results show that TTLA outperforms the tools in terms of both efficiency and tightness of the reachable set overapproximation. In addition, TTLA enables scalable verification, with neural network analysis time under 0.7 s even for large networks.

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

Verifying Neural Network Controlled Systems by Combining Taylor Models and Linear Abstract Domains

  • Minghao Li,
  • Liqian Chen,
  • Xinyu Wang,
  • Shifu Yang,
  • Yuan Zhou,
  • Ji Wang

摘要

Verifying the safety properties of neural network controlled systems (NNCSs) is essential before their deployment in safety-critical scenarios. NNCSs face significant verification challenges due to the complex nonlinear interactions between neural network controllers and dynamic systems. While Taylor models (TMs) excel in capturing nonlinear dynamics of the system and linear abstract domains efficiently verify neural networks, their isolated use faces two limitations: TMs struggle with neural network scalability, while linear abstract domains cannot precisely represent nonlinear system states. To overcome these limitations, we present a verification approach that synergistically integrates TMs with linear abstract domains. Since naive interval-based approximations often destroy variable dependencies between TMs and linear abstract domains, we further propose a parity-characteristic-driven linearization method to construct interval linear abstraction of TMs, preserving variable dependencies by extracting relationships in nonlinear terms and incorporating them into linear terms. Based on the interval linear abstraction of TMs, our approach enables bidirectional conversion between TMs and different linear abstract domains while reducing precision loss during abstraction conversion. We implemented a prototype named TTLA. Experimental results show that TTLA outperforms the tools in terms of both efficiency and tightness of the reachable set overapproximation. In addition, TTLA enables scalable verification, with neural network analysis time under 0.7 s even for large networks.