Approximate Bisimulation Relations for Neural Networks and Application to Assured Neural Network Compression

TL;DR

This paper introduces an approximate bisimulation relation for neural networks, enabling quantitative comparison, model reduction, and assured compression, which accelerates verification processes and enhances neural network reliability.

Contribution

It develops a novel approximate bisimulation framework for neural networks and applies it to neural network compression and verification acceleration.

Findings

Quantitative measurement of output differences between neural networks.

Effective neural network compression with assured accuracy.

Accelerated verification of neural networks using the proposed method.

Abstract

In this paper, we propose a concept of approximate bisimulation relation for feedforward neural networks. In the framework of approximate bisimulation relation, a novel neural network merging method is developed to compute the approximate bisimulation error between two neural networks based on reachability analysis of neural networks. The developed method is able to quantitatively measure the distance between the outputs of two neural networks with the same inputs. Then, we apply the approximate bisimulation relation results to perform neural networks model reduction and compute the compression precision, i.e., assured neural networks compression. At last, using the assured neural network compression, we accelerate the verification processes of ACAS Xu neural networks to illustrate the effectiveness and advantages of our proposed approximate bisimulation approach.