Efficient Non-Equivalence Certification and an All-U Equivalence Criterion for Clifford–U Circuits

Quantum circuit equivalence checking asks whether two circuits implement the same unitary (up to a global phase). It guarantees compiler correctness and safe optimization, yet most existing approaches scale exponentially with qubits or depth, or are restricted to Clifford-only cases or commuting substructures. These limitations confine equivalence checking to narrow special cases, far from practical circuits. In this work, we present a novel equivalence-checking method for circuits formed by arbitrary single-qubit layers interleaved with Clifford layers. This pattern is common in variational quantum algorithms (VQAs), for example, and can represent any unitary with sufficient depth. For any pair of circuits that share the same single-qubit layers in the same order, we prove: (1) there is an efficient classical algorithm that certifies their non-equivalence in time linear in qubits and depth; and (2) a criterion which can be efficiently evaluated classically that holds if and only if the pair is equivalent for every possible choice of the shared single-qubit layers. These guarantees enable linear-time verification at scale. Our framework supports regression and differential testing of compilers, certification of optimization passes, and provides reliability checks for the compilation of parameterized circuits.