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.

翻译：量子纠错（QEC）通过在多个物理量子比特上编码逻辑信息并定期测量奇偶性来检测错误，从而实现对噪声硬件的可靠计算。解码器是利用这些测量值推断最可能发生的错误、以便系统进行纠正的经典算法。解码器的准确性——即其做出错误推测的概率——直接决定了可可靠执行的量子计算的规模。面对众多竞争性解码算法，QEC系统设计者需要可靠的方法来评估它们。当前主流方法是通过蒙特卡洛模拟来评估解码器，但模拟存在诸多缺陷，例如需要大量样本才能获得低方差估计。本研究开发了一种用于评估解码器的新型系统分析方法。我们为QEC程序的核心语言引入了新颖的形式语义，该语义能够捕捉事实上的标准Stim电路格式，为新兴的容错量子系统设计空间提供了理论化的基础。给定QEC程序和解码器后，我们的验证器能同时量化解码器的准确度及其对物理错误率漂移的鲁棒性。该方法包含两个关键组件：（i）对可能错误空间的结构化搜索；（ii）约束多项式优化内核。全面的实证评估表明，我们的方法可优于模拟，尤其在低错误率场景中表现突出，并且能够用于量化解码器在物理错误率区间上的鲁棒性。