Decision Diagrams for Symbolic Verification of Quantum Circuits

TL;DR

This paper introduces a novel decision diagram approach for symbolic verification of quantum circuits, enabling efficient analysis of large and complex quantum algorithms with symbolic components.

Contribution

It presents the first symbolic decision diagram method for quantum circuit verification, supporting symbolic objects and enabling verification of large-scale quantum circuits.

Findings

Verified 160-qubit quantum Fourier transform in three minutes

Enabled efficient verification of algorithms with oracles and classical controls

Demonstrated effectiveness on Bernstein-Vazirani, Grover's, and error correction circuits

Abstract

With the rapid development of quantum computing, automatic verification of quantum circuits becomes more and more important. While several decision diagrams (DDs) have been introduced in quantum circuit simulation and verification, none of them supports symbolic computation. Algorithmic manipulations of symbolic objects, however, have been identified as crucial, if not indispensable, for several verification tasks. This paper proposes the first decision-diagram approach for operating symbolic objects and verifying quantum circuits with symbolic terms. As a notable example, our symbolic tensor decision diagrams (symbolic TDD) could verify the functionality of the 160-qubit quantum Fourier transform circuit within three minutes. Moreover, as demonstrated on Bernstein-Vazirani algorithm, Grover's algorithm, and the bit-flip error correction code, the symbolic TDD enables efficient verification of quantum circuits with user-supplied oracles and/or classical controls.