論文の概要: Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over {H,X,C-NOT}: CSS Constructions, Soundness, and Mutation-Based Validation

• arxiv url: http://arxiv.org/abs/2610.03794v1
• Date: Thu, 01 Oct 2026 00:22:13 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-13 05:13:25.446623
• Title: Generalised Bit-Vector Abstractions for Formal Verification of Quantum Error-Detection and Entanglement Circuits over {H,X,C-NOT}: CSS Constructions, Soundness, and Mutation-Based Validation
• Title（参考訳）: H,X,C-NOT}上の量子誤り検出および絡み合い回路の形式的検証のための一般化ビットベクトル抽象化:CSS構成,音質,変異に基づく検証
• Abstract要約: 量子回路の形式的検証は、回路サイズが大きくなるにつれて困難になる。 前回の研究では、重ね合わせ追跡を基底状態の挙動から分離するビットベクトル抽象化を導入した。 本稿では,その枠組みを5方向に拡張する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification of quantum circuits becomes difficult as circuit size grows because exhaustive reasoning over the Hilbert space is computationally expensive. In previous work [1], we introduced a bit-vector abstraction that separates superposition tracking from basis-state behavior, enabling SMT-based verification of fixed-size error-detection and entanglement circuits built from H, X, and C-NOT gates. This paper extends the framework in five directions. First, we generalise correctness properties to parametrised repetition and concatenated phase-flip codes with up to 101 logical elements. Second, we verify syndrome extraction for CSS codes specified by arbitrary parity-check matrices, including the Steane, [[15,7,3]] Hamming, [[15,1,3]] Reed-Muller, and rotated surface codes with distances up to 101. We consider arbitrary error patterns, detection up to a specified weight, and recovery using a classical decoder, with counterexamples beyond each code's correction or detection capability. Third, we characterize the {H,X,C-NOT} fragment for which the abstraction faithfully represents Hilbert-space semantics. We prove soundness, demonstrate necessity with counterexamples, validate the characterisation against state-vector simulation, and prove the six lemmas from the original work. Fourth, a mutation study using 13 operators identifies equivalent mutants and detects all 622 non-equivalent mutants within the evaluated fault model. Fifth, a direct Z3 implementation verifies GHZ circuits with up to 262,144 qubits across three topologies on a 16GB laptop. Random H+C-NOT networks show verification cost rises sharply with depth when outputs depend on many inputs. The approach does not target general stabilizer circuits, Y-type stabilizers, fault-tolerant protocols, or physical noise; we identify extensions needed to address these cases.
• Abstract（参考訳）: ヒルベルト空間上の徹底的な推論は計算的に高価であるため、回路サイズが大きくなるにつれて量子回路の形式的検証は困難になる。 従来の研究[1]では,H,X,C-NOTゲートから構築した固定サイズ誤差検出回路と絡み込み回路のSMTによる検証を可能にするため,重ね合わせ追跡を基底状態の動作から分離するビットベクトル抽象化を導入した。 本稿では,その枠組みを5方向に拡張する。 まず、パラメトリ繰り返しと最大101個の論理的要素を持つ位相フリップ符号の整合性特性を一般化する。 次に,Steane,[[15,7,3]] Hamming,[[15,1,3]] Reed-Mullerなどの任意のパリティチェック行列で指定されたCSSコードのシンドローム抽出を検証する。 我々は、任意のエラーパターン、指定された重みまでの検出、古典的なデコーダによるリカバリについて検討し、各コードの修正や検出能力を超えている。 第三に、抽象がヒルベルト空間の意味論を忠実に表現する {H,X,C-NOT} フラグメントを特徴付ける。 我々は,音質の証明,反例の必要性の証明,状態ベクトルシミュレーションに対するキャラクタリゼーションの検証,オリジナル作品からの6つの補題の証明を行う。 第4に、13の演算子を用いた突然変異研究は、等価変異体を特定し、評価された断層モデル内の622の非等価変異体全てを検出する。 第5に、Z3実装は16GBラップトップ上の3つのトポロジで最大262,144キュービットのGHZ回路を検証する。 ランダムH+C-NOTネットワークは、多くの入力に依存する出力で検証コストが急上昇することを示す。 本手法は, 一般的な安定化回路, Y型安定化回路, 耐故障プロトコル, 物理ノイズを対象としない。

関連論文リスト

• Certified decoding of quantum LDPC codes [31.93810256110857]
  量子低密度パリティチェック(qLDPC)符号は、フォールトトレラント量子計算の量子ビットオーバーヘッドを桁違いに減少させる。 多くの物理誤差は安定化器と同値であるため、縮退した最大形(ML)デコーダは、単一エラーではなく分割関数であるエラーの同値クラス全体の確率を比較する必要がある。 非方向性のグラフィカルモデルにおいて、退化復号化を確率的推論として扱う。
  論文  参考訳（メタデータ） (2026-08-26T08:57:01Z)
• Distributional Energy-Based Models for Uncertainty-Aware Structured LLM Reasoning [40.342912574072024]
  大規模言語モデルは、旅行計画やコードソリューションのような構造化されたアウトプットを生成する。 個々の推論ステップは正しく見えるが、アウトプット全体が予算に違反したり、テストケースに失敗したり、あるいは以前の推論に矛盾することがある。 構造化LCM出力の検証のための決定論的解析制約付き学習品質スコアラを提案する。
  論文  参考訳（メタデータ） (2026-05-15T17:08:27Z)
• Pairwise matrices for sparse autoencoders: single-feature inspection mislabels causal axes [2.741152471987327]
  標準スパースオートエンコーダプロトコルは、各機能をトップアクティベーションコンテキストからラベル付けし、単一機能ステアリングによって検証する。 本稿では,Qwen3-1.7B-Instruct上での標準ワンコーナプロトコルミスをGemma-2-2B-itで再現した,ペアワイズ行列プロトコルと共変ステアリング係数を提案する。 これら3つの所見はGemmaでモデル特異的な損傷シグネチャを再現し,一致した形状制御はCIを10倍に分離する。
  論文  参考訳（メタデータ） (2026-05-04T21:11:21Z)
• Low Overhead Universal Quantum Computation with Triorthogonal Codes [8.516351290711953]
  普遍的フォールトトレラント量子計算における三角符号の利用について検討する。 本稿では,任意の量子誤り訂正符号が普遍性とゲートセットの両方をサポートすることを禁止しているEastin-Knill定理を回避する2つの方法を提案する。
  論文  参考訳（メタデータ） (2025-10-07T09:17:10Z)
• Universal quantum computation via scalable measurement-free error correction [45.29832252085144]
  本研究では,中間回路計測を行なわずに誤り訂正を行うシナリオにおいて,普遍的な量子計算をフォールトトレラントにすることができることを示す。 論理的な$mathitCCZ$ゲートを実現するため,Bacon-Shor符号の無測定変形プロトコルを導入する。 特に,回路レベルのエラーレートが10～3ドル以下であれば,破れない論理性能が達成可能であることを示す。
  論文  参考訳（メタデータ） (2024-12-19T18:55:44Z)
• Demonstrating dynamic surface codes [118.67046728951689]
  曲面符号の3つの時間力学的実装を実験的に実証した。 まず、曲面コードを六角格子上に埋め込んで、キュービットあたりの結合を4つから3つに減らした。 第二に、サーフェスコードを歩き、データの役割を交換し、各ラウンドごとにキュービットを測定し、蓄積した非計算エラーの組込み除去による誤り訂正を達成する。 第3に、従来のCNOTの代わりにiSWAPゲートを用いた表面コードを実現し、追加のオーバーヘッドを伴わずに、エラー訂正のための実行可能なゲートセットを拡張した。
  論文  参考訳（メタデータ） (2024-12-18T21:56:50Z)
• Emergent unitary designs for encoded qubits from coherent errors and syndrome measurements [0.8491161158902805]
  曲面符号における符号化量子ビットのユニタリ設計を効率よく生成する手法を提案する。 論理的ユニタリのアンサンブルが熱力学限界におけるユニタリ設計に収束することを数値的に示す。 本結果は,符号化量子ビット上のユニタリ設計を実現するための実用的な方法を提供する。
  論文  参考訳（メタデータ） (2024-12-05T18:36:14Z)
• Fault-tolerant parity readout on a shuttling-based trapped-ion quantum computer [64.47265213752996]
  耐故障性ウェイト4パリティチェック測定方式を実験的に実証した。 フラグ条件パリティ測定の単発忠実度は93.2(2)%である。 このスキームは、安定化器量子誤り訂正プロトコルの幅広いクラスにおいて必須な構成要素である。
  論文  参考訳（メタデータ） (2021-07-13T20:08:04Z)

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

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