論文の概要: Qafny: Quantum Program Verification Through Type-guided Classical Separation Logic

• arxiv url: http://arxiv.org/abs/2211.06411v2
• Date: Wed, 12 Jul 2023 13:47:59 GMT
• ステータス: 処理完了
• システム内更新日: 2023-07-13 20:17:47.529026
• Title: Qafny: Quantum Program Verification Through Type-guided Classical Separation Logic
• Title（参考訳）: Qafny: タイプ誘導古典分離論理による量子プログラム検証
• Authors: Liyi Li, Mingwei Zhu, Rance Cleaveland, Yi Lee, Le Chang, Xiaodi Wu
• Abstract要約: 本稿では,量子プログラムの検証を目的とした自動証明システムであるQafnyを紹介する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。 我々は、量子ウォークアルゴリズム、グローバーの探索アルゴリズム、ショアの因数分解アルゴリズムなど、顕著な量子アルゴリズムを効率的に検証する方法を実証する。
• 参考スコア（独自算出の注目度）: 7.2169657809052525
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Formal verification has been proven instrumental to ensure that quantum programs implement their specifications but often requires a significant investment of time and labor. To address this challenge, we present Qafny, an automated proof system designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations. By modeling these operations as proof rules within a classical separation logic framework, Qafny provides automated support for the reasoning process that would otherwise be tedious and time-consuming. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs both into the Dafny programming language and into executable quantum circuits. Using Qafny, we demonstrate how to efficiently verify prominent quantum algorithms, including quantum-walk algorithms, Grover's search algorithm, and Shor's factoring algorithm, with significantly reduced human efforts.
• Abstract（参考訳）: 形式的検証は、量子プログラムが仕様を実装していることを保証するのに役立っているが、しばしば時間と労力のかなりの投資を必要とする。 この課題に対処するために,量子プログラムの検証用に設計された自動証明システムであるqafnyを提案する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。 これらの操作を古典的な分離論理フレームワーク内の証明ルールとしてモデル化することで、qafnyは退屈で時間のかかる推論プロセスに対する自動サポートを提供する。 我々は証明システムの健全性と完全性を証明し、qafnyプログラムをdafnyプログラミング言語と実行可能な量子回路に変換するプロトタイプコンパイラを実装した。 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)

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

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