一句话：提出 Coq 中实现的高保障框架 VQO，形式验证从 OQIMP 到 OQASM 再到 SQIR 的量子 oracle 编译器，并用 QFT 降低量子比特开销。
量子算法常需在经典数据的量子叠加态上执行算术、谓词判定等经典运算，这类 oracle 往往是量子程序中最大的组成部分。为便于构造高效且正确的 oracle，本文提出 VQO——一个用 Coq 证明助手实现的高保障框架。其核心是 oracle 量子汇编语言 OQASM：借助量子傅里叶变换在两个基之间移动量子比特，从而支持重要优化，同时不引入纠缠及其导致的指数级膨胀。该设计使作者得以证明 VQO 两条编译路径的正确性（OQIMP 到 OQASM、OQASM 到通用量子汇编语言 SQIR），并用 QuickChick 基于性质的测试框架高效检验 OQASM 程序性质。作者用 VQO 实现了 Shor 与 Grover 算法所需的多类算术与几何算子，发现基于 QFT 的算术 oracle 所需量子比特少于（有时远少于）用“经典”门构造的版本；而后者在量子比特与门数上也不逊于甚至优于未经验证的先进量子编程平台 Quipper 所生成的 oracle。
Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the largest components of a quantum program. To ease the construction of efficient, correct oracle functions, this paper presents VQO, a high-assurance framework implemented with the Coq proof assistant. The core of VQO is OQASM, the oracle quantum assembly language. OQASM operations move qubits between two different bases via the quantum Fourier transform, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM’s design enabled us to prove correct VQO’s compilers—from a simple imperative language called OQIMP to OQASM, and from OQASM to SQIR, a general-purpose quantum assembly language—and allowed us to efficiently test properties of OQASM programs using the QuickChick property-based testing framework. We have used VQO to implement a variety of arithmetic and geometric operators that are building blocks for important oracles, including those used in Shor’s and Grover’s algorithms. We found that VQO’s QFT-based arithmetic oracles require fewer qubits, sometimes substantially fewer, than those constructed using “classical” gates; VQO’s versions of the latter were nevertheless on par with or better than (in terms of both qubit and gate counts) oracles produced by Quipper, a state-of-the-art but unverified quantum programming platform.
@article{paperbot1428,
title = {Verified compilation of Quantum oracles},
author = {Liyi Li and Finn Voichick and Kesha Hietala and Yuxiang Peng and Xiaodi Wu and Michael Hicks},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563309}
}