Efficient equivalence checking of Clifford-U circuits with shared single-qubit unitaries

TL;DR

This paper introduces an efficient classical algorithm for checking the equivalence of quantum circuits composed of shared single-qubit layers and Clifford layers, which is crucial for compiler validation and optimization in quantum computing.

Contribution

It presents a novel, scalable method for equivalence checking of a broad class of quantum circuits involving shared single-qubit unitaries, applicable to variational algorithms and Trotter decompositions.

Findings

The algorithm can determine equivalence for all choices of shared single-qubit unitaries.

It can also certify non-equivalence for fixed single-qubit assignments.

Supports validation and optimization of quantum compilers.

Abstract

Quantum circuit equivalence checking asks whether two circuits implement the same unitary. It guarantees compiler correctness and safe optimization, yet most existing approaches scale exponentially with the number of qubits or the circuit depth, or are restricted to specific circuit structures. In this work, we present an equivalence-checking method for circuits formed by arbitrary single-qubit layers interleaved with Clifford layers. This pattern is common in variational quantum algorithms and Hamiltonian simulation via Trotter decomposition. It can also represent any unitary with sufficient depth. We prove the existence of an efficient classical algorithm that determines whether a pair of circuits with shared single-qubit layers are equivalent for every possible choice of the shared single-qubit unitaries. The same algorithm can also certify their non-equivalence for fixed assignments of single-qubit unitaries. Our framework supports the validation of emerging quantum compilers and facilitate the discovery of novel circuit optimization passes.