Fast equivalence checking of quantum circuits of Clifford gates

TL;DR

This paper introduces a fast, deterministic algorithm for checking the equivalence of Clifford quantum circuits, significantly outperforming previous methods and enabling verification of large-scale quantum circuits efficiently.

Contribution

The paper presents a new $O(n imes m)$ time algorithm for Clifford circuit equivalence checking, outperforming prior SAT-based and path-integral methods.

Findings

Can verify 1000-qubit circuits in ~22 seconds

Handles 100,000-qubit circuits in ~15 minutes

Outperforms existing equivalence checking approaches by orders of magnitude

Abstract

Checking whether two quantum circuits are equivalent is important for the design and optimization of quantum-computer applications with real-world devices. We consider quantum circuits consisting of Clifford gates, a practically-relevant subset of all quantum operations which is large enough to exhibit quantum features such as entanglement and forms the basis of, for example, quantum-error correction and many quantum-network applications. We present a deterministic algorithm that is based on a folklore mathematical result and demonstrate that it is capable of outperforming previously considered state-of-the-art method. In particular, given two Clifford circuits as sequences of single- and two-qubit Clifford gates, the algorithm checks their equivalence in $O(n \cdot m)$ time in the number of qubits $n$ and number of elementary Clifford gates $m$. Using the performant Stim simulator as backend, our implementation checks equivalence of quantum circuits with 1000 qubits (and a circuit depth of 10.000 gates) in $\sim$22 seconds and circuits with 100.000 qubits (depth 10) in $\sim$15 minutes, outperforming the existing SAT-based and path-integral based approaches by orders of magnitude. This approach shows that the correctness of application-relevant subsets of quantum operations can be verified up to large circuits in practice.