技術要約：量子誤り訂正のためのパラメトリックな証明付きコンパイル

問題表明

ショアの素因数分解アルゴリズムのような長時間の量子計算には、ノイズのある物理操作にもかかわらず、信頼できる論理量子ビットが必要です。量子誤り訂整（QEC）は、論理情報を複数の物理量子ビットに符号化することで、誤りの検出と訂正を行います。しかし、スタビライザーを測定するためのシンドローム抽出回路自体が、誤りを導入することもあります。アンシラ量子ビットにおける単一の故障は、複数のデータ量子ビットへと伝播し、「フックエラー（hook errors）」を引き起こす可能性があります。これらは論理エラーを模倣したり、データエラーの証拠を打ち消したりすることがあります。

解決すべき中心的な課題は、回路レベルの符号距離（$d_{circ}$）を確立することです。これは、検出器を作動させることなく論理データエラーを引き起こすために必要な、注入されたパウリ故障の最小数として定義されます。符号の計算は一般にNP困難です。さらに、QEC符号は（異なる距離 $d$ を持つ表面符号のように）符号のファミリーとして存在しており、$d$ を増やすと量子ビット、スタビライザー、ゲートの数も変化します。従来の検証手法では、多くの場合、各特定の実装に対して特性を再証明する必要があり、その証明は $d$ に伴って増大してしまいます。著者らは、特定の符号距離 $d$ に依存せず、異なるシンドローム抽出スキーム（Standard, Flag, Shor, Knell）を考慮した、符号ファミリー全体に対する有限かつパラメトリックな証明を求めています。

手法：PC-QEC フレームワーク

著者らは、抽出回路とともにシンボリックな証明をコンパイルするフレームワークである PC-QEC（Parametric Proof-Carrying Quantum Error Correction）を提案しています。このアプローチは、高レベルの符号代数と、故障伝播の詳細な実装を分離します。

1. 3層アーキテクチャ

本フレームワークは、3つの異なる層にわたって動作します。

• CodeML (ソース): 符号ファミリーを順序付きパウリ因子を用いて記述するパラメトリックな言語です。スタビライザーとその結合次数（例：$Z_0 Z_3 Z_1 Z_4$）を記号的に定義します。符号の適格性に関する代数的前提および論理エラーの幾何学的特性を提供します。
• QStab (中間表現): 残留データエラー、読み出しオフセット、およびスタビライザー測定境界における故障予算を追跡する中間表現（IR）です。これは、残留エラーの「カット・シグネチャ（cut signatures）」と故障数（$\ell$）を関連付けるプログラム不変量を確立します。
• QClifford (ターゲット): 明示的な故障サイトを持つ、放出されたクリフォード回路（アダマール、CNOT、測定）です。これは、故障を考慮したホーア論理（Hoare logic）を用いて、QStabで確立された不変量をゲートレベルの実装が保持していることを検証します。

2. コアメカニズム：カット・シグネチャ

鍵となる革新は、論理エラーとフックエラーを区別するための**パリティプローブ（カット）**の使用です。

• 論理エラー: 表面符号において、論理エラー（例：$Z$ エラーの列）は、特定のコレクション（例：すべての列）におけるすべての $d$ 個のカットを横切ります。
• フックエラー: アンシラの故障によって引き起こされるフックエラーは、各コレクションにおいて最大で1つのカットのみを横切ります。これは、アンシラへのデータ量子ビットの結合順序（例：同じ列にある量子ビットをペアにする）を注意深く制御することで実現され、それらの寄与がカット・シグネチャ内で相殺され、最大で1つの未相殺の寄与のみが残るように設計されています。

この証明は、主に2つの特性に基づいています。

1. 符号代数: すべての論理エラーは、あるコレクションにおいて少なくとも $d$ 個のカットを横切らなければなりません。
2. プログラム不変量: $\ell < d$ の故障がある場合、残留エラーは任意のコレクションにおいて最大で $\ell$ 個のカットしか横切ることができません。

$\ell < d$ であるため、不変量は残留エラーが論理エラーの条件を満たすことができないことを保証します。

3. 証明付きコンパイル

システムは、 $d$ に依存しないサイズの有限なシンボリック証明書を生成します。

• 帰納法: 特定の $d$ に対してゲートを列挙する代わりに、証明は符号距離およびスタビライザー測定の数に関する帰納法を使用します。
• シンボリック境界: 証明は、カット・シグネチャと故障数のシンボリックな式を追跡します。
• 翻訳: コンパイラは、ソースの不変量（QStab）をターゲットのホーア証明（QClifford）へと翻訳します。その際、各ゲートと故障サイトが、まだアンシラ量子ビットから完全に伝播されていない「保留中」の寄与を考慮しつつ、カットの境界を保持していることを検証します。

主な貢献

1. パラメトリックな証明付きコンパイル: PC-QECは、あらゆる正当な符号距離 $d$ に対して有効な、符号ファミリー全体の回路レベルの符号距離に関する有限かつシンボリックな証明を提供する初のフレームワークです。
2. ユニバーサルなスキーム・サポート: 本フレームワークは、4つの主要なシンドローム抽出スキーム（Standard, Flag, Shor, Knell）をカバーしており、同じ高レベルの証明構造を異なるバックエンド実装に適応できることを示しています。
3. 回路レベルの距離保証: 著者らは、回転表面符号（Rotated Surface code）において、Standard Schemeの下で奇数の $d$ に対して $d_{circ} = d$ であることを証明しました。また、他のファミリー（Hypergraph-Product, Toric, Triangular Color code）についても下限値を提供しています。
4. 機械化されたメタ理論: 標準的な表面、HGP、およびToric符号のファミリーに対するアプローチの健全性と正確性は、Lean 4 で機械化されています。
5. 効率的な検証: 著者らは、符号ファミリー（例：回転表面符号のすべての奇数 $d \ge 3$）のシンボリック証明書のチェックが、有限の時間（平均214秒）で行われ、特定の $d$ ごとに証明を再実行する必要がないことを示しています。

結果

評価は5つの符号ファミリーと複数の抽出スキームを対象としています。

• 回転表面符号 (Rotated Surface Code): Standard Schemeの下で、すべての奇数 $d \ge 3$ に対して $d_{circ} = d$ であることを証明しました。シンボリック証明書のチェックは平均214秒で完了します。
• その他のファミリー:
  • 非回転表面符号およびToric符号: $d_{circ} = d$ を証明。
  • Cartesian LP符号: $d_{circ} = 4t$ （$t$ はパラメータ）を証明。
  • 三角形カラー符号 (Triangular Color Code): 減少した重みの不変量により、下限値 $\lceil d/3 \rceil$ を証明。
• 有限のインスタンス: システムは、5量子ビット、Steane、およびShor符号などの有限の回路を正常に検証し、結合順序（例：結合の順序）といった抽出の選択が、証明された距離にどのように直接影響するかを示しました。例えば、Shor符号の結合順序をブロック型からインターリーブ型に変更することで、距離が1から3へと回復しました。
• パフォーマンス: 有限のターゲット回路のチェック時間は0.2〜0.5秒でした。最も複雑なシンボリックチェック（Cartesian LPおよびColor符号）は数千秒を要しましたが、これは回路のサイズではなく、代数的前提の複雑さを反映したものです。

意義と主張

本論文は、PC-QECが高レベルの符号代数と低レベルの回路のフォールトトレランス（耐故障性）の間の溝を埋めるものであると主張しています。符号の幾何学的な論理エラー特性の証明と、故障伝播に関する実装固有の証明を分離することで、本フレームワークはQEC回路のスケーラブルなテストと形式検証を可能にします。

著者らは、彼らのアプローチが、新しい符号サイズごとに距離を再証明する必要なく、スケーラブルなテストツール（ScaLERなど）に対して距離の前提を正当化する有限のシンボリック証明書を提供することを強調しています。本研究は、符号のファミリーと抽出スキームが特定の代数的および順序的契約に従っている限り、無限の符号ファミリーの回路レベルの距離を、固定サイズの証明を用いて検証することが可能であることを実証しています。本論文は、論理エラー率を数値的に最適化することを目的としているのではなく、宣言された故障および読み出しの契約の下で、回路レベルの距離が理論的な符号距離を満たすことを厳密に、機械的に検証された保証を提供することを目的としています。