A subexponential algorithm for the erasure logical error rate of sparse stabilizer codes

Abstract

How well a quantum error-correcting code protects against the loss of qubits is measured by the logical error rate I_H(p) of the optimal erasure decoder, as a function of the loss probability p. For a stabilizer code on n qubits this is an average over all 2^n erased sets; it is exponentially small at the loss rates of interest, where simulation sees no failures, and we know of no algorithm faster than enumeration. We show that the whole curve can be computed to relative accuracy with a SAT solver, using polynomially many satisfiability questions about formulas whose size is linear in the size of the code. Precisely, let H be a sparse check matrix and F_H = 1 - I_H the optimal entanglement fidelity. For any bounded-density 3-SAT algorithm with time poly * T(v) and polynomial space, a randomized algorithm computes, in time poly(input, 1/eps, log(1/delta)) * T(O(n)) and polynomial space, a monotone polynomial that approximates both I_H and F_H to relative error eps, simultaneously at every p in [0,1], with probability 1 - delta. Two features separate this from approximate counting with an oracle. The logical error rate is itself a projected count, through a second certificate complementary to the one for the fidelity, which gives relative accuracy in the tail that matters; and every query has O(n) variables, without which a subexponential SAT algorithm would yield nothing. With the machine-checked subexponential 3-SAT algorithm of OpenAI the running time is poly * 2^O(n (log log n)^2 / sqrt(log n)) with polynomial space, unconditionally, and the reduction, the engine and their composition are kernel-checked in one Lean 4 development with standard axioms only. Conversely, any output meeting the guarantee determines the code distance, and so does a single value of I_H at a small explicit p known up to an exponential factor; the task is therefore NP-hard already for sparse codes. The speed-up is asymptotic; for codes of practical size we combine the same certificate with sampling and compute logical error rates down to 10^-28 for surface, toric and bivariate bicycle codes of up to 128 qubits, with the distance, the minimum-size failure sets and the leading coefficient certified by proof-checked SAT refutations. The reduction extends to correlated erasures generated by linear-size circuits from latent bits in a fixed number of probability classes. The Lean development, code and data are available at https://github.com/Oliverds321/stabilizer-erasure-sat-lean.

Keywords