High-Rate Quantum Codes with Proven Distance and Low-Weight Measurements

技術要約：距離の証明と低重み測定を伴う高レート量子符号

問題提起
本論文は、量子誤り訂正における3つの重要なパラメータ間の根本的なトレードオフに対処している。それは、符号化率（データ量子ビットに対する保護された論理量子ビットの数）、符号距離（検出不可能な論理エラーの最小重み）、および測定重み（単一の測定演算子が触れるデータ量子ビットの数）である。サブシステム符号は、重いスタビライザー測定をより軽い非可換なゲージ測定に置き換えるメカニズムを提供するが、そのような符号の正確な距離（特に、ゲージ演算子による乗算を考慮した「ドレス（dressed）」距離）を決定することは、数値探索を必要とするか、あるいは一般的な族に対して厳密な証明を欠くことが多い。著者らは、矩形格子上で、明示的かつ証明されたパラメータを持つ、低重み測定を備えた高レート符号の構成を求めている。

手法
著者らは、次元 $L$ の矩形座標格子（各辺の長さ $q_i \ge 4$ は偶数）上で定義される、RLG($q_1, \dots, q_L$) と表記される量子サブシステム符号の族を研究している。

• 構成: この符号は、「座標線」ゲージ演算子を測定することによって定義される。各軸 $i$ に対して、その軸に平行なすべてのラインに沿った $X$ または $Z$ として作用する演算子がゲージ群に含まれる。
• 代数的枠組み: 解析には、パウリ演算子のバイナリ・シンプレクティック記述を利用する。この符号はCSS型であり、ゲージ群は純粋な $X$ 演算子および純粋な $Z$ 演算子によって生成される。著者らは、$\mathbb{F}_2$ 上のテンソル積計算を用いて、ゲージ群およびスタビライザー群のランクを決定する。
• 形式的検証: 手法の重要な部分は、対話型定理証明器である Lean を用いた形式的検証である。著者らは、符号構造を定義し、軸の数に関する帰納法を通じて距離の下界を形式的に証明する Lean モジュール（例：RLG.lean, GridLines.lean）を提供している。このアプローチにより、一般の場合における数値的な距離探索を回避している。
• 最適化: 固定されたデータ量子ビット予算（具体的には $N \le 10,000$）の下で、著者らは偶数の矩形タプルに対する厳密な有限列挙を行い、特定の距離（$D=16, 32, 64$）における符号化率と最大測定重みの間のパレート境界を特定している。

主要な貢献

1. 正確なパラメータ公式: 論文では、任意の有効なタプルの辺の長さに対して、データ量子ビット数 ($N$)、保護された論理量子ビット数 ($K$)、ゲージ量子ビット数 ($g$)、およびドレス距離 ($D$) の閉形式の式を導出している。
   • $N = \prod q_i$
   • $K = \prod (q_i - 2)$
   • $D = 2^L$ （ここで $L$ は軸の数）
   • 最大測定重みは $w = \max_i q_i$ である。
2. 証明されたドレス距離: ヒューリスティックや数値チェックに依存する多くのサブシステム符号の解析とは異なり、本研究はドレス距離が正確に $2^L$ であることを厳密に証明している。この証明は、（ゲージ演算子による乗算後であっても）いかなる非自明な論理演算子も、そのサポートサイズが少なくとも $2^L$ であることを示している。
3. ベア（bare）距離 vs ドレス（dressed）距離: 著者らは、この族において、ベア距離（すべてのゲージと可換な論理演算子の最小重み）も $2^L$ であり、ドレス距離と一致することを証明している。
4. スタビライザー重み解析: 論文は、測定されるゲージ演算子は低重み ($w$) である一方で、非単位元スタビライザー（ゲージラインの積）は最小重み $2^{L-1} \min_i q_i$ を持つことを確立している。これは、ゲージの自由度が直接測定される演算子の重みを軽減するものの、コードに固有の重いスタビライザー制約を排除するわけではないことを強調している。
5. 有限最適化の結果: 10,000 個のデータ量子ビットの予算の下で、著者らは最適な符号構成を特定している。
   • 距離 16: 10,000 個のデータ量子ビットを持つ符号は、重み 10 の測定を使用して 4,096 個の論理量子ビット ($K/N \approx 41\%$) を保護する。
   • 距離 32: 7,776 個のデータ量子ビットを持つ符号は、重み 6 の測定を使用して 1,024 個の論理量子ビット ($K/N \approx 13.2\%$) を保護する。
   • 距離 64: 9,216 個のデータ量子ビットを持つ符号は、重み 6 の測定を使用して 256 個の論理量子ビット ($K/N \approx 2.8\%$) を保護する。

結果と主張
本論文は、この特定の符号族における、この特定の距離（16, 32, 64）での符号化率と測定重みの間の「完全なトレードオフ」を提供すると主張している。結果は、中程度の距離（例：$D=16$）において、比較的低い測定重みで高いレートが達成可能であることを示している。しかし、距離が増加するにつれて、レートは大幅に低下し、軸の数 ($L$) を増やす必要があり、これは（固定された $N$ に対して）距離 ($D=2^L$) を増加させる一方で、レートを減少させる。

著者らは、これらの結果がこの符号族の静的なパラメータに関するものであることを明示している。彼らは、フォールトトレラント回路距離、論理エラー率、または回路レベルのノイズ下での特定のデコーディング性能を確立することを主張していない。また、この構成は「多重ハイパーキューブ（many-hypercube）」符号を拡張するものであるが、すべての偶数矩形タプルを統一的な代数的記述で扱うことで、これまであまり探索されてこなかった混合辺長を許容している。

意義
本研究の意義は、距離の選択を、残りの有限最適化問題から分離できる点にある。距離が軸の数 ($L$) のみに依存し、レートと測定重みが辺の長さ ($q_i$) に依存することを証明することで、著者らはハードウェアの制約（測定重み）と論理的要件（距離とレート）に基づいて符号を選択するための明確な設計空間を提供している。

論文は、「ゲージの自由度」によって重いスタビライザーが運ぶ情報に軽い測定を通じてアクセスできることを強調しているが、同時にその代償も明確にしている。すなわち、スタビライザー制約自体は依然として重い（重み $\ge 2^{L-1} \min q_i$）ということである。したがって、著者らは、この族が漸近的な意味での従来の量子低密度パリティ検査（QLDPC）スタビライザー族（定数レート、線形距離、有界重みを持つもの）ではなく、正確な有限パラメータと特定の最適化ランドスケープを提供するものであると述べている。Lean による形式化の導入は、距離の証明が機械的にチェックされていることを保証しており、数値探索に頼ることなく、主張されたパラメータに対して高度な厳密性を与えている。