論文の概要: 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（参考訳）: 量子誤差補正のエンド・ツー・エンド形式化
• 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 が得られる。 結果として得られるライブラリは再利用可能であり、フォールトトレラントな量子計算のエンドツーエンド検証に向けたより広範なリーンベースの取り組みをプラグインするように設計されている。

関連論文リスト

• Probabilistic Error Cancellation for Single-Mode Gottesman-Kitaev-Preskill Codes [45.91504150103373]
  本稿では,Gottesman-Kitaev-Preskill符号の文脈における確率的誤差キャンセル(probabilistic error cancel)と呼ばれる量子誤差軽減法について検討する。 我々は,GKP符号の安定化サブシステム分解を用いて,雑音処理のための効果的な論理チャネルを得る。
  論文  参考訳（メタデータ） (2026-09-15T12:29:45Z)
• Theory of approximate quantum error correction and the error-set model [53.73800998389749]
  誤差セットモデルに基づく近似量子誤差補正の理論を考案する。 与えられたエラーセットを修正するコードは、クラウス演算子が線形スパンにある全てのチャネルに対して自動的に保護される。 この線形性は、符号距離、消去と一般的な誤りの等価性、および理論上は良い符号をもたらす。
  論文  参考訳（メタデータ） (2026-07-25T02:15:33Z)
• 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)
• Toward Uncertainty-Aware and Generalizable Neural Decoding for Quantum LDPC Codes [0.9453554184019106]
  量子誤り訂正(QEC)はスケーラブルな量子コンピューティングに不可欠である。 我々は,ドット生成物とマルチヘッドの両方に注意を集中させるベイズグラフニューラルデコーダである textbfQuBA を提案する。 textbfSAGU textbf(Sequential Aggregate Generalization under Uncertainty)は、ドメイン間の堅牢性を向上したマルチコードトレーニングフレームワークである。
  論文  参考訳（メタデータ） (2025-10-05T01:08:39Z)
• Romanesco codes: Bias-tailored qLDPC codes from fractal codes [0.0]
  バイアスノイズに適応したクリフォード変形自転車コード群を導入・解析する。 我々のqLDPC符号は、制限域ゲートと低重安定化器を備えた二部形六角形格子上で定義される。 高い符号化率を持つ小さな例は、幅広いバイアスに対して良好に機能する。
  論文  参考訳（メタデータ） (2025-05-30T18:06:24Z)
• 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)
• Finding the disjointness of stabilizer codes is NP-complete [77.34726150561087]
  我々は、$c-不連続性を計算すること、あるいはそれを定数乗算係数の範囲内で近似することの問題はNP完全であることを示す。 CSSコード、$dコード、ハイパーグラフコードなど、さまざまなコードファミリの相違点に関するバウンダリを提供します。 以上の結果から,一般的な量子誤り訂正符号に対するフォールトトレラント論理ゲートの発見は,計算に難題であることが示唆された。
  論文  参考訳（メタデータ） (2021-08-10T15:00:20Z)

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

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