論文の概要: Formal Verification of Quantum Ancilla Safety
- arxiv url: http://arxiv.org/abs/2608.13099v1
- Date: Thu, 13 Aug 2026 11:20:06 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-14 18:29:38.500279
- Title: Formal Verification of Quantum Ancilla Safety
- Title（参考訳）: 量子アンシラ安全性の形式的検証
- Abstract要約: クリーンで汚いアンシラ安全のためのエンドツーエンドの検証・修復フレームワークを提案する。
まず、$m$-qubitの汚いアンシラレジスタの検証が、独立したクリーンなアンシラ安全性チェックに分解されることを証明します。
次に、各クリーンアンシラ安全インスタンスを、パウリ-$Z$およびパウリ-$X$作用素に対する代数的可換性チェックに還元する。
- 参考スコア（独自算出の注目度）: 3.5368690233168114
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Ensuring ancilla safety is a critical correctness requirement for quantum compilation, since ancilla qubits are routinely introduced to implement complex operations with fewer gates and reduced depth. However, formally verifying this property is computationally hard due to state-space explosion in the number of qubits, particularly for dirty ancillae, which carry unknown initial states and must be restored after use. We propose an end-to-end verification-and-repair framework that rigorously addresses both clean and dirty ancilla safety. Our core contribution is a two-step reduction strategy: we first prove that verifying an $m$-qubit dirty ancilla register decomposes into $2m$ independent clean ancilla safety checks; subsequently, we reduce each clean ancilla safety instance to an algebraic commutativity check against Pauli-$Z$ and Pauli-$X$ operators. This approach yields an efficient and naturally parallel verifier and enables actionable diagnosis by classifying violations into logic errors and phase errors. Leveraging this diagnosis, we further design lightweight repair routines that append local single-qubit rotations to eliminate a broad class of local ancilla faults. We implement the full pipeline in a prototype tool using a dual-backend architecture combining decision diagrams and weighted model counting, and validate it on diverse circuits ranging from arithmetic benchmarks to Grover's algorithm. Our experiments demonstrate scalability to thousands of qubits and show that the proposed repairs effectively improve ancilla safety while preserving circuit functionality.
- Abstract（参考訳）: アンシラキュービットは、ゲートが少なく、深さが減少する複雑な操作を実装するために定期的に導入されるため、量子コンパイルにおいて、アンシラ安全性の確保は重要な正当性要件である。
しかし、この性質を公式に検証するのは、量子ビット数における状態空間の爆発のため、特に未知の初期状態を持ち、使用後に回復しなければならない汚いアンシラのため、計算的に困難である。
クリーンかつ汚いアンシラの安全性に厳格に対処するエンドツーエンドの検証・修復フレームワークを提案する。
私たちはまず、$m$-qubitの汚いアンシラレジスタの検証を2M$の独立クリーンアンシラ安全チェックに分解し、その後、各クリーンアンシラ安全インスタンスをPauli-Z$およびPauli-X$演算子に対する代数的可換性チェックに還元する。
このアプローチは、効率的で自然な並列検証を行い、違反を論理エラーと位相エラーに分類することで、実用的な診断を可能にする。
この診断を応用して、局所的な単一ビット回転を付加する軽量な修復ルーチンを設計し、広範囲な局所的なアンシラ断層を除去する。
決定図と重み付きモデルカウントを組み合わせたデュアルバックエンドアーキテクチャを用いて,プロトタイプツールで完全なパイプラインを実装し,演算ベンチマークからGroverのアルゴリズムまで多種多様な回路上で検証する。
本実験は,数千量子ビットのスケーラビリティを実証し,回路機能を維持しつつ,アンシラの安全性を効果的に向上することを示す。
関連論文リスト
- Sound Debloating of Redundant Checks in Zero-Knowledge Machine-Learning Circuits [8.87115326771099]
音質を確実に保ちながら冗長チェックを除去する自動フレームワークを提案する。
我々のツールは最大48.7%の制約を排除し、セキュリティを弱めることなく証明時間を72.8%まで短縮する。
論文 参考訳（メタデータ） (2026-09-09T13:27:25Z) - The Gain-Engineered Transmon [68.89136228609398]
標準的なトランスモン・リードアウト共振器回路において,ノイズバイアス量子ビットを導入し,実験的に実現する。
本システムは,ハードウェア効率のよい量子エラー検出と修正手法のための単純なビルディングブロックとして利用するための道を開く。
論文 参考訳（メタデータ） (2026-08-26T17:00:42Z) - Quantum Uncomputation of Clean and Dirty Ancilla Qubits [1.6179458386967447]
クリーンアンシラと汚いアンシラの両非計算の統一的な形式化を提案する。
本稿では,2つの相補的合成指向存在チェック手法を提案する。
最先端のReqompcitereqompと比較すると、RwUnは実用的な複素依存性ベンチマークを100%カバーしている。
論文 参考訳（メタデータ） (2026-08-10T13:13:54Z) - Raw-Curve Quantum Fingerprints: A Mahalanobis Authentication Framework with Drift Early Warning and Adversarial Detection [11.819995530903567]
量子クラウドプラットフォームは強力なコンピューティング機能を提供することを目指しているが、ユーザは、どの物理デバイスがワークロードを実行するかを検証する直接的な手段を持っていない。
この透明性の欠如により、悪意のある敵がジョブを代替または劣等なプロセッサにリダイレクトするハードウェア置換攻撃が可能になる。
実測データから多次元量子指紋を構築することにより,この問題に対処する汎用認証フレームワークを提案する。
論文 参考訳（メタデータ） (2026-06-10T04:10:21Z) - Dynamic analysis enhances issue resolution [53.50448142467294]
DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。
テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。
Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
論文 参考訳（メタデータ） (2026-03-23T14:48:54Z) - Dynamical error reshaping for dual-rail erasure qubits [1.6312989763677892]
消去チェックや2ビットゲートを行いながらトランスモンノイズの悪影響を抑える方法を示す。
本稿では,これらの操作に対して,消去チェックエラーを2桁の精度で抑制する制御方式を提案する。
論文 参考訳（メタデータ） (2025-10-09T16:35:22Z) - Verification-Aided Learning of Neural Network Barrier Functions with
Termination Guarantees [6.9060054915724]
バリア関数は、システムの安全性を保証するための一般的なフレームワークである。
これらの関数を見つける一般的な方法は存在しない。
近年のアプローチでは、自己教師付き学習技術を用いてこれらの機能を学習している。
論文 参考訳（メタデータ） (2024-03-12T04:29:43Z) - Demonstrating a long-coherence dual-rail erasure qubit using tunable transmons [59.63080344946083]
共振結合された一対のトランスモンからなる「デュアルレール量子ビット」が高コヒーレントな消去量子ビットを形成することを示す。
我々は、チェック毎に0.1%$ dephasingエラーを導入しながら、消去エラーの中間回路検出を実演する。
この研究は、ハードウェア効率の量子誤り訂正のための魅力的なビルディングブロックとして、トランスモンベースのデュアルレールキュービットを確立する。
論文 参考訳（メタデータ） (2023-07-17T18:00:01Z) - Software mitigation of coherent two-qubit gate errors [55.878249096379804]
2量子ゲートは量子コンピューティングの重要な構成要素である。
しかし、量子ビット間の不要な相互作用(いわゆる寄生ゲート)は、量子アプリケーションの性能を低下させる。
寄生性2ビットゲート誤差を軽減するための2つのソフトウェア手法を提案する。
論文 参考訳（メタデータ） (2021-11-08T17:37:27Z) - Fault-tolerant parity readout on a shuttling-based trapped-ion quantum
computer [64.47265213752996]
耐故障性ウェイト4パリティチェック測定方式を実験的に実証した。
フラグ条件パリティ測定の単発忠実度は93.2(2)%である。
このスキームは、安定化器量子誤り訂正プロトコルの幅広いクラスにおいて必須な構成要素である。
論文 参考訳（メタデータ） (2021-07-13T20:08:04Z) - Efficient and robust certification of genuine multipartite entanglement
in noisy quantum error correction circuits [58.720142291102135]
実効多部絡み(GME)認証のための条件付き目撃手法を導入する。
線形な二分割数における絡み合いの検出は, 多数の測定値によって線形にスケールし, GMEの認証に十分であることを示す。
本手法は, 距離3の位相的カラーコードとフラグベースの耐故障バージョンにおける安定化作用素の雑音可読化に適用する。
論文 参考訳（メタデータ） (2020-10-06T18:00:07Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。