Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Verification of Quantum Circuits through Discrete-Time Barrier Certificates

Marco Lewis, Sadegh Soudjani, Paolo Zuliani

TL;DR

The paper addresses verifying quantum circuits by treating them as discrete-time complex dynamical systems and extending barrier certificates to the complex domain. It introduces k-inductive hybrid barrier certificates over complex variables and computes them via Hermitian Sum of Squares (HSOS), enabling safety proofs without evolving the system. The authors develop a Python HSOS solver, verify barriers with SMT tools, and demonstrate the approach on phase, NOT, alternating X/Z, and Grover circuits, highlighting both feasibility for small instances and scalability challenges. This work provides a principled, automatable framework for complex-domain safety verification in quantum settings, with potential applications to broader complex dynamical systems and future work on noise and dimensionality reduction.

Abstract

Current methods for verifying quantum computers are predominately based on interactive or automatic theorem provers. Considering that quantum computers are dynamical in nature, this paper employs and extends the concepts from the verification of dynamical systems to verify properties of quantum circuits. Our main contribution is to propose k-inductive barrier certificates over complex variables and show how to compute them using Hermitian Sum of Squares optimization. We apply this new technique to verify properties of different quantum circuits.

Verification of Quantum Circuits through Discrete-Time Barrier Certificates

TL;DR

The paper addresses verifying quantum circuits by treating them as discrete-time complex dynamical systems and extending barrier certificates to the complex domain. It introduces k-inductive hybrid barrier certificates over complex variables and computes them via Hermitian Sum of Squares (HSOS), enabling safety proofs without evolving the system. The authors develop a Python HSOS solver, verify barriers with SMT tools, and demonstrate the approach on phase, NOT, alternating X/Z, and Grover circuits, highlighting both feasibility for small instances and scalability challenges. This work provides a principled, automatable framework for complex-domain safety verification in quantum settings, with potential applications to broader complex dynamical systems and future work on noise and dimensionality reduction.

Abstract

Current methods for verifying quantum computers are predominately based on interactive or automatic theorem provers. Considering that quantum computers are dynamical in nature, this paper employs and extends the concepts from the verification of dynamical systems to verify properties of quantum circuits. Our main contribution is to propose k-inductive barrier certificates over complex variables and show how to compute them using Hermitian Sum of Squares optimization. We apply this new technique to verify properties of different quantum circuits.
Paper Structure (26 sections, 4 theorems, 30 equations, 6 figures, 1 algorithm)

This paper contains 26 sections, 4 theorems, 30 equations, 6 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Background
  4. Notation
  5. Quantum Circuits
  6. Barrier Certificates for Real Systems
  7. Quantum Circuits as Dynamical Systems
  8. Complex Barrier Certificates
  9. Computation of Barrier Certificates through Hermitian Sum of Squares
  10. Sum of Squares for Complex Numbers
  11. Semi-algebraic Sets
  12. HSOS Equations for Barrier Certificate Constraints
  13. Algorithm for finding a Barrier Certificate
  14. Case Studies
  15. Experimental Setup
  16. ...and 11 more sections

Key Result

theorem 4

Let $S = (\mathcal{Z}, \mathcal{Z}_0, F, f)$ and the unsafe set be $\mathcal{Z}_u$. Suppose there exists a $k$-inductive hybrid barrier certificate: a collection of functions $\{B_t(z)\}_{t\in\mathbb{Z}_{\geq 0}}$, where $B_t(z) \in \mathbb{R}$ for all $t \geq 0$, $z \in \mathcal{Z}$; and constants Then the safety of $S$ with respect to $\mathcal{Z}_u$ is guaranteed.

Figures (6)

  • Figure 1: Gate representations of the $H, Z, X$ and $CNOT$ operations respectively.
  • Figure 2: Example of a quantum circuit.
  • Figure 3: Quantum circuit with 3 unitary operations consisting of grouped gates.
  • Figure 4: Quantum circuit for alternating between $X$ and $Z$ gates with 3 qubits.
  • Figure 5: The quantum circuit for a 3-qubit version of Grover's algorithm. The initial Hadamard gates applied to the state $\ket{000}$ prepare the quantum state for the repeated operations applied to it.
  • ...and 1 more figures

Theorems & Definitions (25)

  • Remark 1
  • definition 1: Safety
  • Remark 2
  • definition 2: Discrete-Time Barrier Certificate Anand21
  • Remark 3
  • definition 3: Discrete-time complex-space system
  • definition 4: Safety
  • theorem 4: $k$-Inductive Hybrid Barrier Certificate
  • proof
  • Remark 5
  • ...and 15 more