論文の概要: Quantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification

• arxiv url: http://arxiv.org/abs/2211.06411v1
• Date: Fri, 11 Nov 2022 18:50:52 GMT
• ステータス: 処理完了
• システム内更新日: 2023-01-19 18:09:00.860599
• Title: Quantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification
• Title（参考訳）: 量子自然証明:ハイブリッド量子古典的プログラム検証の新しい視点
• Authors: Liyi Li, Mingwei Zhu, Yi Lee, Le Chang, Xiaodi Wu
• Abstract要約: 本稿では,量子古典アルゴリズムの自動検証システムである量子自然証明(QNP)を提案する。 QNPはQafnyという名前の型誘導量子証明システムであり、量子演算を古典的な配列演算と見なしている。 Qafnyは量子回路にコンパイルでき、検証された全ての量子プログラムを量子マシン上で実行することができる。
• 参考スコア（独自算出の注目度）: 8.204279513963261
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Many quantum programs are assured by formal verification, but such verification is usually laborious and time-consuming. This paper proposes quantum natural proof (QNP), an automated proof system for verifying hybrid quantum-classical algorithms. Natural proofs are a subclass of proofs that are amenable to completely automated reasoning, provide sound but incomplete procedures, and capture common reasoning tactics in program verification. The core of QNP is a type-guided quantum proof system, named Qafny, which views quantum operations as some classical array operations that can be modeled as proof rules in a classical separation logic framework, suitable for automated reasoning. We proved the soundness and completeness of the Qafny proof system as well as the soundness of the proof system compilation from Qafny to Dafny. By using the QNP implementation in Dafny, automated verification can be efficiently perform for many hybrid quantum-classical algorithms, including GHZ, Shor's, Grover's, and quantum walk algorithms, which saves a great amount of human efforts. In addition, quantum programs written in Qafny can be compiled to quantum circuits so that every verified quantum program can be run on a quantum machine.
• Abstract（参考訳）: 多くの量子プログラムは形式的検証によって保証されるが、そのような検証は通常、手間と時間を要する。 本稿では,ハイブリッド量子古典アルゴリズムの自動検証システムである量子自然証明(QNP)を提案する。 自然証明は、完全に自動化された推論、健全だが不完全な手順を提供し、プログラム検証における一般的な推論の戦術を捉えることができる証明のサブクラスである。 QNPの中核はQafnyという名前の型誘導量子証明システムであり、量子演算を古典的な配列演算とみなし、自動推論に適した古典的な分離論理フレームワークの証明規則としてモデル化することができる。 我々は、Qafnyの証明システムの健全性と完全性、およびQafnyからDafnyへの証明システムのコンパイルの健全性を示した。 dafnyのqnp実装を使用することで、ghz、shor's、grover's、quantum walkアルゴリズムなど、多数のハイブリッド量子古典アルゴリズムに対して、自動化された検証を効率的に実行することができる。 さらに、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)

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

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