論文の概要: A Practical Quantum Hoare Logic with Classical Variables, I

• arxiv url: http://arxiv.org/abs/2412.09869v1
• Date: Fri, 13 Dec 2024 05:28:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-16 15:01:33.016675
• Title: A Practical Quantum Hoare Logic with Classical Variables, I
• Title（参考訳）: 古典的変数を持つ実用的量子ホア論理I
• Authors: Mingsheng Ying,
• Abstract要約: 古典変数を持つ量子プログラムを推論するためのHoare型論理について述べる。 私たちのアプローチは、以前の作業よりもいくつかの改善を提供します。 これは量子配列とパラメータ化された量子ゲートを含む古典変数を持つ量子プログラムに適用される。
• 参考スコア（独自算出の注目度）: 2.789440475527173
• License:
• Abstract: In this paper, we present a Hoare-style logic for reasoning about quantum programs with classical variables. Our approach offers several improvements over previous work: (1) Enhanced expressivity of the programming language: Our logic applies to quantum programs with classical variables that incorporate quantum arrays and parameterised quantum gates, which have not been addressed in previous research on quantum Hoare logic, either with or without classical variables. (2) Intuitive correctness specifications: In our logic, preconditions and postconditions for quantum programs with classical variables are specified as a pair consisting of a classical first-order logical formula and a quantum predicate formula (possibly parameterised by classical variables). These specifications offer greater clarity and align more closely with the programmer's intuitive understanding of quantum and classical interactions. (3) Simplified proof system: By introducing a novel idea in formulating a proof rule for reasoning about quantum measurements, along with (2), we develop a proof system for quantum programs that requires only minimal modifications to classical Hoare logic. Furthermore, this proof system can be effectively and conveniently combined with classical first-order logic to verify quantum programs with classical variables. As a result, the learning curve for quantum program verification techniques is significantly reduced for those already familiar with classical program verification techniques, and existing tools for verifying classical programs can be more easily adapted for quantum program verification.
• Abstract（参考訳）: 本稿では,古典変数を持つ量子プログラムを推論するためのHoare型論理について述べる。 1) プログラミング言語の表現性の向上: 量子配列とパラメータ化量子ゲートを組み込んだ古典変数を持つ量子プログラムに適用する。 2)直観的正当性仕様:古典変数を持つ量子プログラムの前提条件と後条件は古典的一階述語論理式と量子述語論理式(古典変数によってパラメータ化される可能性がある)からなる対として規定される。 これらの仕様はより明確で、プログラマの量子と古典的な相互作用に対する直感的な理解とより密接に一致している。 (3) 簡単な証明システム:(2) とともに古典ホア論理への最小限の変更しか必要としない量子プログラムの証明システムを開発する。 さらに、この証明システムは、古典的な変数を持つ量子プログラムを検証するために、古典的な一階述語論理と有効かつ便利な組み合わせが可能である。 その結果、古典的プログラム検証技術に慣れ親しんだ者に対しては、量子プログラム検証技術の学習曲線が大幅に減少し、古典的プログラム検証のための既存のツールをより容易に量子プログラム検証に適合させることができる。

関連論文リスト

• Quantum Machine Learning: from physics to software engineering [58.720142291102135]
  古典的な機械学習アプローチが量子コンピュータの設備改善にどのように役立つかを示す。 量子アルゴリズムと量子コンピュータは、古典的な機械学習タスクを解くのにどのように役立つかについて議論する。
  論文  参考訳（メタデータ） (2023-01-04T23:37:45Z)
• Anticipative measurements in hybrid quantum-classical computation [68.8204255655161]
  量子計算を古典的な結果によって補う手法を提案する。 予測の利点を生かして、新しいタイプの量子測度がもたらされる。 予測量子測定では、古典計算と量子計算の結果の組み合わせは最後にのみ起こる。
  論文  参考訳（メタデータ） (2022-09-12T15:47:44Z)
• Classical surrogates for quantum learning models [0.7734726150561088]
  本稿では,訓練された量子学習モデルから効率的に得られる古典的モデルである古典的サロゲートの概念を紹介する。 我々は、よく解析された再アップロードモデルの大規模なクラスが古典的なサロゲートを持つことを示す。
  論文  参考訳（メタデータ） (2022-06-23T14:37:02Z)
• Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs [1.1878820609988696]
  量子変数を持つ一階述語論理は、量子プログラムの様々な性質を特定し、推論するためのアサーション言語として必要とされる。 本稿では,Birkhoff-von Neumann量子論理を量子変数上の普遍的および存在的量子化器を用いて一階拡張する。
  論文  参考訳（メタデータ） (2022-05-04T08:57:44Z)
• Qunity: A Unified Language for Quantum and Classical Computing (Extended Version) [3.5348690973777006]
  量子プログラミング言語Quinityを紹介します。 Qunityは量子コンピューティングを古典コンピューティングの自然な一般化として扱う。 我々はQunityがいくつかの量子アルゴリズムをきれいに表現する方法を示す。
  論文  参考訳（メタデータ） (2022-04-26T15:34:22Z)
• LQP: The Dynamic Logic of Quantum Information [77.34726150561087]
  本稿では,複合量子システムにおける情報フローの推論のための動的論理形式について紹介する。 本稿では,この論理の文法,関係意味論,音響証明システムについて述べる。 アプリケーションとしては,テレポーテーションプロトコルと標準量子秘密共有プロトコルに対して,正式な正当性を与えるために,我々のシステムを利用する。
  論文  参考訳（メタデータ） (2021-10-04T12:20:23Z)
• 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)
• On the Principles of Differentiable Quantum Programming Languages [13.070557640180004]
  変分量子回路(VQC)は、最も重要な短期量子応用の1つであると予測されている。 本稿では,量子回路における自己微分法の最初の形式化を提案する。
  論文  参考訳（メタデータ） (2020-04-02T16:46:13Z)
• From a quantum theory to a classical one [117.44028458220427]
  量子対古典的交叉を記述するための形式的アプローチを提示し議論する。 この手法は、1982年にL. Yaffeによって、大きな$N$の量子場理論に取り組むために導入された。
  論文  参考訳（メタデータ） (2020-04-01T09:16:38Z)

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

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