Work In Progress: Safety and Robustness Verification of Autoencoder-Based Regression Models using the NNV Tool

State-of-the-art and well-trained neural networks (NN) can easily be attacked by small perturbations in inputs, leading to significant aberrations in their outputs [14, 23, 33]. These input perturbations are not only limited to image-based networks but also apply to other input types as well, e.g., time-series data or input signals. Such lack of robustness poses serious risks to information integrity, privacy and security, and can be catastrophic in safety-critical applications [11, 29]. While verification of NNs with image inputs is a vastly growing research area; specifically, with recent ongoing works on safety and robustness checking of feedforward (FFNN), convolutional (CNN), and semantic segmentation networks (SSN); less has been done in the domain of autoencoder verification. Classification models using autoencoders work almost similar to usual classifiers, but there is a need for new research to develop verification techniques for regression models. The regression-based autoencoders regenerate the input in its output and thus can be checked using verification techniques whether the recreated output comes within a certain accepted range of the unperturbed input, in case there is a certain fault/attack on its input side. In a prior work, the authors of [36] introduced a novel framework for NN verification named Neural Network Verification (NNV) [38] tool, capable of evaluating the robustness of several DNN architectures, e.g., FFNN, CNN, SSN, etc. Later, a new set-based approach, Imagestar [34, 36] is also incorporated into this tool. In this work in progress work, we explore similar methods in the context of autoencoder verification via experimenting on a sampled dataset and checking if the output lies within a pre-determined safe threshold around the corresponding uninterrupted input values, given a specific type of fault in the input.