Scalable Equivalence Checking and Verification of Shallow Quantum Circuits

TL;DR

This work tackles the challenging problem of checking equivalence between shallow quantum circuits, where direct classical simulation is often intractable. The authors develop a constraint-based representation of a circuit’s output as a commuting tuple of local projections, leveraging light-cone locality to keep the description compact for fixed depth $d$. They present efficient procedures for two notions of equivalence, using reversibility and Choi-state techniques to reduce strong equivalence to the weak form, with runtimes scaling as $T(n,d)=f(d)\cdot O(n)$ where $f(d)$ is exponential in $d$ but independent of $n$. The framework also supports static and run-time assertions expressed as conjunctions of local projections, enabling both verification and debugging, including NISQ-device verification. Empirical results on large qubit counts (e.g., up to $n=100$) demonstrate practical efficiency: depths like $d=3$ achieve sub-second to tens-of-second run times, while deeper shallow circuits remain tractable due to the linear scaling in $n$ and the controlled growth of projection sizes.

Abstract

This paper concerns the problem of checking if two shallow (i.e., constant-depth) quantum circuits perform equivalent computations. Equivalence checking is a fundamental correctness question -- needed, e.g., for ensuring that transformations applied to a quantum circuit do not alter its behavior. For quantum circuits, the problem is challenging because a straightforward representation on a classical computer of each circuit's quantum state can require time and space that are exponential in the number of qubits $n$. The paper presents decision procedures for two variants of the equivalence-checking problem. Both can be carried out on a classical computer in time and space that, for any fixed depth, is linear in $n$. Our critical insight is that local projections are precise enough to completely characterize the output state of a shallow quantum circuit. Instead of explicitly computing the output state of a circuit, we generate a set of local projections that serve as constraints on the output state. Moreover, the circuit's output state is the unique quantum state that satisfies all the constraints. Beyond equivalence checking, we show how to use the constraint representation to check a class of assertions, both statically and at run time. Our assertion-checking methods are sound and complete for assertions expressed as conjunctions of local projections. Our experiments show that on a server equipped with 2 x Intel\textsuperscript{\textregistered} Xeon\textsuperscript{\textregistered} Gold 6338 CPUs (128 threads total) and 1.0~TiB of RAM, running Ubuntu 20.04.6 LTS, the constraint representation of a random 100-qubit circuit of depth 6 can be computed in 19.8 seconds. For fixed inputs $\ket{0}^{\otimes 100}$, equivalence checking of {random} 100-qubit circuits of depth 3 takes 4.46 seconds; for arbitrary inputs, it takes no more than 31.96 seconds.

Figures (7)

• Figure 1: The example: each layer consists of two-qubit unitaries applied to disjoint qubits.
• Figure 2: Running times for computing local-projection descriptions and explicit state vectors. (a) Depth is fixed at $d=6$. (b) The number of qubits is fixed at $n=30$. Each point is averaged over 100 random circuits. Error bars (visible when the figure is magnified) indicate one standard deviation.
• Figure 3: Three implementations of a controled-controlled-$U$ gate NI11, where $W^2=U$.
• Figure 4: For $U = \text{diag}(e^{-i\theta}, e^{i\theta})$, we have a depth-4 implementation of a controlled-controlled-$U$ gate PhysRevA.91.032302, where $W^2 = U$, and 2-qubit gate $V$ is defined by $V\ket{00} = \ket{01}$, $V\ket{01} = \ket{00}$, $V\ket{10} = \ket{10}$, and $V\ket{11} = \ket{11}$.
• Figure 5: Graphs of running time as a function of number of qubits for (a) checking equivalence and inequivalence under \ref{['equi-w']} (i.e., fixed input state $\ket{0}^{\otimes n}$), and (b) checking equivalence/inequivalence under \ref{['equi-s']}. Error bars (visible in (a) when the figure is magnified) indicate one standard deviation.

Theorems & Definitions (9)

• Lemma 4.1: YP21
• Lemma 4.2: YP21
• Lemma 4.3
• Lemma 4.4
• Theorem 5.1
• definition 1: Weak equivalence
• definition 2: Strong equivalence
• definition 3: Syntax and Semantics of the assertion in li2019proq
• definition 4: Semantics for commuting local projections as an assertion