Reachability-Based Robustness Verification of Deep Neural Networks with Emphasis on Safety-Critical Time-Series Applications

Abstract

The advancement of Deep Neural Network (DNN) technologies and their verification methodologies has not fully extended to the realm of time-series neural network (NN) applications, a domain integral to safety-critical functions across various sectors. Historically centered on image-based networks, NNs now confront the broader complexities of time-series data, incorporating elements like environmental noise and rapid data fluctuations. This shift underscores the need for robust NNs capable of accurately interpreting and processing such intricate inputs.

In industrial contexts, for example, NNs play a pivotal role in forecasting operational trends and performing functions like anomaly detection and data compression in time-series formats. The use of autoencoders for encoding complex time-series data exemplifies the growing importance of NNs in these applications. The evolution of time-series-based applications in audio and video processing, including speech recognition and event detection, further highlights the urgency of developing robust verification methods. Accurate processing of dynamic and 'noisy' time-series data is crucial for reliable decision-making and operational efficiency in these critical fields. This thesis introduces the first reachability-based formal verification methodology tailored for time-series applications, specifically focusing on autoencoder models. This represents a strategic pivot from predominantly image-based NN analyses, addressing the nuanced complexities of variable-length time series regression neural networks in predictive maintenance and similar high-stakes applications. Following other case studies in PHM and audio classification domains, this research meets two critical needs in neural network verification: robustness verification for time-series applications in safety-critical domains and the enhancement of the Neural Network Verification (NNV) tool to support more complex network architectures and layer types. This enhancement to the NNV tool, a product of the veriViTAL lab, includes support for LSTM-based DNN applications and introduces the capability to handle variable-length sequences through the integration of sequence input layers. These advancements collectively forge a path toward more comprehensive and reliable NN verification in the context of evolving time-series applications.