Verifying Neural Network Controlled Systems by Combining Taylor Models and Linear Abstract Domains
摘要
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.