# Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 14 of its 44 references that are in the map.
- First posted on arXiv 11 May 2026.

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

- [Explaining and Harnessing Adversarial Examples](https://mlsanity.com/paper/1412.6572/) (2014)
- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [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)
- [The 6th International Verification of Neural Networks Competition (VNN-COMP 2025): Summary and Results](https://mlsanity.com/paper/2512.19007/) (2025)
- [Sparse Polynomial Zonotopes: A Novel Set Representation for Reachability Analysis](https://mlsanity.com/paper/1901.01780/) (2019)
- [Computing-In-Memory Neural Network Accelerators for Safety-Critical Systems: Can Small Device Variations Be Disastrous?](https://mlsanity.com/paper/2207.07626/) (2022)
- [On the Accuracy of Analog Neural Network Inference Accelerators](https://mlsanity.com/paper/2109.01262/) (2021)
- [Formal Verification of Graph Convolutional Networks with Uncertain Node Features and Uncertain Graph Structure](https://mlsanity.com/paper/2404.15065/) (2024)
- [Out of the Shadows: Exploring a Latent Space for Neural Network Verification](https://mlsanity.com/paper/2505.17854/) (2025)
- [PolyThrottle: Energy-efficient Neural Network Inference on Edge Devices](https://mlsanity.com/paper/2310.19991/) (2023)
- [The Promise of Analog Deep Learning: Recent Advances, Challenges and Opportunities](https://mlsanity.com/paper/2406.12911/) (2024)
- [GLOVA: Global and Local Variation-Aware Analog Circuit Design with Risk-Sensitive Reinforcement Learning](https://mlsanity.com/paper/2505.11208/) (2025)
- [J3DAI: A tiny DNN-Based Edge AI Accelerator for 3D-Stacked CMOS Image Sensor](https://mlsanity.com/paper/2506.15316/) (2025)

## Abstract (arXiv)

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. This model is formally verified via reachability analysis using polynomial zonotopes, thus avoiding conventional, time-consuming Monte Carlo simulations. We evaluate our proposed verification approach on three different datasets and on fully-connected and convolutional analog neural networks. Our experimental results confirm the effectiveness of our verification approach by reducing the verification time from up to a day to seconds while enclosing up to 99% of the variation samples.