論文の概要: Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction

• arxiv url: http://arxiv.org/abs/2609.36065v1
• Date: Mon, 28 Sep 2026 18:20:12 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-30 21:28:46.934042
• Title: Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction
• Title（参考訳）: Irene: 構造保存型シンボリックリダクションによるハイブリッド量子プログラムの等価チェック
• Abstract要約: 我々は、有界ハイブリッド量子プログラムの同値チェックフレームワークであるIreneを提案する。 アイリーンは3段階の推論を通じて、同値義務を徐々に単純化する。 我々は、7つのベンチマークスイートから1,982個のプログラムペアに対して5つの等価チェッカーに対してアイリーンを評価する。
• 参考スコア（独自算出の注目度）: 7.475350839155081
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Equivalence checking is essential for validating compiler transformations of hybrid quantum programs, which combine quantum operations, measurements, and classical control. Measurement-dependent control limits unitary reasoning, while dependencies between classical outcomes and quantum operations can enlarge intermediate symbolic states. We present Irene, an equivalence-checking framework for bounded hybrid quantum programs based on structure-preserving symbolic reduction. The framework progressively simplifies equivalence obligations through three levels of reasoning. At the gate level, algebraic identities simplify unitary regions. At the hybrid path-sum (HPS) level, reduced symbolic execution states are represented as typed graphs, whose isomorphism certifies equivalence. Remaining obligations are handled by density kernels that characterize transformations of input density operators into observable outputs, allowing comparison even when internal measurement histories differ. Residual coefficient differences are encoded as SMT queries. A common set of symbolic reductions supports HPS and density-kernel reasoning by preserving factored Boolean and arithmetic expressions, eliminating reducible dependencies before expanding residual sums. We evaluate Irene against five equivalence checkers on 1,982 program pairs from seven benchmark suites. Irene solves 1,584 pairs (79.92%), compared with 57.52% for MQT QCEC, the baseline with the highest aggregate coverage, with a mean end-to-end time of 3.93 seconds per solved pair. Applied as an equivalence-checking oracle, Irene also identifies 15 previously unknown bugs in quantum compilers, including Qiskit, Cirq, and PennyLane.
• Abstract（参考訳）: 等価チェックは、量子演算、測定、古典制御を組み合わせたハイブリッド量子プログラムのコンパイラ変換を検証するために不可欠である。 測定依存制御はユニタリ推論を制限するが、古典的な結果と量子演算の間の依存関係は中間的記号状態を大きくすることができる。 構造保存型シンボリックリダクションに基づく有界ハイブリッド量子プログラムの等価チェックフレームワークであるIreeneを提案する。 この枠組みは3段階の推論を通じて、同値義務を徐々に単純化する。 ゲートレベルでは、代数的アイデンティティはユニタリ領域を単純化する。 ハイブリッドパスサム(HPS)レベルでは、縮小されたシンボル実行状態は型付きグラフとして表現され、同型は同値である。 残留義務は、入力密度演算子の可観測出力への変換を特徴付ける密度カーネルによって処理され、内部測定履歴が異なっても比較が可能である。 残差差はSMTクエリとして符号化される。 シンボリックリダクションの共通セットは、分解されたブール式と算術式を保存することでHPSと密度カーネル推論をサポートし、残余和を拡張する前に再現可能な依存関係を排除している。 我々は、7つのベンチマークスイートから1,982個のプログラムペアに対して5つの等価チェッカーに対してアイリーンを評価する。 Irene は 1,584 対 (79.92%) を解き、MQT QCEC は 57.52% である。 等価チェックのオラクルとして応用されたIrene氏は、Qiskit、Cirq、PennyLaneなど、これまで知られていない15の量子コンパイラのバグも特定している。

関連論文リスト

• Entanglement Quantification via Symmetric Extensions: A Resource Theory Hierarchy [3.662037602213926]
  k対称PT拡張に基づく絡み合い尺度Ekの階層化を導入する。 それぞれのEkは最小の固有値シフトによって定義され、自由操作の下で忠実で凸で単調である。 階層構造は k = 1 で PPT-ロバスト性を厳密に洗練し、k = 2 で有界な絡み合いを検出し、分離性測度を k -> 無限大として正確に収束させる。
  論文  参考訳（メタデータ） (2026-07-18T20:39:35Z)
• Loophole-Robust Certification of Quantum Advantage [0.0]
  最適なベンチマーク依存の古典スコアは、$S_leqmin1,S_mathrmcl+$に従っており、この境界を飽和させる一連のタスクを構成する。 フレームワークを有限サンプルデータ、相互情報制約、多部タスク、因果経路に沿って分布する相関に拡張する。
  論文  参考訳（メタデータ） (2026-07-13T18:12:04Z)
• GroverFigureOfMerit: An Agnostic Figure of Merit for Quantum Backend Characterization in the NISQ Era [41.99844472131922]
  本稿では,Groverのアルゴリズムに基づくメリットのフィギュアを,量子バックエンド性能を均等に評価するアルゴリズム的ストレステストとして提案する。 この計量は、目標状態の成功確率と、非一様増幅と非マーク状態へのリークに対する罰則を組み合わせ、ハードウェアアーキテクチャ全体で統一されたスコアを得る。
  論文  参考訳（メタデータ） (2026-07-09T16:08:48Z)
• EQE-QAOA: An Equivalence-Preserving Qubit Efficient Framework for Combinatorial Optimization [54.05451096499336]
  既存の技術は情報損失のコストで量子ビットの削減に依存しており、計算性能は劣化している。 等価保存量子ビット効率QAOAを提案し、性能を劣化させることなく必要なキュービット数を著しく削減する。 完全独立変数を持つ非制約問題を除いて,大規模最適化問題に広く適用可能であることを示す。
  論文  参考訳（メタデータ） (2026-04-20T13:57:49Z)
• One-Shot Structured Pruning of Quantum Neural Networks via $q$-Group Engineering and Quantum Geometric Metrics [7.913101398893967]
  量子ニューラルネットワーク(QNN)はゲートレベルの深刻な冗長性に悩まされており、ノイズの多い中間スケールの量子デバイスへの展開を妨げる。 q-iPruneは、$q$の変形群とタスク条件群からなる代数的構造を基盤とした一発的構造化プルーニングフレームワークである。 標準的な量子機械学習ベンチマークの実験では、q-iPruneは、有界なタスク性能の劣化を維持しながら、実質的なゲート低減を実現している。
  論文  参考訳（メタデータ） (2025-12-30T06:37:28Z)
• Performance Guarantees for Quantum Neural Estimation of Entropies [31.955071410400947]
  量子神経推定器(QNE)は古典的ニューラルネットワークとパラメトリズド量子回路を組み合わせたものである。 非漸近的エラーリスク境界の形で測定された相対エントロピーのQNEの形式的保証について検討する。 我々の理論は、測定された相対エントロピーに対するQNEの原則的実装を促進することを目的としている。
  論文  参考訳（メタデータ） (2025-11-24T16:36:06Z)
• Characterizing randomness in parameterized quantum circuits through expressibility and average entanglement [39.58317527488534]
  量子回路(PQC)は、その主応用の範囲外ではまだ完全には理解されていない。 我々は、量子ビット接続性に関する制約の下で、PQCにおけるランダム状態の生成を分析する。 生成した状態の分布の均一性の増加と絡み合いの発生との間には,どれだけ急激な関係があるかを示す。
  論文  参考訳（メタデータ） (2024-05-03T17:32:55Z)
• Generalised Coupling and An Elementary Algorithm for the Quantum Schur Transform [0.0]
  量子シュア変換を実装するための透過的アルゴリズムを提案する。 クレーブシュ=ゴルダン係数を介して結合された量子ビットからなるシュル状態について検討する。 Wigner 6-j 記号と SU(N) Clebsch-Gordan 係数が我々の枠組みに自然に適合していることが示されている。
  論文  参考訳（メタデータ） (2023-05-06T15:19:52Z)
• Iterative Qubit Coupled Cluster using only Clifford circuits [36.136619420474766]
  古典的に容易に生成できる理想的な状態準備プロトコルを特徴付けることができる。 繰り返し量子ビット結合クラスタ(iQCC)の変種を導入して,これらの要件を満たす手法を提案する。 本研究では, チタン系化合物Ti(C5H5)(CH3)3と (20, 20) 活性空間の複雑な系に研究を拡張した。
  論文  参考訳（メタデータ） (2022-11-18T20:31:10Z)

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

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