序列神经网络可扩展的形式化验证方法

his paper focuses on investigating a scalable formal verification approach for sequential neural networks. Owing to their substantial capabilities in processing sequential data, sequential neural networks have found widespread application across various software systems, particularly in the case of Transformer and Recurrent Neural Network models. However, in the context of continuous data collection in system environments, sequential data may be compromised by measurement errors or adversarial noise. This paper introduces a formal verification method that utilizes sampling, linear programming, and extreme value theory to support the robustness verification and analysis of sequential neural network models, such as Transformers and RNNs. To demonstrate the method\'s effectiveness, this research evaluates and analyzes its application across real-world sequence data analysis systems, including network traffic data classification and recommendation systems. Compared to the current state-of-the-art verifiers, experimental results demonstrate an improvement in verification accuracy through our method, offering a tighter approximation to the boundaries of nonlinear operations, and supporting a diverse range of neural network model structures and operations, thus showcasing significant scalability.