Fugu-MT 論文翻訳(概要): Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs

論文の概要: Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs

arxiv url: http://arxiv.org/abs/2308.04741v1
Date: Wed, 9 Aug 2023 07:23:22 GMT
ステータス: 処理完了
システム内更新日: 2023-08-10 14:52:32.386195
Title: Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
Title（参考訳）: 古典量子プログラムの確率的振る舞いに関する局所的推論
Authors: Yuxin Deng, Huiling Wu, Ming Xu
Abstract要約: 確率的振る舞いに関する局所的推論のための新しい量子ホア論理を提案する。論理学における証明規則は意味論的意味論に関して健全であることを示す。我々はHHLやショアのアルゴリズムを含む非自明な量子アルゴリズムの正しさを正式に検証する。
参考スコア（独自算出の注目度）: 2.8135066372665953
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms.
Abstract（参考訳）: 古典的構成と量子的構成の両方でプログラムの機能的正当性を検証することは難しい課題である。量子測定と非有界なループによる確率的振る舞いの存在は検証作業を大幅に複雑にする。本稿では,確率特性を規定する分布公式を導入することにより,確率的挙動に関する局所的推論のための新しい量子ホア論理を提案する。論理の証明規則は意味論的意味論に関して健全であることを示す。論理の有効性を示すために, hhl と shor のアルゴリズムを含む非自明な量子アルゴリズムの正しさを正式に検証する。

関連論文リスト

BI-based Reasoning about Quantum Programs with Heap Manipulations [5.744265100221585]
ヒープ操作を伴う量子プログラミング言語Q While-hpのセマンティクスについて述べる。我々は,意味を分離するための解釈を含む,BIスタイルの量子論理を開発する。次に、この量子BIスタイルの論理をアサーション言語として採用し、ヒープ制御量子プログラムを推論する。
論文参考訳（メタデータ） (2024-09-16T10:34:45Z)
A refinement of the argument of local realism versus quantum mechanics by algorithmic randomness [0.0]
量子力学において、確率の概念は決定的な役割を果たす。現代数学では、確率論は測度論以外に何の意味も持たない。本稿では, 定性原理とよばれるボルンの規則を改良し, 操作方法による測定結果の特性を規定する。
論文参考訳（メタデータ） (2023-12-20T18:22:42Z)
Verification of Nondeterministic Quantum Programs [1.9302781323430196]
非決定論的選択は、実装の詳細を指定せずにプログラムの振る舞いを記述する方法を提供する有用なプログラム構成である。非決定性は量子プログラミングにも導入され、非決定性量子プログラムの終了は広く分析されてきた。
論文参考訳（メタデータ） (2023-02-15T22:37:23Z)
Qafny: A Quantum-Program Verifier [39.47005122712576]
本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
論文参考訳（メタデータ） (2022-11-11T18:50:52Z)
Entanglement and coherence in Bernstein-Vazirani algorithm [58.720142291102135]
Bernstein-Vaziraniアルゴリズムは、オラクルに符号化されたビット文字列を決定できる。我々はベルンシュタイン・ヴァジラニアルゴリズムの量子資源を詳細に分析する。絡み合いがない場合、初期状態における量子コヒーレンス量とアルゴリズムの性能が直接関係していることが示される。
論文参考訳（メタデータ） (2022-05-26T20:32:36Z)
Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
本稿では,量子状態の知識を必要とせず,量子回路の可換性を検証する回路指向対称性検証を提案する。特に、従来の量子領域形式を回路指向安定化器に一般化するフーリエ時間安定化器(STS)手法を提案する。
論文参考訳（メタデータ） (2021-12-27T21:15:35Z)
The Logic of Quantum Programs [77.34726150561087]
本稿では,量子プログラムにおける情報フローの論理計算について述べる。特に、複素量子系における量子測定、ユニタリ進化、絡み合いを扱うことができる動的論理を導入する。
論文参考訳（メタデータ） (2021-09-14T16:08:37Z)
Depth-efficient proofs of quantumness [77.34726150561087]
量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
論文参考訳（メタデータ） (2021-07-05T17:45:41Z)
Secure Two-Party Quantum Computation Over Classical Channels [63.97763079214294]
古典的アリス(Alice)と量子的ボブ(Quantum Bob)が古典的なチャネルを通してのみ通信できるような設定を考える。悪質な量子逆数の場合,ブラックボックスシミュレーションを用いた2次元量子関数を実現することは,一般に不可能であることを示す。我々は、QMA関係Rの古典的量子知識(PoQK)プロトコルを入力として、古典的当事者によって検証可能なRのゼロ知識PoQKを出力するコンパイラを提供する。
論文参考訳（メタデータ） (2020-10-15T17:55:31Z)
Quantum Hoare logic with classical variables [3.1181601933418897]
古典変数と量子変数の両方を含む簡単な時相言語に対して量子ホア論理を提案する。古典量子状態とそれに対応するアサーションの新たな定義により、論理体系は非常に単純であり、古典的プログラムの伝統的なホア論理と類似している。
論文参考訳（メタデータ） (2020-08-15T23:56:18Z)
Using Quantum Metrological Bounds in Quantum Error Correction: A Simple Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
本稿では、量子誤り訂正符号の品質と、論理ゲートの普遍的な集合を達成する能力とを結びつける、近似したイージン・クニル定理の証明を示す。我々の導出は、一般的な量子気象プロトコルにおける量子フィッシャー情報に強力な境界を用いる。
論文参考訳（メタデータ） (2020-04-24T17:58:10Z)

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