Quantum Circuit Equivalence Checking: A Tractable Bridge From Unitary to Hybrid Circuits

TL;DR

The paper tackles the challenging problem of verifying equivalence between hybrid quantum circuits that include measurements and discards, which are common in quantum compilation flows. It introduces a lifting strategy that converts unitary circuit verification into hybrid circuit equivalence checking using the deferred measurement transformation, aided by the path-sums formalism. The authors implement SQbricks, comprising SQbricks-Verif for unitary verification and SQbricks-Lifting for lifting to hybrid circuits, and demonstrate strong performance gains over state-of-the-art tools across DisFree, Mix, and Dis categories, while also revealing practical insights into Qiskit compiler behavior. The work provides a scalable, open-source baseline for automated hybrid circuit equivalence checking and offers concrete benchmarks and methodological guidance for future research in quantum circuit verification.

Abstract

Equivalence checking of hybrid quantum circuits is of primary importance, given that quantum circuit transformations are omnipresent along the quantum compiler chain. While some approaches exist for automating this task, most focus on the simple case of unitary circuits. At the same time, real quantum computing requires hybrid circuits equipped with measurement operators. Moreover, the few approaches targeting the hybrid case are limited to a restricted class of problems. We propose tackling the Quantum Hybrid Circuit Equivalence Checking problem through lifting unitary circuit verification using a transformation known as deferred measurement. We show that this approach alone significantly outperforms prior work, and that, with the addition of specific unitary-level techniques we call separation and projection, it can handle much larger classes of hybrid circuit equivalence problems. We have implemented and evaluated our method over standard circuit transformations such as teleportation, one-way measurement, or the IBM Qiskit compiler, demonstrating its promises. As a side finding, we have identified and reported several unexpected behaviours with the Qiskit compiler.