Verifying Fault-Tolerance of Quantum Error Correction Codes

TL;DR

This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs by incorporating the techniques of quantum symbolic execution, and provides an automatic verification tool for quantum fault-tolerance.

Abstract

Quantum computers have advanced rapidly in qubit count and gate fidelity. However, large-scale fault-tolerant quantum computing still relies on quantum error correction code (QECC) to suppress noise. Manually or experimentally verifying the fault-tolerance property of complex QECC implementation is impractical due to the vast error combinations. This paper formalizes the fault-tolerance of QECC implementations within the language of quantum programs. By incorporating the techniques of quantum symbolic execution, we provide an automatic verification tool for quantum fault-tolerance. We evaluate and demonstrate the effectiveness of our tool on a universal set of logical operations across different QECCs.

Figures (8)

• Figure 1: Two implementations of multi-qubit Pauli measurement $P_1\otimes P_2\otimes P_3\otimes P_4$.
• Figure 2: Rules for the ideal transition relation. In rule (IN), $\rho_{q:=\lvert0\rangle}= \lvert0\rangle_q\langle0\rvert\rho\lvert0\rangle_q\langle0\rvert+\lvert0\rangle_q\langle1\rvert\rho\lvert1\rangle_q\langle0\rvert$ where we use $\lvert i\rangle_q$ to denote the pure state $\lvert i\rangle$ at qubit $q$ and $\lvert i\rangle_q\langle j\rvert$ is the abbreviation of product of $\lvert i\rangle_q$ and $\,_q\langle j\rvert$; in rule (UT), $U_{\overline{q}}$ means a unitary that acts as $U$ on $\overline{q}=q_i\ldots q_j$, and acts trivially on other qubits.
• Figure 3: Two-party magic state distillation framework with a QECC $\mathcal{C}$ on Bob and a distillation code $\mathcal{D}$ on Alice.
• Figure 4: Comparison of $4$-qubit cat state preparations with different checks. By our verification tool, we found that the first is non-FT and the second is FT.
• Figure 5: An implementation of $8$-qubit cat state preparation. By our verification tool, it is proved to be FT up to $2$ faults but disproved to be FT for $3$ faults.

Theorems & Definitions (57)

• definition thmcounterdefinition
• definition thmcounterdefinition: Syntax of Classical-Quantum Programs (cq-prog)
• definition thmcounterdefinition: Classical-Quantum Configuration
• definition thmcounterdefinition: Faulty Transition
• definition thmcounterdefinition: Transition Tree with Faults
• proposition thmcounterproposition
• definition thmcounterdefinition: Fault-Tolerance of QECC Gadgets
• theorem thmcountertheorem: Discretization of Input Space
• definition thmcounterdefinition: Transition Tree with Pauli Faults
• theorem thmcountertheorem: Discretization of Faults