論文の概要: Qafny: A Quantum-Program Verifier

• arxiv url: http://arxiv.org/abs/2211.06411v5
• Date: Mon, 8 Jul 2024 16:28:26 GMT
• ステータス: 処理完了
• システム内更新日: 2024-07-10 05:52:24.720600
• Title: Qafny: A Quantum-Program Verifier
• Title（参考訳）: Qafny: 量子プログラム検証器
• Authors: Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu,
• Abstract要約: 本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。 我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
• 参考スコア（独自算出の注目度）: 39.47005122712576
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Because of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny's automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm.
• Abstract（参考訳）: 量子プログラムの確率論的/非決定論的挙動のため、それらの仕様が正しく実装されていることを確認するために、それらを正式に検証することが非常に望ましい。 しかし、形式的検証も伝統的にかなりの努力を要する。 この課題に対処するために,プログラム検証器Dafnyをベースとした自動証明システムであるQafnyを紹介し,量子プログラムの検証を行う。 コアとなるQafnyは、量子演算を古典的な分離論理フレームワークでモデル化された古典的な配列演算に変換する型誘導量子証明システムを使用している。 証明システムの健全性と完全性を証明するとともに,Qafnyプログラムと仕様をDafnyに変換して自動検証を行うプロトタイプコンパイラを実装した。 次に、量子ウォークアルゴリズム、Groverアルゴリズム、Shorアルゴリズムを含む重要な量子アルゴリズムを効率よく検証する上で、Qafnyの自動機能の有用性について説明する。

関連論文リスト

• Verification of Recursively Defined Quantum Circuits [7.042810171786408]
  本稿では,量子回路の正当性検証のための証明システムを提案する。 応用例としては、(多重量子ビット)制御ゲート、(多重量子ビット)GHZを生成する量子回路などがある。
  論文  参考訳（メタデータ） (2024-04-09T01:35:13Z)
• Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs [3.871660145364189]
  確率的振る舞いに関する局所的推論のための新しい量子ホア論理を提案する。 論理学における証明規則は意味論的意味論に関して健全であることを示す。 我々はHHLやショアのアルゴリズムを含む非自明な量子アルゴリズムの正しさを正式に検証する。
  論文  参考訳（メタデータ） (2023-08-09T07:23:22Z)
• QbC: Quantum Correctness by Construction [4.572433350229651]
  提案するQuantum Correctness by Construction (QbC) は,その仕様から量子プログラムを構築するための手法である。 プリコンディションとポストコンディションを使用してプログラム特性を規定し、その仕様から量子状態におけるプログラム構築のための音質および完全改善ルールを提案する。 このアプローチは、プログラムの詳細を導出する方法を自然に提案し、その過程で重要な設計上の選択を強調します。
  論文  参考訳（メタデータ） (2023-07-28T16:00:57Z)
• quAssert: Automatic Generation of Quantum Assertions [5.263910852465185]
  本稿では,量子回路の静的解析とランダムサンプリングに基づく量子アサーションの自動生成と配置を提案する。 純粋古典状態、重ね合わせ状態、および絡み合った状態などの量子回路の特別な性質を統計的手法を用いて明らかにする。 量子ベンチマークを用いた誤り検出において生成したアサーションの有効性を示す。
  論文  参考訳（メタデータ） (2023-03-02T18:49:14Z)
• Verification of Nondeterministic Quantum Programs [1.9302781323430196]
  非決定論的選択は、実装の詳細を指定せずにプログラムの振る舞いを記述する方法を提供する有用なプログラム構成である。 非決定性は量子プログラミングにも導入され、非決定性量子プログラムの終了は広く分析されてきた。
  論文  参考訳（メタデータ） (2023-02-15T22:37:23Z)
• Delegated variational quantum algorithms based on quantum homomorphic encryption [69.50567607858659]
  変分量子アルゴリズム(VQA)は、量子デバイス上で量子アドバンテージを達成するための最も有望な候補の1つである。 クライアントのプライベートデータは、そのような量子クラウドモデルで量子サーバにリークされる可能性がある。 量子サーバが暗号化データを計算するための新しい量子ホモモルフィック暗号(QHE)スキームが構築されている。
  論文  参考訳（メタデータ） (2023-01-25T07:00:13Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  本稿では,量子状態の知識を必要とせず,量子回路の可換性を検証する回路指向対称性検証を提案する。 特に、従来の量子領域形式を回路指向安定化器に一般化するフーリエ時間安定化器(STS)手法を提案する。
  論文  参考訳（メタデータ） (2021-12-27T21:15:35Z)
• Efficient criteria of quantumness for a large system of qubits [58.720142291102135]
  大規模部分量子コヒーレント系の基本パラメータの無次元結合について論じる。 解析的および数値計算に基づいて、断熱進化中の量子ビット系に対して、そのような数を提案する。
  論文  参考訳（メタデータ） (2021-08-30T23:50:05Z)
• Depth-efficient proofs of quantumness [77.34726150561087]
  量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。 本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
  論文  参考訳（メタデータ） (2021-07-05T17:45:41Z)
• Facial Expression Recognition on a Quantum Computer [68.8204255655161]
  量子機械学習手法を用いて表情認識の可能な解を示す。 適切に定義された量子状態の振幅に符号化されたグラフの隣接行列を操作する量子回路を定義する。
  論文  参考訳（メタデータ） (2021-02-09T13:48:00Z)

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

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