論文の概要: QECert: Formal Foundations for Quantum Error-Correction Theory in Lean

• arxiv url: http://arxiv.org/abs/2611.05047v1
• Date: Tue, 03 Nov 2026 15:15:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-11-07 14:45:10.708311
• Title: QECert: Formal Foundations for Quantum Error-Correction Theory in Lean
• Title（参考訳）: QECert: リーンにおける量子エラー補正理論の形式的基礎
• Abstract要約: 既存の形式化は、安定化コードとコード検証の基盤を確立している。 QECertは、これらの理論的問題に対して再利用可能な形式的基盤を提供するリーンライブラリです。
• 参考スコア（独自算出の注目度）: 6.754233473183281
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Quantum error correction provides the mathematical basis for protecting quantum information against noise. Existing formalizations have established foundations for stabilizer codes and code verification. However, a systematic formal treatment of the asymptotic constructions and fundamental limitations that underpin scalable quantum error correction is still needed. We present QECert, a Lean library providing reusable formal foundations for these theoretical questions. It connects quantum error-correction criteria, stabilizer and Calderbank-Shor-Steane codes, and algebraic and homological constructions within a common framework. Asymptotically good quantum low density parity check codes provide the principal case study. We formalize constructions and asymptotic parameter theorems spanning hypergraph products, balanced products, lifted products, and quantum Tanner codes. Further developments cover Bravyi-Poulin-Terhal bounds and related locality restrictions, constant overhead magic state distillation, and energy barriers and storage errors for quantum memories. QECert establishes a reusable formal foundation for studying the capabilities, resource requirements, and fundamental limitations of quantum error correction, supporting systematic verification and further development of its theory.
• Abstract（参考訳）: 量子誤り訂正は、ノイズに対して量子情報を保護する数学的基礎を提供する。 既存の形式化は、安定化コードとコード検証の基盤を確立している。 しかし、漸近的な構造と拡張性のある量子誤り訂正の基盤となる基本的な制限の体系的な形式的処理は依然として必要である。 QECertは、これらの理論的問題に対して再利用可能な形式的基盤を提供するリーンライブラリです。 量子誤差補正基準、安定化器、カルダーバンク・ソー=ステアン符号、および共通フレームワーク内の代数的およびホモロジー的構造を結合する。 漸近的に良い量子低密度パリティチェック符号は、主要なケーススタディを提供する。 我々は、ハイパーグラフ積、平衡積、持ち上げ積、量子タナー符号にまたがる構成と漸近パラメータ定理を定式化する。 さらに、ブラヴィイ・プーリン・ターハル境界と関連する局所性制限、一定のオーバーヘッドのマジック状態蒸留、量子メモリのエネルギー障壁と保存誤差をカバーしている。 QECertは、量子誤り訂正の能力、リソース要件、基本的な限界を研究するための再利用可能な公式基盤を確立し、体系的な検証と理論のさらなる発展を支援している。

関連論文リスト

• Lean-QIT: Towards a Formal Infrastructure for Quantum Information Theory [13.58013986113788]
  量子情報理論(QIT)は、量子情報処理の能力と基本的な限界を特徴づける。 既存の開発には、コード、エラー基準、達成可能なレート、能力を定義する再利用可能な運用層がない。 有限次元QITのためのLean 4ライブラリであるLeanQITを紹介します。
  論文  参考訳（メタデータ） (2026-07-10T17:28:26Z)
• Error Correction in Lattice Quantum Electrodynamics with Quantum Reference Frames [1.177047754711803]
  QECC(Quantum error-correcting codes)は、冗長性はノイズから情報を保護するリソースとして機能することを示している。 ゲージ理論が同様の意味で理解可能かどうかを問うとともに、格子量子電磁力学においてこの考えを具体化する。
  論文  参考訳（メタデータ） (2026-04-07T17:51:56Z)
• Formal Verification of Variational Quantum Circuits [44.06507276521908]
  変分量子回路(VQC)は多くの量子機械学習アルゴリズムの中心的なコンポーネントである。 本稿では,VQCの形式的検証問題に関する基礎的および実践的研究について述べる。
  論文  参考訳（メタデータ） (2025-07-14T12:28:32Z)
• VQC-MLPNet: An Unconventional Hybrid Quantum-Classical Architecture for Scalable and Robust Quantum Machine Learning [50.95799256262098]
  変分量子回路(VQC)は量子機械学習を約束するが、表現性、訓練性、耐雑音性の課題に直面している。 本稿では,VQCが学習中に古典多層パーセプトロンの第一層重みを生成するハイブリッドアーキテクチャであるVQC-MLPNetを提案する。
  論文  参考訳（メタデータ） (2025-06-12T01:38:15Z)
• Single-shot and measurement-based quantum error correction via fault complexes [0.0]
  フォトニクスは、スケーラブルなフォールトトレラント量子コンピュータへの実行可能なパスを提供する。 葉は耐障害性グラフ状態の構築である。 本稿では,動的量子誤り訂正プロトコルの表現であるフォールトコンプレックスを紹介する。
  論文  参考訳（メタデータ） (2024-10-16T18:52:24Z)
• Stabilizer Formalism for Operator Algebra Quantum Error Correction [0.0]
  演算子量子誤差補正(OAQEC)と呼ばれる一般量子エラー補正フレームワークに対する安定化器形式を導入する。 与えられた符号に対して修正可能なパウリ誤差を完全に特徴づける定理を定式化する。 最近のハイブリッドサブスペースのコード構造が形式主義によってどのように捉えられているかを示す。
  論文  参考訳（メタデータ） (2023-04-22T16:45:50Z)
• Qafny: A Quantum-Program Verifier [39.47005122712576]
  本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。 我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
  論文  参考訳（メタデータ） (2022-11-11T18:50:52Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  本稿では,量子状態の知識を必要とせず,量子回路の可換性を検証する回路指向対称性検証を提案する。 特に、従来の量子領域形式を回路指向安定化器に一般化するフーリエ時間安定化器(STS)手法を提案する。
  論文  参考訳（メタデータ） (2021-12-27T21:15:35Z)
• Fusion-based quantum computation [43.642915252379815]
  フュージョンベース量子コンピューティング(Fusion-based quantum computing、FBQC)は、核融合と呼ばれるエンタングリングの測定を、小さな定数サイズのエンタングルド・リソース状態の量子ビット上で行う、普遍量子計算のモデルである。 本稿では,これらのスキームにおける耐故障性と計算を解析するための安定化器形式について紹介する。 このフレームワークは、フォトニクスのような量子コンピューティングの特定の物理系で発生するエラー構造を自然に捉えている。
  論文  参考訳（メタデータ） (2021-01-22T20:00:22Z)
• Using Quantum Metrological Bounds in Quantum Error Correction: A Simple Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
  本稿では、量子誤り訂正符号の品質と、論理ゲートの普遍的な集合を達成する能力とを結びつける、近似したイージン・クニル定理の証明を示す。 我々の導出は、一般的な量子気象プロトコルにおける量子フィッシャー情報に強力な境界を用いる。
  論文  参考訳（メタデータ） (2020-04-24T17:58:10Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。