Spy Inside: Scalable Verification of Dependable Transformers for Event Time Series Systems

Event time series appear in many software scenarios and are a necessary data type in data analytics systems. Transformers are the preferred type of sequential neural network for advanced analytics on event time series, particularly due to their significant contributions to the recent surge of large language models (LLMs). Event series analytics heavily depends on the quality of input data, which may contain natural measurement errors or adversarial noises. Since the input data deviates from the true state, the opaque nature of neural networks presents a challenge in ensuring the reliability of output, which might be deemed untrustworthy. In this paper, we introduce an innovative formal verification framework for Transformer-based event series systems, leveraging sampling, linear programming, and the extreme value theorem. This framework can support the verification of the dependability of Transformers in managing inputs characterized by unpredictability and uncertainty. To exemplify its utility, we apply our verification approach to verify natural requirements from a real-world event series environments: network traffic classification. It outperforms the current state-of-the-art verifier in terms of effectiveness, providing more stringent verified bounds. Our experimental findings provide valuable benchmarks for guaranteeing reliable deployment of systems in scenarios where the credibility of event data is compromised, and for exposing specific cases in which the expected requirements are not satisfied.