VeriCompress: A Tool to Streamline the Synthesis of Verified Robust Compressed Neural Networks from Scratch

TL;DR

VeriCompress is a tool that automates the creation of verified robust, compressed neural networks optimized for safety-critical, resource-limited platforms, achieving faster training and better accuracy and robustness than existing methods.

Contribution

It introduces VeriCompress, a novel automated approach for synthesizing verified robust compressed neural networks with improved speed, accuracy, and resource efficiency.

Findings

Models trained with VeriCompress are 2-3 times faster to train.

Achieves 15.1% higher accuracy and 9.8% better robustness on average.

Models require 5-8 times less memory and 2-4 times less inference time.

Abstract

AI's widespread integration has led to neural networks (NNs) deployment on edge and similar limited-resource platforms for safety-critical scenarios. Yet, NN's fragility raises concerns about reliable inference. Moreover, constrained platforms demand compact networks. This study introduces VeriCompress, a tool that automates the search and training of compressed models with robustness guarantees. These models are well-suited for safety-critical applications and adhere to predefined architecture and size limitations, making them deployable on resource-restricted platforms. The method trains models 2-3 times faster than the state-of-the-art approaches, surpassing relevant baseline approaches by average accuracy and robustness gains of 15.1 and 9.8 percentage points, respectively. When deployed on a resource-restricted generic platform, these models require 5-8 times less memory and 2-4 times less inference time than models used in verified robustness literature. Our comprehensive evaluation across various model architectures and datasets, including MNIST, CIFAR, SVHN, and a relevant pedestrian detection dataset, showcases VeriCompress's capacity to identify compressed verified robust models with reduced computation overhead compared to current standards. This underscores its potential as a valuable tool for end users, such as developers of safety-critical applications on edge or Internet of Things platforms, empowering them to create suitable models for safety-critical, resource-constrained platforms in their respective domains.