論文の概要: End-to-End Formalization of Quantum Error Correction

• arxiv url: http://arxiv.org/abs/2605.16523v1
• Date: Fri, 15 May 2026 18:17:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-19 17:57:46.604421
• Title: End-to-End Formalization of Quantum Error Correction
• Title（参考訳）: 量子誤差補正のエンド・ツー・エンド形式化
• Authors: Mattias Ehatamm, Yi Lee, Xiaodi Wu, Runzhou Tao,
• Abstract要約: 量子エラー訂正符号(QECC)はノイズの多い量子ハードウェアと信頼性の高い計算の間にあり、実際に使用されるコードパラメータは信頼に値するものである必要がある。 Lean-QECは、産業コードサイズでマシンチェックされた距離証明書を提供する、Stabler-code理論の最初のLean 4の形式化です。
• 参考スコア（独自算出の注目度）: 6.320988144551776
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from $n$ to $k\lceil \log_2 n\rceil$. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.
• Abstract（参考訳）: 量子エラー訂正符号(QECC)はノイズの多い量子ハードウェアと信頼性の高い計算の間にあり、実際に使用されるコードパラメータは信頼に値するものである必要がある。 符号の強さを要約する唯一の数字はその距離であるが、距離の下限の証明は一般にNPハードであり、ペンと紙の証明の範囲を超え、直接の証明補助スクリプティングである。 結果として、文学における距離の値は、非スケーリングハンド証明か、またはコードが保証を提供するはずの場所に、信頼ギャップを残した未検証の解決者から生じる。 Lean-QECは、産業コードサイズでエンドツーエンドでマシンチェックされた距離証明書を提供する、Stabler-code理論の最初のLean 4の形式化です。 Lean-QECは、キュービット状態の線型代数、パウリ群、安定化符号、二進シンプレクティック表現、古典的符号化理論、CSSおよびバイバーリエート自転車群を定式化する。 組合せ障壁を断ち切るため、Lean-QECは証明された縮小により距離条件をブール適合式に変換する。 パイプラインは、LeanのMatrix表現を置き換えるBitVecフラットなエンコーディングと、変数カウントを$n$から$k\lceil \log_2 n\rceil$に縮小するエラーロケーションエンコーディングを通じてスケールする。 これにより、[90, 8, 10] および [[70, 6, 9] BB コードを含む、Bivariate Bicycle および Generalized Bicycle family 内で、幅広い産業的に実行可能な qLDPC コードに対して、自動生成の Lean-checked distance proofs が得られる。 結果として得られるライブラリは再利用可能であり、フォールトトレラントな量子計算のエンドツーエンド検証に向けたより広範なリーンベースの取り組みをプラグインするように設計されている。

関連論文リスト

• Error Correction of Beamsplitter-Generated Entangled GKP States [56.80803785296797]
  有望なボソニックコードは、Gottesman-Kitaev-Preskill (GKP)コードである。 ビームスプリッタ上にグリッド構造を持つが論理情報を持たない2つのクヌート状態に干渉することにより、GKP量子ビットの絡み合った状態を生成する。 我々は,平均忠実度69%のベル状態をすべて生成し,量子誤差補正を用いて絡み合った状態寿命の延長を示す。
  論文  参考訳（メタデータ） (2026-05-08T17:01:19Z)
• Self-dual Stacked Quantum Low-Density Parity-Check Codes [9.268855474673822]
  自己双対qLDPC符号を積み重ねて自己双対qLDPC符号を構築する手法を提案する。 我々は、回路レベルのノイズモデルの下で、これらの符号の性能を量子メモリとして評価するために数値計算を行う。
  論文  参考訳（メタデータ） (2026-02-17T05:55:48Z)
• Single-Shot and Few-Shot Decoding via Stabilizer Redundancy in Bivariate Bicycle Codes [5.685589351789461]
  我々は、$g(z)$がコードの安定化器の冗長性と、単発デコードに必要な古典的なアンフシンドローム符号の構造を規定していることを証明した。 共振器BBアンザッツの内部では、高い量子レートはシンドローム距離に上限を課し、単発性能を制限する。
  論文  参考訳（メタデータ） (2026-01-03T09:49:58Z)
• Existence and Characterisation of Bivariate Bicycle Codes [0.0]
  BB符号は、オーバーヘッドが低く、誤り訂正能力が向上したコンパクトな量子メモリを提供することを示す。 リング構造を利用してこれらの符号を探索し、それらの次元とそれらの存在条件を予測する。
  論文  参考訳（メタデータ） (2025-02-24T11:04:15Z)
• Single-shot decoding of good quantum LDPC codes [38.12919328528587]
  量子タナー符号が逆雑音の単ショット量子誤り補正(QEC)を促進することを証明した。 本稿では,複数ラウンドのQECにおける誤りを抑えるために,並列復号アルゴリズムを各ラウンドで一定時間実行するのに十分であることを示す。
  論文  参考訳（メタデータ） (2023-06-21T18:00:01Z)
• Deep Quantum Error Correction [73.54643419792453]
  量子誤り訂正符号(QECC)は、量子コンピューティングのポテンシャルを実現するための鍵となる要素である。 本研究では,新しいエンペンド・ツー・エンドの量子誤りデコーダを効率的に訓練する。 提案手法は,最先端の精度を実現することにより,QECCのニューラルデコーダのパワーを実証する。
  論文  参考訳（メタデータ） (2023-01-27T08:16:26Z)
• Neural Belief Propagation Decoding of Quantum LDPC Codes Using Overcomplete Check Matrices [60.02503434201552]
  元のチェック行列における行の線形結合から生成された冗長な行を持つチェック行列に基づいてQLDPC符号を復号する。 このアプローチは、非常に低い復号遅延の利点を付加して、復号性能を著しく向上させる。
  論文  参考訳（メタデータ） (2022-12-20T13:41:27Z)

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

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