发表机构
Shenzhen University of Advanced Technology; Guangdong Provincial Key Laboratory of Computility Microelectronics; Pengxin Quantum Technology (Shenzhen) Co., Ltd.; Sun Yat-sen University（深圳先进技术大学; 广东省计算微电子重点实验室; 鹏芯量子技术（深圳）有限公司; 中山大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究提出用可证明大小的证书检验量子码参数，将距离判定转为可验证计算，在环面码上提速并覆盖多码族。
AI 中文摘要
一个码由三个数描述：其物理量子比特数、逻辑量子比特数，以及其无法检测的最小错误（以量子比特计）。前两者是线性代数问题。第三个，即距离，是在一个指数级大的集合上的最优值，由求解器读出，而求解器的答案不附带证书。一个码的参数能否在码之间统一检验，并附带一个已证明大小的证书，这一问题尚未解决。这里我们证明它们可以，方法是将工作单元从码转移到\f{证书}，一个短对象，可以是列表、配对或符号实例，其正确性由\f{Lean}证明助手的内核通过计算决定。内核是检查每一步的小核心。证书的大小本身是一个定理：其枚举形式列出权重低于距离$d$的向量，共$\binom{n}{j}$个（$j<d$），在固定距离$d$下，这是码长$n$的多项式。没有在$n$和$d$上对码统一的界限比这更小。对于乘积族，证书更小，界限只需符号性地证明一次。判定一个向量位于校验矩阵的行空间（即其行的和集）之外，变成一次矩阵-向量乘积和一次内积。在一个十八量子比特的环面码（一种闭合为环面的表面码）上，该决策的整文件检查从42秒降至9秒。随后有十一个码族和三十九个参数集，最宽达1872量子比特。除了\f{Lean}逻辑的三个标准公理外，没有信任任何其他内容，尽管生成码校验的生成器止步于二十量子比特，且144量子比特码的下界是导入而非在此证明的。距离变得可检验而非仅被相信，同样的方法适用于任何计算以求解器结束的其他地方。
英文摘要
Quantum error correction protects quantum information by encoding it in a code described by three numbers: how many physical qubits it uses, how many logical qubits it protects, and the smallest error it cannot detect. The last is an optimum over exponentially many candidates, so it is read off a solver rather than checked. Here we show that code parameters can be certified by a short certificate, a list or a pairing or a symbolic instance, whose correctness the kernel of a proof assistant decides by computation, and whose size is itself a theorem rather than an estimate. Two published code families have distances settled here: the bivariate bicycle code's $[[144,12,12]]$, certified, and the affine-permutation codes printed at $[[1152,580,\le 12]]$ and $[[2304,1156,\le 14]]$, settled at twelve and fourteen. Eleven code families and thirty-nine parameter sets follow, with nothing beyond three standard axioms trusted and the pipeline's specification step preset to twenty columns.
