Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes

TL;DR

This paper introduces a polynomial zonotope-based formal verification method for analog neural networks that accounts for process variations, significantly reducing verification time compared to Monte Carlo simulations.

Contribution

It presents a novel polynomial model and reachability analysis approach for verifying analog neural networks under process variations, improving efficiency and accuracy.

Findings

Verification time reduced from days to seconds.

Encloses 99% of variation samples.

Effective for both fully-connected and convolutional networks.

Abstract

Analog neural networks are gaining attention due to their efficiency in terms of power consumption and processing speed. However, since analog neural networks are implemented as physical circuits, they are highly sensitive to manufacturing process variations, which can cause large deviations from the nominal model. We present a polynomial-based model that resembles the performance of the neuron circuit under process variations. Then, we formally verify the behavior of the circuit-level model using reachability analysis with polynomial zonotopes, thus, avoiding conventional, time-consuming Monte Carlo simulations. We evaluate our proposed verification approach on three different datasets, verifying both fully-connected and convolutional analog neural networks. Our experimental results confirm the effectiveness of our verification approach by reducing the verification time from days to seconds while enclosing 99% of the variation samples.