Formal Verification of Variational Quantum Circuits

2025/07/14 by Nicola Assolini, Assolini, Nicola, Luca Marzari +5
Computer Science · Engineering · #FOS: Computer and information sciences #FOS: Physical sciences #Formal Methods in Verification #Machine Learning (cs.LG) #Programming Languages (cs.PL) #Quantum Computing Algorithms and Architecture #Quantum Physics (quant-ph) #Radiation Effects in Electronics

paper · pdf · doi:10.48550/arxiv.2507.10635

openalex publication_date 2025/07/14 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

Abstract

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.

Citations

• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation
• ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks
• Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees
• Provable Preimage Under-Approximation for Neural Networks (Full Version)
• Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs
• Quantum-classical convolutional neural networks in radiological image classification
• Variational Quanvolutional Neural Networks with enhanced image encoding
• Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification
• ZX-calculus for the working quantum computer scientist
• Variational quantum algorithms
• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
• Branch and Bound for Piecewise Linear Neural Network Verification
• Algorithms for Verifying Deep Neural Networks
• Efficient Neural Network Robustness Certification with General Activation Functions
• Formal Security Analysis of Neural Networks using Symbolic Intervals
• An introduction to quantum machine learning
• Intriguing properties of neural networks
• Elementary gates for quantum computation

Related

• On the relation between trainability and dequantization of variational quantum learning models
• Variational quantum computing for quantum simulation: principles, implementations, and challenges
• Model Checking for Verification of Quantum Circuits
• Analysis of Parameterized Quantum Circuits: on The Connection Between Expressibility and Types of Quantum Gates
• When Quantum and Classical Models Disagree: Learning Beyond Minimum Norm Least Square