論文の概要: QisMC: A Model Checker for QISKIT Program Debugging
- arxiv url: http://arxiv.org/abs/2608.24320v1
- Date: Tue, 25 Aug 2026 09:47:13 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-08-26 14:09:34.925778
- Title: QisMC: A Model Checker for QISKIT Program Debugging
- Title(参考訳): QisMC:QISKITプログラムデバッグのためのモデルチェッカー
- Abstract要約: 本稿では,Qiskitプログラムのデバッグ専用の量子モデルチェッカーであるQisMCを紹介する。
理論的には、量子古典遷移系と量子計算ツリー論理の概念を導入する。
実装面では、QisMCはトランジッションシステム生成、論理式表現、モデルチェックアルゴリズムを含むエンドツーエンドのフレームワークを提供する。
- 参考スコア(独自算出の注目度): 4.521745462304204
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: We present QisMC, the first quantum model checker dedicated to debugging Qiskit programs. On the theoretical side, we introduce the notion of quantum-classical transition system and a quantum computation tree logic (qCTL) grounded in Birkhoff-von Neumann logic for modeling the behaviors and specifying the properties of Qiskit programs, respectively. On the implementation side, QisMC provides an end-to-end framework encompassing transition system generation, logical formula representation, and model checking algorithms, and it efficiently performs image computation based on decision diagrams. These methods and design principles give QisMC advantages over previous Qiskit program debuggers, including a unified property specification language, a fully automated and exhaustive verification process, and the ability to generate counterexamples. Extensive illustrative examples and benchmark evaluations demonstrate the practicality, efficiency, and scalability of QisMC in verifying realistic quantum programs.
- Abstract(参考訳): 本稿では,Qiskitプログラムのデバッグ専用の量子モデルチェッカーであるQisMCを紹介する。
理論面では、ビロフ・ヴォン・ノイマン論理に基づく量子古典遷移系と量子計算木論理(qCTL)の概念を導入し、その振る舞いをモデル化し、それぞれカイスキットプログラムの特性を規定する。
実装面では、QisMCはトランジッションシステム生成、論理式表現、モデルチェックアルゴリズムを含むエンドツーエンドのフレームワークを提供し、意思決定図に基づく画像計算を効率的に行う。
これらの手法と設計原則は、統合されたプロパティ仕様言語、完全に自動化され徹底的な検証プロセス、反例を生成する機能を含む、以前のQiskitプログラムデバッガよりもQisMCの利点を提供する。
大規模な実証例とベンチマーク評価は、現実的な量子プログラムの検証におけるQisMCの実用性、効率、拡張性を示している。
関連論文リスト
- Many-body Quantum Score: a scalable benchmark for digital and analog quantum processors and first test on a commercial neutral atom device [0.0]
量子処理ユニット(QPU)の能力を評価するために,多体量子スコア(MBQS)を提案する。
MBQSは、QPUが特定の量子クエンチに従って横フィールドイジングモデルの相関関数を確実に再現できる量子ビットの最大数を同定することにより、性能を定量化する。
論文 参考訳(メタデータ) (2026-01-06T23:19:35Z) - Error Mitigation of Fault-Tolerant Quantum Circuits with Soft Information [39.64742821341961]
量子誤り訂正(QEC)の時代において、量子エラー軽減(QEM)が引き続き大きなメリットをもたらすことを示す。
我々は、選択後および実行中止ポリシー、確率的エラーキャンセル、ゼロノイズ外挿という3つの論理レベルのQEM手法を開発し、分析する。
我々の手法は、0.1%未満のショットを捨てながら、論理誤差率を100倍以上に削減する。
論文 参考訳(メタデータ) (2025-12-10T17:49:06Z) - Formal Verification of Variational Quantum Circuits [44.06507276521908]
変分量子回路(VQC)は多くの量子機械学習アルゴリズムの中心的なコンポーネントである。
本稿では,VQCの形式的検証問題に関する基礎的および実践的研究について述べる。
論文 参考訳(メタデータ) (2025-07-14T12:28:32Z) - RhoDARTS: Differentiable Quantum Architecture Search with Density Matrix Simulations [44.13836547616739]
変分量子アルゴリズム(VQA)は、ノイズ中間スケール量子(NISQ)コンピュータを活用するための有望なアプローチである。
与えられたVQA問題を効率的に解く最適な量子回路を選択することは、非自明な作業である。
量子アーキテクチャ探索(QAS)アルゴリズムは、与えられた問題に合わせた量子回路の自動生成を可能にする。
論文 参考訳(メタデータ) (2025-06-04T08:30:35Z) - Quantum Machine Learning in Log-based Anomaly Detection: Challenges and Opportunities [36.437593835024394]
我々は、LogADのコンテキストでQMLモデルを評価するための統合フレームワーク、我々のフレームワークを紹介します。
DeepLog、LogAnomaly、LogRobustといった最先端のメソッドが私たちのフレームワークに含まれている。
評価はQMLの性能に重要な要素、例えば特異性、回路数、回路設計、量子状態符号化にまで及んでいる。
論文 参考訳(メタデータ) (2024-12-18T06:13:49Z) - HamilToniQ: An Open-Source Benchmark Toolkit for Quantum Computers [4.795321943127061]
HamilToniQは、QPU(Quantum Processing Units)の包括的な評価のための、オープンソースのアプリケーション指向ベンチマークツールキットである。
QPUタイプ、トポロジ、マルチQPUシステムを評価する方法論のフレームワークが組み込まれている。
HamilToniQの標準スコアであるH-Scoreは、QPUの忠実度と信頼性を定量化する。
論文 参考訳(メタデータ) (2024-04-22T08:27:14Z) - A Design Framework for the Simulation of Distributed Quantum Computing [2.969582361376132]
大規模量子コンピュータの需要増加は分散量子コンピューティング(DQC)の研究を推し進めている
最近の実験的試みは、そのような設計のためのビルディングブロックのいくつかを実証している。
DQCシステムは、量子ネットワークのインフラによって接続された量子処理ユニットのクラスタである。
論文 参考訳(メタデータ) (2023-06-20T13:52:05Z) - Potential and limitations of quantum extreme learning machines [55.41644538483948]
本稿では,QRCとQELMをモデル化するフレームワークを提案する。
我々の分析は、QELMとQRCの両方の機能と限界をより深く理解するための道を開いた。
論文 参考訳(メタデータ) (2022-10-03T09:32:28Z) - QSAN: A Near-term Achievable Quantum Self-Attention Network [73.15524926159702]
SAM(Self-Attention Mechanism)は機能の内部接続を捉えるのに長けている。
短期量子デバイスにおける画像分類タスクに対して,新しい量子自己注意ネットワーク(QSAN)を提案する。
論文 参考訳(メタデータ) (2022-07-14T12:22:51Z) - Quantum circuit architecture search on a superconducting processor [56.04169357427682]
変分量子アルゴリズム(VQA)は、ファイナンス、機械学習、化学といった様々な分野において、証明可能な計算上の優位性を得るための強力な証拠を示している。
しかし、現代のVQAで利用されるアンザッツは、表現性と訓練性の間のトレードオフのバランスをとることができない。
8量子ビット超伝導量子プロセッサ上でVQAを強化するために,効率的な自動アンサッツ設計技術を適用した最初の実証実験を実証する。
論文 参考訳(メタデータ) (2022-01-04T01:53:42Z) - Supervisory Control of Quantum Discrete Event Systems [2.3097706741644686]
本稿では,量子有限オートマトン(QFA)をモデリング形式として用いて,QDESの基本的枠組みを確立する。
本稿では,QDESのスーパーバイザリコントロールと,従来のDESに対するQDESの本質的な優位性を検証するために,QFAの新たな事例をいくつか提示する。
論文 参考訳(メタデータ) (2021-04-20T04:17:41Z) - Error mitigation and quantum-assisted simulation in the error corrected
regime [77.34726150561087]
量子コンピューティングの標準的なアプローチは、古典的にシミュレート可能なフォールトトレラントな演算セットを促進するという考え方に基づいている。
量子回路の古典的準確率シミュレーションをどのように促進するかを示す。
論文 参考訳(メタデータ) (2021-03-12T20:58:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。