Analyzing Decoders for Quantum Error Correction

TL;DR

This paper introduces a formal, systematic method for evaluating quantum error correction decoders, providing more reliable and efficient analysis than traditional Monte Carlo simulations, especially at low error rates.

Contribution

We develop a formal semantics for QEC programs and a verifier that quantifies decoder accuracy and robustness, outperforming simulation in certain regimes.

Findings

Our approach outperforms Monte Carlo simulation at low error rates.

The verifier can quantify decoder robustness across a range of physical error rates.

The formal semantics provides a solid foundation for fault-tolerant quantum system design.

Abstract

Quantum error correction (QEC) enables reliable computation on noisy hardware by encoding logical information across many physical qubits and periodically measuring parities to detect errors. A decoder is the classical algorithm that uses these measurements to infer which error most likely occurred, so that the system can correct it. The decoder's accuracy-how rarely it makes the wrong guess-directly determines the scale of quantum computation that can be reliably executed. With a wealth of competing decoding algorithms, a QEC system designer needs reliable methods to evaluate them. Today, the dominant approach is to evaluate decoders using Monte Carlo simulation. However, simulation has several drawbacks such as requiring many samples to produce low variance estimates. In this work, we develop a new systematic analysis for evaluating decoders. We introduce a novel formal semantics of a core language for QEC programs that captures the de facto standard Stim circuit format, providing a principled theoretical foundation for the emerging space of fault-tolerant quantum systems design. Given a QEC program and a decoder, our verifier can quantify both the decoder accuracy and the decoder robustness to drift in physical error rate. Our approach has two key components: (i) a structured search over the space of possible errors; and (ii) a constrained polynomial optimization kernel. A thorough empirical evaluation of our approach suggests that it can outperform simulation, especially in low error rate regimes, and that it can be deployed to quantify decoder robustness over an interval of physical error rates.