論文の概要: QbC: Quantum Correctness by Construction

• arxiv url: http://arxiv.org/abs/2307.15641v1
• Date: Fri, 28 Jul 2023 16:00:57 GMT
• ステータス: 処理完了
• システム内更新日: 2023-07-31 12:03:52.535104
• Title: QbC: Quantum Correctness by Construction
• Title（参考訳）: QbC: 構成による量子精度
• Authors: Anurudh Peduri, Ina Schaefer, Michael Walter
• Abstract要約: 提案するQuantum Correctness by Construction (QbC) は,その仕様から量子プログラムを構築するための手法である。 プリコンディションとポストコンディションを使ってプログラム特性を規定し、量子時相言語で正しいプログラムを構築するための改良ルールセットを提案する。 このアプローチは、プログラムの詳細を導出する方法を自然に提案し、その過程で重要な設計上の選択を強調します。
• 参考スコア（独自算出の注目度）: 5.84115060036817
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a complete program and only then verifies its correctness. In this work, we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose a set of refinement rules to construct correct programs in a quantum while language. We validate QbC by constructing quantum programs for two idiomatic problems, teleportation and search, from their specification. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play an important role in supporting the design and taxonomization of quantum algorithms and software.
• Abstract（参考訳）: 量子アルゴリズムの急速な進歩と複雑さの増大により、量子プログラムの正確性が大きな関心事となっている。 過去数年間の研究で、量子ホア論理のような証明システムを用いて量子プログラムを正式に検証するための様々なアプローチが提案されている。 これらの以前のアプローチはすべてポストホックで、まず完全なプログラムを実装し、その正しさを検証します。 本稿では, 量子プログラムの仕様から, 正確性を保証する方法で構築する手法として, 構成による量子正当性(QbC)を提案する。 我々は,プログラム特性の指定にプリ条件とポスト条件を用い,量子ビット言語で正しいプログラムを構築するための改良規則を提案する。 本稿では,2つの慣用問題,テレポーテーションとサーチの量子プログラムを構築することでQbCを検証する。 このアプローチは、プログラムの詳細を導出する方法を自然に示唆し、その過程で重要な設計選択を強調する。 このように、QbCは量子アルゴリズムとソフトウェアの設計と分類を支援する上で重要な役割を果たすと信じている。

関連論文リスト

• Quantum Subroutine for Variance Estimation: Algorithmic Design and Applications [80.04533958880862]
  量子コンピューティングは、アルゴリズムを設計する新しい方法の基礎となる。 どの場の量子スピードアップが達成できるかという新たな課題が生じる。 量子サブルーチンの設計は、従来のサブルーチンよりも効率的で、新しい強力な量子アルゴリズムに固い柱を向ける。
  論文  参考訳（メタデータ） (2024-02-26T09:32:07Z)
• Design by Contract Framework for Quantum Software [1.9988400064884826]
  本稿では,量子ソフトウェアのための設計・設計フレームワークを提案する。 特定の手順によって構築された全ての量子回路の入力および出力状態に関するアサーションを提供する。 我々のフレームワークは量子ソフトウェアの全手順を検証するのに十分な表現力を持っている。
  論文  参考訳（メタデータ） (2023-03-31T00:21:28Z)
• Simple Tests of Quantumness Also Certify Qubits [69.96668065491183]
  量子性の検定は、古典的検証者が証明者が古典的でないことを(のみ)証明できるプロトコルである。 我々は、あるテンプレートに従う量子性のテストを行い、(Kalai et al., 2022)のような最近の提案を捉えた。 すなわち、同じプロトコルは、証明可能なランダム性や古典的な量子計算のデリゲートといったアプリケーションの中心にあるビルディングブロックであるqubitの認定に使用できる。
  論文  参考訳（メタデータ） (2023-03-02T14:18:17Z)
• 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)
• Depth-efficient proofs of quantumness [77.34726150561087]
  量子性の証明は、古典的検証器が信頼できない証明器の量子的利点を効率的に証明できる挑戦応答プロトコルの一種である。 本稿では、証明者が量子回路を一定深度でしか実行できない量子性構成の証明を2つ与える。
  論文  参考訳（メタデータ） (2021-07-05T17:45:41Z)
• On exploring the potential of quantum auto-encoder for learning quantum systems [60.909817434753315]
  そこで我々は,古典的な3つのハードラーニング問題に対処するために,QAEに基づく効果的な3つの学習プロトコルを考案した。 私たちの研究は、ハード量子物理学と量子情報処理タスクを達成するための高度な量子学習アルゴリズムの開発に新たな光を当てています。
  論文  参考訳（メタデータ） (2021-06-29T14:01:40Z)
• Quantum walk processes in quantum devices [55.41644538483948]
  グラフ上の量子ウォークを量子回路として表現する方法を研究する。 提案手法は,量子ウォークアルゴリズムを量子コンピュータ上で効率的に実装する方法である。
  論文  参考訳（メタデータ） (2020-12-28T18:04:16Z)
• Proving Quantum Programs Correct [3.2513560268591735]
  グローバーのアルゴリズムや量子位相推定を含む様々な量子アルゴリズムの正確性を検証する。 量子コンテキストにおける形式的検証の成功と課題の両方を強調することを目的としている。
  論文  参考訳（メタデータ） (2020-10-03T00:55:41Z)
• Electronic structure with direct diagonalization on a D-Wave quantum annealer [62.997667081978825]
  本研究は、D-Wave 2000Q量子アニール上の分子電子ハミルトニアン固有値-固有ベクトル問題を解くために、一般量子アニール固有解法(QAE)アルゴリズムを実装した。 そこで本研究では,D-Waveハードウェアを用いた各種分子系における基底および電子励起状態の取得について述べる。
  論文  参考訳（メタデータ） (2020-09-02T22:46:47Z)
• On the Principles of Differentiable Quantum Programming Languages [13.070557640180004]
  変分量子回路(VQC)は、最も重要な短期量子応用の1つであると予測されている。 本稿では,量子回路における自己微分法の最初の形式化を提案する。
  論文  参考訳（メタデータ） (2020-04-02T16:46:13Z)

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

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