TY - JOUR T1 - Quantitative Robustness Analysis of Quantum Programs (Extended Version) JF - Proc. ACM Program. Lang. Y1 - 2018 A1 - Shih-Han Hung A1 - Kesha Hietala A1 - Shaopeng Zhu A1 - Mingsheng Ying A1 - Michael Hicks A1 - Xiaodi Wu AB -

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.

VL - 3 U4 - Article 31 UR - https://arxiv.org/abs/1811.03585 CP - POPL U5 - https://doi.org/10.1145/3290344 ER -