Formal Verification of Variational Quantum Circuits

• URL: http://arxiv.org/abs/2507.10635v1
• Date: Mon, 14 Jul 2025 12:28:32 GMT
• Title: Formal Verification of Variational Quantum Circuits
• Authors: Nicola Assolini, Luca Marzari, Isabella Mastroeni, Alessandra di Pierro,
• Abstract summary: Variational quantum circuits (VQCs) are a central component of many quantum machine learning algorithms.<n>We present the first in-depth theoretical and practical study of the formal verification problem for VQCs.
• Score: 44.06507276521908
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• VQC-MLPNet: An Unconventional Hybrid Quantum-Classical Architecture for Scalable and Robust Quantum Machine Learning [60.996803677584424]
  Variational Quantum Circuits (VQCs) offer a novel pathway for quantum machine learning.<n>Their practical application is hindered by inherent limitations such as constrained linear expressivity, optimization challenges, and acute sensitivity to quantum hardware noise.<n>This work introduces VQC-MLPNet, a scalable and robust hybrid quantum-classical architecture designed to overcome these obstacles.
  arXiv  Detail & Related papers  (2025-06-12T01:38:15Z)
• RhoDARTS: Differentiable Quantum Architecture Search with Density Matrix Simulations [48.670876200492415]
  Variational Quantum Algorithms (VQAs) are a promising approach for leveraging powerful Noisy Intermediate-Scale Quantum (NISQ) computers.<n>We propose $rho$DARTS, a differentiable Quantum Architecture Search (QAS) algorithm that models the search process as the evolution of a quantum mixed state.
  arXiv  Detail & Related papers  (2025-06-04T08:30:35Z)
• Quantum Pattern Detection: Accurate State- and Circuit-based Analyses [2.564905016909138]
  We propose a framework for the automatic detection of quantum patterns using state- and circuit-based code analysis.<n>In an empirical evaluation, we show that our framework is able to detect quantum patterns very accurately and that it outperforms existing quantum pattern detection approaches.
  arXiv  Detail & Related papers  (2025-01-27T09:42:41Z)
• Quantum algorithms: A survey of applications and end-to-end complexities [88.57261102552016]
  The anticipated applications of quantum computers span across science and industry.<n>We present a survey of several potential application areas of quantum algorithms.<n>We outline the challenges and opportunities in each area in an "end-to-end" fashion.
  arXiv  Detail & Related papers  (2023-10-04T17:53:55Z)
• Ansatz-Agnostic Exponential Resource Saving in Variational Quantum Algorithms Using Shallow Shadows [5.618657159109373]
  Variational Quantum Algorithms (VQA) have been identified as a promising candidate for the demonstration of near-term quantum advantage. We present a protocol based on shallow shadows that achieves similar levels of savings for almost any shallow ansatz studied in the literature. We show that two important applications in quantum information for which VQAs can be a powerful option, namely variational quantum state preparation and variational quantum circuit synthesis.
  arXiv  Detail & Related papers  (2023-09-09T11:00:39Z)
• Pre-training Tensor-Train Networks Facilitates Machine Learning with Variational Quantum Circuits [70.97518416003358]
  Variational quantum circuits (VQCs) hold promise for quantum machine learning on noisy intermediate-scale quantum (NISQ) devices. While tensor-train networks (TTNs) can enhance VQC representation and generalization, the resulting hybrid model, TTN-VQC, faces optimization challenges due to the Polyak-Lojasiewicz (PL) condition. To mitigate this challenge, we introduce Pre+TTN-VQC, a pre-trained TTN model combined with a VQC.
  arXiv  Detail & Related papers  (2023-05-18T03:08:18Z)
• Uncovering Instabilities in Variational-Quantum Deep Q-Networks [0.0]
  We show that variational quantum deep Q-networks (VQ-DQN) are subject to instabilities that cause the learned policy to diverge. We execute RL algorithms on an actual quantum processing unit (an IBM Quantum Device) and investigate differences in behaviour between simulated and physical quantum systems.
  arXiv  Detail & Related papers  (2022-02-10T17:52:44Z)
• Model Checking for Verification of Quantum Circuits [1.1878820609988696]
  We will describe a framework for assertion-based verification of quantum circuits. Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks.
  arXiv  Detail & Related papers  (2021-04-23T00:43:37Z)
• Using Quantum Metrological Bounds in Quantum Error Correction: A Simple Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
  We present a proof of the approximate Eastin-Knill theorem, which connects the quality of a quantum error-correcting code with its ability to achieve a universal set of logical gates. Our derivation employs powerful bounds on the quantum Fisher information in generic quantum metrological protocols.
  arXiv  Detail & Related papers  (2020-04-24T17:58:10Z)
• On the Principles of Differentiable Quantum Programming Languages [13.070557640180004]
  Variational Quantum Circuits (VQCs) are predicted to be one of the most important near-term quantum applications. We propose the first formalization of auto-differentiation techniques for quantum circuits.
  arXiv  Detail & Related papers  (2020-04-02T16:46:13Z)
• Entanglement Classification via Neural Network Quantum States [58.720142291102135]
  In this paper we combine machine-learning tools and the theory of quantum entanglement to perform entanglement classification for multipartite qubit systems in pure states. We use a parameterisation of quantum systems using artificial neural networks in a restricted Boltzmann machine (RBM) architecture, known as Neural Network Quantum States (NNS)
  arXiv  Detail & Related papers  (2019-12-31T07:40:23Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.