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

arXiv: https://arxiv.org/abs/2207.06759 · HTML: https://mlsanity.com/paper/2207.06759/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 23 of its 51 references that are in the map.
- First posted on arXiv 14 Jul 2022.

## Builds on (most cited first, 23 of 23)

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [DeepFool: a simple and accurate method to fool deep neural networks](https://mlsanity.com/paper/1511.04599/) (2015)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Image Segmentation Using Deep Learning: A Survey](https://mlsanity.com/paper/2001.05566/) (2020)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Safety Verification of Deep Neural Networks](https://mlsanity.com/paper/1610.06940/) (2016)
- [Towards Fast Computation of Certified Robustness for ReLU Networks](https://mlsanity.com/paper/1804.09699/) (2018)
- [Formal Verification of Piece-Wise Linear Feed-Forward Neural Networks](https://mlsanity.com/paper/1705.01320/) (2017)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems](https://mlsanity.com/paper/2004.05519/) (2020)
- [An approach to reachability analysis for feed-forward ReLU neural networks](https://mlsanity.com/paper/1706.07351/) (2017)
- [On the Robustness of Semantic Segmentation Models to Adversarial Attacks](https://mlsanity.com/paper/1711.09856/) (2017)
- [Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks](https://mlsanity.com/paper/1708.03322/) (2017)
- [Verification of Deep Convolutional Neural Networks Using ImageStars](https://mlsanity.com/paper/2004.05511/) (2020)
- [Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness](https://mlsanity.com/paper/1904.09959/) (2019)
- [Studying Robustness of Semantic Segmentation under Domain Shift in cardiac MRI](https://mlsanity.com/paper/2011.07592/) (2020)
- [Improved Noise and Attack Robustness for Semantic Segmentation by Using Multi-Task Training with Self-Supervised Depth Estimation](https://mlsanity.com/paper/2004.11072/) (2020)
- [Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations](https://mlsanity.com/paper/1712.08163/) (2017)
- [Automated Evaluation of Semantic Segmentation Robustness for Autonomous Driving](https://mlsanity.com/paper/1810.10193/) (2018)
- [Formal Verification of CNN-based Perception Systems](https://mlsanity.com/paper/1811.11373/) (2018)
- [Specification-Guided Safety Verification for Feedforward Neural Networks](https://mlsanity.com/paper/1812.06161/) (2018)

## Abstract (arXiv)

This work in progress paper introduces robustness verification for autoencoder-based regression neural network (NN) models, following state-of-the-art approaches for robustness verification of image classification NNs. Despite the ongoing progress in developing verification methods for safety and robustness in various deep neural networks (DNNs), robustness checking of autoencoder models has not yet been considered. We explore this open space of research and check ways to bridge the gap between existing DNN verification methods by extending existing robustness analysis methods for such autoencoder networks. While classification models using autoencoders work more or less similar to image classification NNs, the functionality of regression models is distinctly different. We introduce two definitions of robustness evaluation metrics for autoencoder-based regression models, specifically the percentage robustness and un-robustness grade. We also modified the existing Imagestar approach, adjusting the variables to take care of the specific input types for regression networks. The approach is implemented as an extension of NNV, then applied and evaluated on a dataset, with a case study experiment shown using the same dataset. As per the authors' understanding, this work in progress paper is the first to show possible reachability analysis of autoencoder-based NNs.
