Quantum code parameters, checkable by a certificate of provable size

技術要約：証明可能なサイズの証明書によって検証可能な量子符号パラメータ

問題提起
量子誤り訂正符号は、物理量子ビット数 ($n$)、論理量子ビット数 ($k$)、および符号距離 ($d$) という3つのパラメータによって特徴付けられる。$n$ と $k$ は線形代数（具体的にはパリティ検査行列のランク）によって決定されるが、$d$ は論理演算子の最小重みとして定義される。$d$ の決定は、チェック行列のカーネル内にある、他のチェック行列の行空間に含まれない最も軽いベクトルを見つける問題である。これは、指数関数的に巨大な集合 ($2^n$) 上の最適化問題である。

現在、$d$ は通常、外部ソルバー（混合整数計画法やSATソルバーなど）によって決定されている。これらのソルバーは数値的な回答を提供するが、信頼できる論理的枠組み内で独立して検証可能な「正当性の証明書」を提供することはない。その結果、量子誤り訂正における閾値の主張は、しばしば未検証のソルバーの出力に依存している。本論文は、証明助手（proof assistant）のカーネル内でのみ検証が行われる、証明可能なサイズの証明書を用いて、異なる符号間で一様に符号パラメータをチェックできるかという未解決の問いに取り組んでいる。

手法
著者らは、Lean 証明助手に実装された検証フレームワークを提案している。核心となる戦略は、検証の単位を符号そのものから、Lean の信頼できるカーネル内で正当性が決定される短いオブジェクトである「証明書（certificate）」へと移行させることである。この手法は、主に以下の3つのメカニズムに基づいている。

1. 行簡約とランクの証明:
   パリティ検査行列 ($H_X$ および $H_Z$) のランクは、カーネル内でのガウス消去法（行簡約）による直接的な計算によって証明される。スケーラビリティに対処するため、著者らは「アペンドオンリー（追加型）」のエシュロン形式ルーチンを利用している。標準的な後退代入は、幅の広い行列に対してスケーリングが悪化する（$O(n^3)$ またはそれ以上）が、この追加型バリアントは、ランク判定とメンバーシップ判定に十分な弱い不変量を維持することで、カーネルがより広い行列を効率的に処理することを可能にする。

2. 上界のための双対ウィットネス:
   特定のベクトル $v$ が論理演算子であること（すなわち $v \in \ker H$ かつ $v \notin \text{rowspace } H$ であること）を証明するために、高コストな行空間へのメンバーシップチェックを**双対ウィットネス（dual witness）**に置き換える。ウィットネス・ベクトル $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 の論理における 3 つの標準的な公理のみが使用される。
• 証明書設計によるスケーラビリティ: 行簡約から双対ウィットネスへ、あるいは列挙から記号的証明へと証明書の形式を変更することで、大幅な性能向上を実現している。例えば、18 量子ビットのトーリック符号におけるメンバーシップ判定のチェックは、行簡約から双対ウィットネスに切り替えることで、42 秒から 9 秒へと短縮された。
• 証明書サイズの定理: 著者らは、列挙証明書のサイズが $d$ が固定されている場合に $n$ の多項式であること、具体的には $\sum_{j<d} \binom{n}{j}$ であることを証明した。これにより、証明書は探索空間全体よりも厳密に小さいことが確立された。

結果
著者らは、11 の符号族および 39 のパラメータセットを検証した。最大規模のインスタンスは、$n = 1872$ 個の物理量子ビット（$d=7$）に達した。

• インスタンス: データセットには、古典符号（ハミング符号、反復符号）、CSS 符号（Steane 符号、Shor 符号、Bivariate Bicycle 符号のような $[[144, 12, 12]]$）、およびハイパーグラフ積符号が含まれる。
• パフォーマンス: 「アペンドオンリー」の行簡約ルーチンにより、カーネルは gauged bivariate bicycle コード $[[24, 3, 4]]$ のランクと距離を数秒から数分で検証できた。一方で、標準的な簡約では実用的な時間内に終了できなかった。
• 探索パイプライン: 44 個のシードグラフに対して探索パイプラインを実行し、990 組のペアを生成した。そのうち 903 個の候補を承認し、259 個については緩和された基準で距離の下界を閉じた（891 個は緩和基準による）。このパイプラインは、大規模なインスタンスでの列挙を避けるため、パスおよび巡回家族に対する記号的定理を利用した。
• 比較: 本論文は、探索パイプラインが既存の公開された符号よりも優れたパラメータを持つ符号を発見しなかったことを指摘している。その価値は、パラメータの最適化ではなく、パラメータの「検証可能性」にある。

意義と主張
本論文は、量子符号のパラメータを「信じられるもの」から「チェック可能なもの」にする問題を解決したと主張している。

• 信頼性: 検証は Lean カーネルと 3 つの標準的な公理のみに依存しており、外部ソルバーの出力を信頼する必要を排除している。
• 効率性: 証明書ベースの検証への移行により、基礎となる探索空間が指数関数的である場合でも、符号パラメータのチェックコストを管理可能なものにしている。
• 汎用性: この手法は特定の符号族に限定されず、パリティチェックによって指定されるあらゆる符号に適用できる。記号的ルートは、これを大規模な積家族へと拡張する。
• 限界: 著者らは、提供されていない事項についても明示している：
  • $[[144, 12, 12]]$ 符号の下界は、この研究内でゼロから証明されたものではなく、独立した各家族の定式化から「転送」されたものである。
  • $[[144, 12, 12]]$ インスタンスに対するソルバーの証明の完全なステップバイステップの再生は、時間的制約（推定 37～44 日間のカーネル実行時間）のため、現在は困難である。
  • 本手法は、シード行列のカーネルが非自明であることを前提としている。カーネルが自明である場合、距離の下界の証明は失敗する可能性がある。
  • 探索パイプラインは、より良いパラメータを持つ新しい符号を見つけることを目的としているのではなく、既存の候補を証明するためのものである。

結論として、本研究は、量子符号の距離がソルバーからのブラックボックスの結果ではなく、検証可能な多項式サイズの証明書を持つ定理となるフレームワークを確立しており、量子誤り訂正における閾値の主張の根拠を根本的に変えるものである。