Handling Non-Unitaries in Quantum Circuit Equivalence Checking

TL;DR

This paper addresses the challenge of verifying dynamic quantum circuits with non-unitary primitives by proposing methods that enable existing equivalence checking techniques to be applicable to this broader class.

Contribution

It introduces two schemes to handle non-unitary elements in dynamic quantum circuits, extending existing verification methods to this new class.

Findings

Existing verification techniques can be adapted for non-unitary dynamic circuits.

The proposed schemes are validated both theoretically and experimentally.

Verification of dynamic circuits becomes feasible with the new approaches.

Abstract

Quantum computers are reaching a level where interactions between classical and quantum computations can happen in real-time. This marks the advent of a new, broader class of quantum circuits: dynamic quantum circuits. They offer a broader range of available computing primitives that lead to new challenges for design tasks such as simulation, compilation, and verification. Due to the non-unitary nature of dynamic circuit primitives, most existing techniques and tools for these tasks are no longer applicable in an out-of-the-box fashion. In this work, we discuss the resulting consequences for quantum circuit verification, specifically equivalence checking, and propose two different schemes that eventually allow to treat the involved circuits as if they did not contain non-unitaries at all. As a result, we demonstrate methodically, as well as, experimentally that existing techniques for verifying the equivalence of quantum circuits can be kept applicable for this broader class of circuits.