一句话：提出递归定义量子电路正确性的证明系统，并证明其可靠性与相对完备性。
近年来递归技术被引入量子编程，使大型量子电路与算法能够更简洁、紧凑地编写。然而，如何形式化验证递归定义量子电路的正确性仍缺乏系统方法。本文提出了一个用于验证递归定义量子电路正确性的证明系统，并建立了该系统的可靠性（soundness）与相对完备性（relative completeness）。为展示其有效性，作者给出了一系列应用实例，包括多量子比特受控门、用于生成多量子比特 GHZ 态的量子电路，以及具有递归结构的更复杂量子算法，如量子傅里叶变换、量子态制备和量子随机存取存储器（QRAM）的形式化验证。
Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and compactly 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 demonstrate its effectiveness, we present a series of application examples, including formal verification of multi-qubit controlled gates, a quantum circuit for generating multi-qubit GHZ (Greenberger-Horne-Zeilinger) states, and more sophisticated quantum algorithms with recursive structures such as the quantum Fourier transform, quantum state preparation, and quantum random access memories (QRAMs).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2404-05934,
title = {Verification of Recursively Defined Quantum Circuits},
author = {Mingsheng Ying and Zhicheng Zhang},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808273}
}