量子科技中心_量科网

量子纠错码（QECC）位于嘈杂量子硬件与可靠计算之间，因此实践中使用的码参数必须可信。衡量一个码强度的单一指标是它的距离，但验证距离下界在一般情况下是NP难问题，这使得它既无法通过纸笔证明，也无法直接通过证明助手脚本完成。因此，文献中的距离值要么来自非规模化的手工证明，要么来自未经验证的求解器，这在码本该提供保证的地方留下了信任缺口。该团队提出Lean-QEC，这是第一个Lean 4稳定子码理论的形式化实现，能够提供工业级码规模下端到端、机器验证的距离证书。Lean-QEC形式化了量子比特状态的线性代数、泡利群、稳定子码、二进制辛表示、经典编码理论，以及CSS和双变量循环码族。为了突破组合爆炸的障碍，Lean-QEC通过一个经过验证的归约过程将距离条件转化为布尔可满足性公式。该流水线通过一种用BitVec扁平化编码替代Lean的矩阵表示的方法实现扩展，并采用一种错误定位编码将变量数量从 \( n \) 减少到 \( k\lceil \log_2 n\rceil \)。借助这些方法，该团队为双变量循环码族和广义循环码族中一系列工业可行的qLDPC码自动生成了Lean验证的距离证明，包括[[90, 8, 10]]和[[70, 6, 9]] BB码，该形式化方法在Lean内核之外可扩展到144个量子比特。最终生成的库是可复用的，并设计为可嵌入更广泛的基于Lean的端到端容错量子计算验证工作。