論文の概要: Efficient Formal Verification of Quantum Error Correcting Programs
- arxiv url: http://arxiv.org/abs/2504.07732v1
- Date: Thu, 10 Apr 2025 13:28:49 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-04-11 12:24:34.002259
- Title: Efficient Formal Verification of Quantum Error Correcting Programs
- Title（参考訳）: 量子誤り訂正プログラムの効率的な形式検証
- Authors: Qifan Huang, Li Zhou, Wang Fang, Mengyu Zhao, Mingsheng Ying,
- Abstract要約: 本稿では,量子誤り訂正(QEC)プログラムの効率的な検証フレームワークを提案する。
提案するプログラムロジックをCoq証明アシスタントで定式化し,QEC検証器として検証する。
検証された安定化器符号14のベンチマークを示す。
- 参考スコア（独自算出の注目度）: 4.936399271348611
- License:
- Abstract: Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers, and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier, Veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionality of the framework by performing different verification tasks across various scenarios. Finally, we present a benchmark of 14 verified stabilizer codes.
- Abstract（参考訳）: 量子誤り訂正(QEC)は、量子ハードウェアのノイズを抑制し、フォールトトレラントな量子計算を可能にするための基礎である。
本稿では,QECプログラムの効率的な検証フレームワークを提案する。
本稿では,QECプログラム用に特別に構築されたアサーション論理とプログラム論理を定義し,音響実証システムを確立する。
そこで我々は,QECプログラムの検証条件(VC)を効率的に処理する手法を開発した。パウリの誤差に対して,VCはSMTの解法で解ける古典的なアサーションに還元され,非パウリの誤差に対してはヒューリスティックなアルゴリズムを提供する。
提案するプログラムロジックをCoq証明アシスタントで定式化し,QEC検証器として検証する。
さらに, 各種耐故障シナリオを検証するために, 自動QEC検証器であるVeri-QECを実装した。
様々なシナリオで異なる検証タスクを実行することで、フレームワークの効率性と幅広い機能を示す。
最後に、検証された安定化器符号14のベンチマークを示す。
関連論文リスト
- Verifying Fault-Tolerance of Quantum Error Correction Codes [7.796308340803447]
大規模フォールトトレラント量子コンピューティングは、ノイズを抑制するために量子エラー訂正符号(QECC)に依存している。
本稿では,量子プログラム言語におけるQECC実装のフォールトトレランスを定式化する。
論文 参考訳（メタデータ） (2025-01-24T10:28:24Z) - Fault-tolerant quantum architectures based on erasure qubits [49.227671756557946]
我々は、支配的なノイズを既知の場所での消去に効率よく変換することで、消去量子ビットの考え方を利用する。
消去量子ビットと最近導入されたFloquet符号に基づくQECスキームの提案と最適化を行う。
以上の結果から, 消去量子ビットに基づくQECスキームは, より複雑であるにもかかわらず, 標準手法よりも著しく優れていることが示された。
論文 参考訳（メタデータ） (2023-12-21T17:40:18Z) - Demonstration of fault-tolerant Steane quantum error correction [0.7174990929661688]
本研究では,複数ラウンドのフォールトトレラントSteane QECをトラップイオン量子コンピュータ上に実装する。
各種QEC符号を用い, フラグ量子ビットを用いた従来の実験手法と比較した。
論文 参考訳（メタデータ） (2023-12-15T12:32:49Z) - Testing the Accuracy of Surface Code Decoders [55.616364225463066]
大規模でフォールトトレラントな量子計算は量子エラー訂正符号(QECC)によって実現される
本研究は,QECC復号方式の精度と有効性をテストするための最初の体系的手法である。
論文 参考訳（メタデータ） (2023-11-21T10:22:08Z) - Enabling Full-Stack Quantum Computing with Changeable Error-Corrected
Qubits [14.770636234849444]
我々は、変更可能な論理量子ビットに基づくFTQCの大規模設計空間を探索するために、CECQを提案する。
様々な量子プログラムの実験は、CECQの有効性を示す。
論文 参考訳（メタデータ） (2023-05-11T18:14:49Z) - Deep Quantum Error Correction [73.54643419792453]
量子誤り訂正符号(QECC)は、量子コンピューティングのポテンシャルを実現するための鍵となる要素である。
本研究では,新しいエンペンド・ツー・エンドの量子誤りデコーダを効率的に訓練する。
提案手法は,最先端の精度を実現することにより,QECCのニューラルデコーダのパワーを実証する。
論文 参考訳（メタデータ） (2023-01-27T08:16:26Z) - Qafny: A Quantum-Program Verifier [39.47005122712576]
本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。
Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。
我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
論文 参考訳（メタデータ） (2022-11-11T18:50:52Z) - Measurement based estimator scheme for continuous quantum error
correction [52.77024349608834]
正準離散量子誤差補正(DQEC)スキームは、安定器上の射影フォン・ノイマン測度を用いて誤差症候群を有限集合に識別する。
連続的量子誤差補正(CQEC)と呼ばれる連続的な測定に基づく量子エラー補正(QEC)は、DQECよりも高速に実行でき、資源効率も向上できる。
論理量子ビットの計測に基づく推定器 (MBE) を構築することにより, 物理量子ビットに発生する誤差をリアルタイムで正確に追跡できることを示す。
論文 参考訳（メタデータ） (2022-03-25T09:07:18Z) - Measuring NISQ Gate-Based Qubit Stability Using a 1+1 Field Theory and
Cycle Benchmarking [50.8020641352841]
量子ハードウェアプラットフォーム上でのコヒーレントエラーを, サンプルユーザアプリケーションとして, 横フィールドIsing Model Hamiltonianを用いて検討した。
プロセッサ上の物理位置の異なる量子ビット群に対する、日中および日中キュービット校正ドリフトと量子回路配置の影響を同定する。
また,これらの測定値が,これらの種類の誤差をよりよく理解し,量子計算の正確性を評価するための取り組みを改善する方法についても論じる。
論文 参考訳（メタデータ） (2022-01-08T23:12:55Z) - QECV: Quantum Error Correction Verification [15.05397810840915]
安定化器符号の形式的正当性を効率よく検証できる検証フレームワークQECVを提案する。
本稿では,QECV プログラムの正しさを効率的に推論するために,QECV の推論規則をセットとした音量子 Hoare 論理証明系を導出する。
論文 参考訳（メタデータ） (2021-11-26T19:40:53Z) - Using Quantum Metrological Bounds in Quantum Error Correction: A Simple
Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
本稿では、量子誤り訂正符号の品質と、論理ゲートの普遍的な集合を達成する能力とを結びつける、近似したイージン・クニル定理の証明を示す。
我々の導出は、一般的な量子気象プロトコルにおける量子フィッシャー情報に強力な境界を用いる。
論文 参考訳（メタデータ） (2020-04-24T17:58:10Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。