Scalable Equivalence Checking and Verification of Shallow Quantum Circuits

Abstract

This paper concerns the problem of checking whether two shallow (i.e., constant-depth) quantum circuits perform equivalent computations. Equivalence checking is a fundamental correctness question—needed, for example, to ensure 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 Projection-Based Equivalence Checking (PBEC), which provides 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, are linear in n. Our key insight is that local projections can serve as constraints that fully characterize the output state of a shallow quantum circuit. The 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 showed that computing the constraint representation of a random 100-qubit 1D circuit of depth 6 takes 129.64 seconds. Equivalence checking between two random 100-qubit 1D circuits of depth 3 requires 4.46 seconds for fixed input 0⊗ 100, and no more than 31.96 seconds for arbitrary inputs. Computing the constraint representation for a random 100-qubit circuit of depth 3 takes 6.99 seconds for a 2D structure, compared to 10.67 seconds for a circuit with arbitrary connectivity. At depth 2, equivalence checking takes 0.20 seconds for fixed input and 0.44 seconds for arbitrary input, with similar performance for both 2D and arbitrary-connectivity circuits.