量子コンピュータの誤り訂正には、「この符号なら情報を守れる」「装置を大きくすると、守れる情報量も増える」といった多くの数学的な結果が使われます。ただし、ある論文の結論を次の設計へ持ち込むには、符号の定義だけでなく、その結論が成立する前提も引き継がなくてはなりません。
Keming He氏らは2026年11月3日、この理論のつながりを証明支援系Leanで扱うライブラリ「QECert」をプレプリントで紹介しました。基本的な誤り訂正条件から符号の構成、大きな符号の性質、配置に伴う制約までを、共通の定義に基づいて組み合わせる取り組みです。公開された証明コードからは、どこまでが結論で、何が前提として残るのかも確認できます。
簡単にまとめると？
- QECertは、量子誤り訂正の定義や定理をLeanで記述し、別の研究でも再利用できるようにつなぐ公開ライブラリです。
- 大規模化に適した量子LDPC符号を扱いますが、一部の定理はグラフの性質を外部の前提として受け取ります。「形式化済み」という言葉だけで、すべての前提まで証明されたとは判断できません。
- 符号の数学的な性能、量子ビットの配置、実機の雑音や動作時間は別の確認事項です。公開コードは理論を調べる入口になり、装置の性能測定に代わるものではありません。
証明を、次の研究で使える部品にする
Leanでは、まず対象とするものを定義し、その対象についての主張と証明を書きます。論文中で「この式から従う」と省略されがちな段階も、検査できる形でつなげます。証明を組み立てるための機能が出した結果は、Leanの中核にある検査部分によって確かめられます。
QECertは数学ライブラリMathlibを土台に、量子状態、量子チャネル、測定といった基本要素をそろえています。量子チャネルは、雑音を受ける変化や情報を回復する操作を表す数学的な枠組みです。そこへ、誤りを検出する検査の組で定まるスタビライザー符号や、二種類の古典符号を組み合わせるCSS符号などを接続します。
共通の定義があると、符号の行列について証明した性質を、「符号化した量子状態に対して何を保証するか」という説明へ結び付けられます。その上で、複数の符号を組み合わせる構成や、誤りを直せる領域に関する補題を使い回し、より大きな結果を組み立てます。個々の定理を別々に保存するだけでなく、結果同士の依存関係を残すことが狙いです。
量子LDPC符号の「大きくしても有利」を確かめる
中心的な題材は、量子LDPC符号です。LDPCは、各検査が調べる量子ビット数と、一つの量子ビットが参加する検査数を小さく抑える考え方です。符号を大きくしても、この二つを一定の上限内に保てれば、検査の一つ一つが際限なく複雑になるのを避けられます。
符号を比べるときには、物理量子ビット数n、保持する論理量子ビット数k、符号距離dを使います。符号距離は、検査では見逃されるのに論理情報を変えてしまう最小の誤りの大きさを表します。大きいほど、小さな誤りと論理情報の変化の間に余裕があります。
QECertが主に扱う「漸近的に良い」符号族では、十分大きな符号について、kもdもnに比例する下限を持ちます。物理量子ビットを増やすにつれ、情報の保持量と誤りへの保護を両方伸ばし、しかも検査の密度を抑えるという条件です。特定の100量子ビット装置での優位性を直接述べるものではなく、規模を増やしていく符号の系列に対する性質です。
論文は、ハイパーグラフ積、リフテッド積、量子Tanner符号などを共通の枠組みで扱います。ただし構成法によって、距離の伸び方や、証明に必要な条件は異なります。同じ「量子LDPC」という名前でも、保持量・距離・検査の負担を一組として見る必要があります。
公開コードで見える、証明の前提
ここで役立つのが、定理の結論だけでなく入力条件も確認できることです。例えば、良いリフテッド積符号を構成する定理には、使用するグラフについてのスペクトル境界が前提として書かれています。これは、グラフ上のつながりが十分よく広がることを、行列の作用の大きさから制限する条件です。
この条件があると、誤りに対応する小さな領域が局所的に閉じこもることを抑える議論へ進めます。公開コードは、その境界を受け取った後の符号の構成や性能を結び付けます。一方、必要なグラフの境界そのものを、この定理の中で無条件に証明したという意味ではありません。リポジトリも、この結果を条件付きの構成として明示しています。
例えば、別のグラフを使って同じ構成を試す研究者は、見た目が似ているからと結論だけを流用できません。新しいグラフが入力条件を満たすか、有限の符号サイズではどの範囲に保証が及ぶかを確認します。形式化の価値は、こうした受け渡しの条件を曖昧にせず残せるところにあります。
| 確かめたいこと | 読む箇所と残る確認 |
|---|---|
| 符号の保持量と距離 | 定理の入力条件と結論。十分大きい符号に関する保証か、有限のサイズでも使えるかを確認します。 |
| 検査の接続と配置 | 検査に参加する数の上限と、空間的な距離の制約を分けます。 |
| 実機での訂正能力 | 雑音模型、測定・復号の手順、処理時間などを別に評価します。 |
接続が疎でも、二次元に置きやすいとは限らない
一つの検査が少数の量子ビットだけを調べることと、その量子ビット同士が装置上で近くにあることは別です。遠く離れた少数の相手とつながる構成も、接続数の条件だけなら満たせます。実機では遠距離の操作や信号の配送が負担になるため、配置も性能の一部になります。
QECertは、この違いを扱うBPT境界なども含めています。二次元に局所的に置かれた、互いに可換な射影演算子で定まる符号では、条件の下でk×d²がnの定数倍以下になります。局所的な状態の次元や相互作用の範囲を固定した場合の制約です。
仮にkとdをどちらもnに比例させようとすると、左辺はnの三乗の大きさになり、右辺のnに比例する増え方と両立しません。これは良い量子LDPC符号の理論と矛盾するのではなく、二次元・短距離という配置条件を加えると別の制限が生じることを示します。実装へ進むときには、どの条件を緩めるのかも問われます。
公開された範囲と、これから確かめる範囲
論文の対象には、量子計算用の補助状態を精製するマジック状態蒸留や、量子メモリのエネルギー障壁・保存誤差も含まれます。ただし、三次元の受動的な量子メモリについては、具体的な構成と寿命の境界をまとめて形式化することが今後の目標として残っています。関連する部品がそろったことと、装置の保証が最後までつながったことを分けて読む必要があります。
今回確認した公開リポジトリでは、LeanとMathlibの版がv4.33.1に指定され、コードはApache-2.0で公開されています。定理を探す索引もありますが、説明用の見出しだけでなく、実際のLean宣言に書かれた条件を読むよう案内しています。オンラインの結果カタログは、確認時点では未公開の予定機能です。
QECertは、理論上の保証を再利用するときの確認点を具体的にする取り組みです。本記事では論文と公開コードの該当部分を照合しましたが、ライブラリ全体の再ビルドや、実機による性能検証は行っていません。今後は、復号器や誤り耐性プロトコルまでどのようにつながるかが、理論を実際の誤り訂正へ近づけるうえでの注目点になります。
出典
- K. Heほか「QECert: Formal Foundations for Quantum Error-Correction Theory in Lean」。arXiv:2611.05047v1、2026年11月3日投稿。本文2〜6節、特に構成の前提、BPT境界、三次元メモリの未完了範囲を参照。プレプリントです。
- Lean-QECert公開リポジトリ。2026年11月5日確認、commit 4a64933303628b4f94c4567347e86636853f64a4。README、lean-toolchain、LICENSE、MAIN_RESULTS.json、条件付きリフテッド積符号の定理を照合。論文と同じ開発主体の資料で、独立した検証報告ではありません。