Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes

Fuente: arXiv
Gespeichert in:
Bibliographische Detailangaben
Hauptverfasser: Abu-Haeyeh, Yasmine, Ladner, Tobias, Althoff, Matthias, Hedrich, Lars
Format: Preprint
Veröffentlicht: 2026
Schlagworte:
Online-Zugang:
Tags: Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
_version_ 1866910209154220032
author Abu-Haeyeh, Yasmine
Ladner, Tobias
Althoff, Matthias
Hedrich, Lars
author_facet Abu-Haeyeh, Yasmine
Ladner, Tobias
Althoff, Matthias
Hedrich, Lars
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2605_10474
institution arXiv
publishDate 2026
record_format arxiv
spellingShingle Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes
Abu-Haeyeh, Yasmine
Ladner, Tobias
Althoff, Matthias
Hedrich, Lars
Machine Learning
Artificial Intelligence
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.
title Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes
topic Machine Learning
Artificial Intelligence
url https://arxiv.org/abs/2605.10474