一句话：为含噪量子 while 程序建立语义与逻辑，定义并证明 ε-鲁棒性，支持纠错方案分析。
量子程序执行时不可避免地受到量子噪声影响，而架构级纠错代价高昂，因此亟需在程序层面推理错误行为的方法。本文为含错量子 while 程序建立操作语义，并给出一种程序逻辑，用于证明作者提出的 ε-鲁棒性：理想程序与含错程序之间可能距离的定量刻画。作者证明了该逻辑的可靠性，并通过案例研究展示其实用性：分析量子伯努利工厂（QBF）与量子游走（QW）含噪版本的鲁棒性，比较不同纠错方案对单量子比特错误的有效性，并分析容错版 QBF 的鲁棒性。
Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called є-robustness, which characterizes possible “distance” between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF.
@article{paperbot645,
title = {Quantitative robustness analysis of quantum programs},
author = {Shih-Han Hung and Kesha Hietala and Shaopeng Zhu and Mingsheng Ying and Michael Hicks and Xiaodi Wu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290344}
}