Quantitative Robustness Analysis of Quantum Programs (Extended Version)

Abstract

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 $\epsilon$-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.

34 pages, LaTeX; v2: fixed typos

References in corpus (13)

• Surface codes: Towards practical large-scale quantum computation
• Quantum Simulation
• Quantum Error Correction for Quantum Memories
• Randomized Benchmarking of Quantum Gates
• Prescription for experimental determination of the dynamics of a quantum black box
• Robust randomized benchmarking of quantum processes
• Distance measures to compare real and ideal quantum processes
• Scalable Noise Estimation with Random Unitary Operators
• Q#: Enabling scalable quantum computing and development with a high-level domain-specific language
• A functional quantum programming language
• Approximation of real error channels by Clifford channels and Pauli measurements
• Comparing the Overhead of Topological and Concatenated Quantum Error Correction
• Simpler semidefinite programs for completely bounded norms

Cited by in corpus (7)

• Statistical Assertions for Validating Patterns and Finding Bugs in Quantum Programs
• Quantum Hoare logic with classical variables
• Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
• On the Principles of Differentiable Quantum Programming Languages
• Enabling Accuracy-Aware Quantum Compilers using Symbolic Resource Estimation
• Verifying Fault-Tolerance of Quantum Error Correction Codes
• Automating Equational Proofs in Dirac Notation