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

TL;DR

This paper introduces a new method for checking the equivalence of hybrid quantum circuits, combining unitary verification with measurement techniques, significantly improving over prior approaches and handling larger classes of problems.

Contribution

The paper presents a novel approach using deferred measurement and unitary-level techniques to efficiently verify hybrid quantum circuit equivalence, extending capabilities beyond existing methods.

Findings

Outperforms prior hybrid circuit equivalence methods

Handles larger classes of hybrid circuits with new techniques

Identifies unexpected behaviors in Qiskit compiler

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.