Verification of Recursively Defined Quantum Circuits
Quantum Physics
2024-11-08 v2 Logic in Computer Science
Programming Languages
Abstract
Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and economically programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrating its effectiveness, a series of application examples of the proof system are given, including (multi-qubit) controlled gates, a quantum circuit generating (multi-qubit) GHZ (Greenberger-Horne-Zeilinger) states, recursive definition of quantum Fourier transform, quantum state preparation, and quantum random-access memories (QRAM).
Cite
@article{arxiv.2404.05934,
title = {Verification of Recursively Defined Quantum Circuits},
author = {Mingsheng Ying and Zhicheng Zhang},
journal= {arXiv preprint arXiv:2404.05934},
year = {2024}
}