一句话：提出首个用 Coq 完全验证的量子电路优化器 VOQC，基于深嵌入 SQIR 并证明优化正确性。
本文提出了 VOQC，这是首个完全经过验证的量子电路优化器，使用 Coq 证明助手编写。量子电路被表示为 SQIR——一种简单、低级的量子中间表示，深嵌入 Coq 中。优化及其他变换被写成 Coq 函数，并针对 SQIR 程序的语义证明其正确性。SQIR 采用复数矩阵语义，这是量子计算的标准语义，但以符号方式处理矩阵，以便对使用任意数量量子比特的程序进行推理。SQIR 的精心设计及所提供的自动化使 VOQC 能够编写并验证广泛的优化，包括来自前沿优化器的完整电路变换。
We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.
@article{paperbot1174,
title = {A verified optimizer for Quantum circuits},
author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434318}
}