Kean Chen, Yuhao Liu, Wang Fang, Jennifer Paykin, Xinchuan Ryan Wu, Albert Schmitz, Steve Zdancewic, Gushu Li (Jan 27 2025).
Abstract: Quantum computers have advanced rapidly in qubit number and gate fidelity. However, they would still lack practicalness without utilizing fault-tolerant quantum error correction code (QECC) implementations to suppress noise. Manually or experimentally verifying the fault-tolerance of complex QECCs is impractical due to the vast error combinations. This paper formalizes fault-tolerance 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.
