# Formal Verification of Variational Quantum Circuits

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 24 of its 70 references that are in the map.
- First posted on arXiv 14 Jul 2025.

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

- [Intriguing properties of neural networks](https://mlsanity.com/paper/1312.6199/) (2013)
- [Variational Quantum Algorithms](https://mlsanity.com/paper/2012.09265/) (2020)
- [Supervised learning with quantum enhanced feature spaces](https://mlsanity.com/paper/1804.11326/) (2018)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [The effect of data encoding on the expressive power of variational quantum machine learning models](https://mlsanity.com/paper/2008.08605/) (2020)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Algorithms for Verifying Deep Neural Networks](https://mlsanity.com/paper/1903.06758/) (2019)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Formal Security Analysis of Neural Networks using Symbolic Intervals](https://mlsanity.com/paper/1804.10829/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [Quantum generative adversarial networks](https://mlsanity.com/paper/1804.08641/) (2018)
- [Quantum Adversarial Machine Learning](https://mlsanity.com/paper/2001.00030/) (2019)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)
- [Quantum-classical convolutional neural networks in radiological image classification](https://mlsanity.com/paper/2204.12390/) (2022)
- [Provable Preimage Under-Approximation for Neural Networks (Full Version)](https://mlsanity.com/paper/2305.03686/) (2023)
- [Variational Quanvolutional Neural Networks with enhanced image encoding](https://mlsanity.com/paper/2106.07327/) (2021)
- [ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks](https://mlsanity.com/paper/2407.01639/) (2024)
- [Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation](https://mlsanity.com/paper/2505.05235/) (2025)
- [A Deductive Verification Framework for Circuit-building Quantum Programs](https://mlsanity.com/paper/2003.05841/) (2020)
- [Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism](https://mlsanity.com/paper/1511.01572/) (2015)
- [Towards Large-scale Functional Verification of Universal Quantum Circuits](https://mlsanity.com/paper/1805.06908/) (2018)
- [Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs](https://mlsanity.com/paper/2206.13772/) (2022)
- [Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation](https://mlsanity.com/paper/2304.00921/) (2023)
- [Linear and non-linear relational analyses for Quantum Program Optimization](https://mlsanity.com/paper/2410.23493/) (2024)

## Built on by (most cited first, 1 of 1)

- [Quantum Interval Bound Propagation for Certified Training of Quantum Neural Networks](https://mlsanity.com/paper/2605.00747/) (2026)

## Abstract (arXiv)

Variational quantum circuits (VQCs) are a central component of many quantum machine learning algorithms, offering a hybrid quantum-classical framework that, under certain aspects, can be considered similar to classical deep neural networks. A shared aspect is, for instance, their vulnerability to adversarial inputs, small perturbations that can lead to incorrect predictions. While formal verification techniques have been extensively developed for classical models, no comparable framework exists for certifying the robustness of VQCs. Here, we present the first in-depth theoretical and practical study of the formal verification problem for VQCs. Inspired by abstract interpretation methods used in deep learning, we analyze the applicability and limitations of interval-based reachability techniques in the quantum setting. We show that quantum-specific aspects, such as state normalization, introduce inter-variable dependencies that challenge existing approaches. We investigate these issues by introducing a novel semantic framework based on abstract interpretation, where the verification problem for VQCs can be formally defined, and its complexity analyzed. Finally, we demonstrate our approach on standard verification benchmarks.