Quantum code parameters, checkable by a certificate of provable size

技术摘要：可由可证明大小证书验证的量子码参数检查

问题陈述
量子纠错码由三个参数表征：物理量子比特数 ($n$)、逻辑量子比特数 ($k$) 和码距 ($d$)。虽然 $n$ 和 $k$ 是由线性代数（具体为校验矩阵的秩）确定的，但 $d$ 被定义为逻辑算子的最小权重。确定 $d$ 涉及寻找校验矩阵核（kernel）中不在另一个校验矩阵行空间中的最轻向量。这是一个在指数级庞大集合 ($2^n$) 上的优化问题。

目前，$d$ 通常由外部求解器（例如混合整数规划或 SAT 求解器）来确定。这些求解器提供数值答案，但没有可以在受信任逻辑框架内独立验证的正确性证书。因此，量子纠错中的阈值声明往往依赖于未经验证的求解器输出。本文探讨了一个开放性问题：是否可以使用具有可证明大小的证书，在不同代码之间统一检查代码参数，且验证过程完全在证明助手的核（kernel）内进行。

方法论
作者提出了一个在 Lean 证明助手 中实现的验证框架。其核心策略是将验证单元从代码本身转向证书——一个其正确性由 Lean 可信核内的计算决定的短小对象。该方法依赖于三种主要机制：

1. 行归约与秩认证：
   通过在核内直接执行高斯消元法（行归约）来认证校验矩阵（$H_X$ 和 $H_Z$）的秩。为了处理可扩展性问题，作者利用了一种“仅追加式”（append-only）阶梯形式例程。与扩展性较差的标准回代法（对于宽矩阵其复杂度为 $O(n^3)$ 或更高）不同，这种仅追加变体维持了一个足以进行秩和成员测试的较弱不变性，使得核能够高效处理更宽的矩阵。

2. 用于上界的对偶见证（Dual Witnesses）：
   为了认证特定向量 $v$ 是一个逻辑算子（即 $v \in \ker H$ 且 $v \notin \text{rowspace } H$），该方法使用对偶见证取代了昂贵的行空间成员检查。提供的见证向量 $w$ 满足 $Hw = 0$（属于核）且 $w \cdot v = 1$（与 $v$ 非平凡配对）。根据线性代数，如果 $w$ 与整个行空间正交但不与 $v$ 正交，那么 $v$ 就不可能在行空间内。这把验证成本降低为一次矩阵-向量乘法和一次内积运算，避免了完整的行归约。

3. 用于下界的证书形式：

   • 枚举路径： 对于 $d$ 相对于 $n$ 较小的代码，下界通过枚举所有权重小于 $d$ 的向量来进行认证。证书是该列表中不可检测逻辑算子的空集。该列表的大小为 $\sum_{j<d} \binom{n}{j}$，对于固定的 $d$，它是 $n$ 的多项式级别，而非指数级 ($2^n$)。
   • 符号/结构化路径： 对于乘积族代码（如超图积码），下界通过使用“清洗论证”（cleaning argument）进行符号化证明。该论证表明任何低权重的逻辑算子都可以被约减为一个稳定子。这种证明针对族参数是一次性建立的，特定的实例仅为该定理的实例化，从而避免了候选生成。

核心贡献

• 统一验证： 本文证明了可以使用证书而非依赖求解器输出，在不同代码族之间统一验证代码参数。
• 仅核验证： 整个验证过程，包括问题的规约和证书的检查，都发生在 Lean 核内。没有任何外部求解器或不受信任的编译器属于可信基，仅使用了 Lean 逻辑中的三个标准公理。
• 通过证书设计实现可扩展性： 通过改变证书形式（例如，从行归约转向对偶见证，或从枚举转向符号证明），作者实现了显著的性能提升。例如，将检查一个 18 量子比特托里码（toric code）的成员断言从行归约切换到对偶见证时，耗时从 42 秒降至 9 秒。
• 证书大小定理： 作者证明了对于固定的 $d$，枚举证书的大小是 $n$ 的多项式，即 $\sum_{j<d} \binom{n}{j}$。这确立了证书严格小于完整搜索空间。

结果
作者验证了 11 个代码族 和 39 个参数集，其中最大的实例达到了 $n = 1872$ 个物理量子比特（$d=7$）。

• 实例： 数据集包括经典码（汉明码、重复码）、CSS 码（Steane 码、Shor 码、双变量双循环码如 $[[144, 12, 12]]$）以及超图积码。
• 性能： “仅追加式”行归约例程使得核能够在数秒和数分钟内验证 gauged bivariate bicycle 码 $[[24, 3, 4]]$ 的秩和距离，而标准归约法在实际时间内无法终止。
• 搜索流水线： 在 44 个种子图上运行了发现流水线，生成了 990 对结果。它接受了 903 个候选者，并封闭了其中 259 个的距离上界（使用放宽标准后为 891 个）。该流水线利用路径族和循环族的符号定理来避免大规模实例的枚举。
• 对比： 文中指出，搜索流水线并未发现比现有已发表代码更好的参数；其价值在于参数的可检查性，而非参数优化。

意义与主张
本文声称解决了使量子码参数变得“可检查而非仅凭相信”的问题。

• 信任： 验证仅依赖于 Lean 核和三个标准公理，消除了对外部求解器输出的信任需求。
• 效率： 向基于证书验证的转变使得检查代码参数的成本变得可控，即使对于底层搜索空间呈指数级的代码也是如此。
• 通用性： 该方法不局限于特定的代码族；它适用于任何由校验矩阵指定的代码。符号化路径将其扩展到了大型乘积族。
• 局限性： 作者明确说明了本文未交付的内容：
  • $[[144, 12, 12]]$ 码的下界是从一个独立的逐族形式化中“迁移”而来的，而非在本研究中从头证明。
  • 由于时间限制（估计需要 37–44 天的核时间），目前尚无法对 $[[144, 12, 12]]$ 实例的求解器证明进行完整的逐步重演。
  • 该方法假设种子矩阵的核是非平凡的；如果核是平凡的，则距离上界可能会失效。
  • 搜索流水线并不声称发现新的最优码，而是旨在认证现有的候选码。

总之，这项工作建立了一个框架，使得量子码的距离不再是来自求解器的黑盒结果，而是一个具有可验证的多项式大小证书的定理，从根本上改变了量子纠错中阈值声明的基础。