論文の概要: Verification of Nondeterministic Quantum Programs

• arxiv url: http://arxiv.org/abs/2302.07973v1
• Date: Wed, 15 Feb 2023 22:37:23 GMT
• ステータス: 処理完了
• システム内更新日: 2023-02-17 15:37:25.385373
• Title: Verification of Nondeterministic Quantum Programs
• Title（参考訳）: 非決定論的量子プログラムの検証
• Authors: Yuan Feng and Yingte Xu
• Abstract要約: 非決定論的選択は、実装の詳細を指定せずにプログラムの振る舞いを記述する方法を提供する有用なプログラム構成である。 非決定性は量子プログラミングにも導入され、非決定性量子プログラムの終了は広く分析されてきた。
• 参考スコア（独自算出の注目度）: 1.9302781323430196
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and the termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian operators on the associated Hilbert space. Hoare-type logic systems for partial and total correctness are proposed, which turn out to be both sound and relatively complete with respect to their corresponding semantic correctness. To show the utility of these proof systems, we analyse some quantum algorithms, such as quantum error correction scheme, the Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.
• Abstract（参考訳）: 非決定論的選択は、実装の詳細を指定せずにプログラムの振る舞いを記述する方法を提供する有用なプログラム構成である。 ソフトウェア開発で有用であることが証明された、プログラムの段階的な洗練をサポートする。 非決定性は量子プログラミングにも導入され、非決定性量子プログラムの終了は広く分析されてきた。 本稿では,ヒルベルト空間上のエルミート作用素の集合によって性質が与えられる非決定論的量子プログラムの検証について,終端解析を超えて検討する。 部分的および全体的正しさに対するフーア型論理系を提案し, 対応する意味的正しさに関して, 音質と相対的に完全であることが判明した。 これらの証明システムの有用性を示すために、量子誤差補正スキーム、deutschアルゴリズム、非決定論的量子ウォークなどの量子アルゴリズムを解析する。 最後に、非決定論的量子プログラムの自動推論を支援するために、証明アシスタントプロトタイプが実装されている。

関連論文リスト

• Refinement calculus of quantum programs with projective assertions [5.151896714190243]
  本稿では,量子プログラムに適した微積分法を提案する。 まず、量子内における非決定論的プログラムの部分的正当性について検討する。 また,ポストコンディションを最も弱いリベラルなポストコンディションに変換する際のセマンティクスも提示する。
  論文  参考訳（メタデータ） (2023-11-23T22:12:57Z)
• QbC: Quantum Correctness by Construction [4.572433350229651]
  提案するQuantum Correctness by Construction (QbC) は,その仕様から量子プログラムを構築するための手法である。 プリコンディションとポストコンディションを使用してプログラム特性を規定し、その仕様から量子状態におけるプログラム構築のための音質および完全改善ルールを提案する。 このアプローチは、プログラムの詳細を導出する方法を自然に提案し、その過程で重要な設計上の選択を強調します。
  論文  参考訳（メタデータ） (2023-07-28T16:00:57Z)
• Quantum Conformal Prediction for Reliable Uncertainty Quantification in Quantum Machine Learning [47.991114317813555]
  量子モデルは暗黙の確率予測器を実装し、測定ショットを通じて各入力に対して複数のランダムな決定を生成する。 本稿では、そのようなランダム性を利用して、モデルの不確実性を確実に捉えることができる分類と回帰の両方の予測セットを定義することを提案する。
  論文  参考訳（メタデータ） (2023-04-06T22:05:21Z)
• Design by Contract Framework for Quantum Software [1.9988400064884826]
  本稿では,量子ソフトウェアのための設計・設計フレームワークを提案する。 特定の手順によって構築された全ての量子回路の入力および出力状態に関するアサーションを提供する。 我々のフレームワークは量子ソフトウェアの全手順を検証するのに十分な表現力を持っている。
  論文  参考訳（メタデータ） (2023-03-31T00:21:28Z)
• Quantum process tomography of continuous-variable gates using coherent states [49.299443295581064]
  ボソニックモード超伝導回路におけるコヒーレント状態量子プロセストモグラフィ(csQPT)の使用を実証する。 符号化量子ビット上の変位とSNAP演算を用いて構築した論理量子ゲートを特徴付けることにより,本手法の結果を示す。
  論文  参考訳（メタデータ） (2023-03-02T18:08:08Z)
• Qafny: A Quantum-Program Verifier [39.47005122712576]
  本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。 我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
  論文  参考訳（メタデータ） (2022-11-11T18:50:52Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  本稿では,量子状態の知識を必要とせず,量子回路の可換性を検証する回路指向対称性検証を提案する。 特に、従来の量子領域形式を回路指向安定化器に一般化するフーリエ時間安定化器(STS)手法を提案する。
  論文  参考訳（メタデータ） (2021-12-27T21:15:35Z)
• Characterizing quantum instruments: from non-demolition measurements to quantum error correction [48.43720700248091]
  量子情報処理では、量子演算はしばしば古典的なデータをもたらす測定とともに処理される。 非単位の動的プロセスは、一般的な量子チャネルの記述が時間進化を記述するのに失敗するシステムで起こりうる。 量子測定は古典的な出力と測定後の量子状態の両方を計測するいわゆる量子機器によって正しく扱われる。
  論文  参考訳（メタデータ） (2021-10-13T18:00:13Z)
• Preparation of quantum superposition using partial negation [1.911678487931003]
  準備過程の速度と準備された重ね合わせの精度は、任意の量子アルゴリズムの成功に特に重要である。 提案手法は、$mathcalO(n)$のステップで必要となる量子重ね合わせを準備するために使用できる。
  論文  参考訳（メタデータ） (2021-09-29T11:57:44Z)
• Facial Expression Recognition on a Quantum Computer [68.8204255655161]
  量子機械学習手法を用いて表情認識の可能な解を示す。 適切に定義された量子状態の振幅に符号化されたグラフの隣接行列を操作する量子回路を定義する。
  論文  参考訳（メタデータ） (2021-02-09T13:48:00Z)

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

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