論文の概要: Proving Quantum Programs Correct
- arxiv url: http://arxiv.org/abs/2010.01240v4
- Date: Tue, 13 Jul 2021 18:50:44 GMT
- ステータス: 処理完了
- システム内更新日: 2023-04-30 02:16:22.288765
- Title: Proving Quantum Programs Correct
- Title(参考訳): 量子プログラムを正しく証明する
- Authors: Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li and Michael Hicks
- Abstract要約: グローバーのアルゴリズムや量子位相推定を含む様々な量子アルゴリズムの正確性を検証する。
量子コンテキストにおける形式的検証の成功と課題の両方を強調することを目的としている。
- 参考スコア(独自算出の注目度): 3.2513560268591735
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: As quantum computing progresses steadily from theory into practice,
programmers will face a common problem: How can they be sure that their code
does what they intend it to do? This paper presents encouraging results in the
application of mechanized proof to the domain of quantum programming in the
context of the SQIR development. It verifies the correctness of a range of a
quantum algorithms including Grover's algorithm and quantum phase estimation, a
key component of Shor's algorithm. In doing so, it aims to highlight both the
successes and challenges of formal verification in the quantum context and
motivate the theorem proving community to target quantum computing as an
application domain.
- Abstract(参考訳): 量子コンピューティングが理論から実践へと着実に進むにつれ、プログラマは共通の問題に直面することになる。
本稿では、SQIR開発における量子プログラミングの領域への機械的証明の適用に関する奨励的な結果を示す。
これは、ショアのアルゴリズムの重要な構成要素であるグローバーのアルゴリズムや量子位相推定を含む量子アルゴリズムの範囲の正しさを検証する。
そうすることで、量子コンテキストにおける形式的検証の成功と課題の両方を強調し、アプリケーションドメインとして量子コンピューティングをターゲットとする定理証明コミュニティを動機付けることを目指している。
関連論文リスト
- Quantum Circuit Ansatz: Patterns of Abstraction and Reuse of Quantum Algorithm Design [3.8425905067219492]
本稿では,量子回路のアンサーゼを分類したカタログを提案する。
各アンザッツは、意図、モチベーション、適用性、回路図、実装、例などの詳細とともに記述される。
量子アルゴリズム設計におけるそれらの応用を説明するための実例が提供されている。
論文 参考訳(メタデータ) (2024-05-08T12:44:37Z) - Quantum Subroutine for Variance Estimation: Algorithmic Design and Applications [80.04533958880862]
量子コンピューティングは、アルゴリズムを設計する新しい方法の基礎となる。
どの場の量子スピードアップが達成できるかという新たな課題が生じる。
量子サブルーチンの設計は、従来のサブルーチンよりも効率的で、新しい強力な量子アルゴリズムに固い柱を向ける。
論文 参考訳(メタデータ) (2024-02-26T09:32:07Z) - Efficient Quantum Modular Arithmetics for the ISQ Era [0.0]
本研究は, モジュラー演算関数の精度向上を目的とした, 量子回路の配列について述べる。
我々はPennyLane量子ソフトウェアにおける理論的枠組みと実践的実装を提供する。
論文 参考訳(メタデータ) (2023-11-14T21:34:39Z) - QbC: Quantum Correctness by Construction [4.572433350229651]
提案するQuantum Correctness by Construction (QbC) は,その仕様から量子プログラムを構築するための手法である。
プリコンディションとポストコンディションを使用してプログラム特性を規定し、その仕様から量子状態におけるプログラム構築のための音質および完全改善ルールを提案する。
このアプローチは、プログラムの詳細を導出する方法を自然に提案し、その過程で重要な設計上の選択を強調します。
論文 参考訳(メタデータ) (2023-07-28T16:00:57Z) - Quantum Annealing for Single Image Super-Resolution [86.69338893753886]
単一画像超解像(SISR)問題を解くために,量子コンピューティングに基づくアルゴリズムを提案する。
提案したAQCアルゴリズムは、SISRの精度を維持しつつ、古典的なアナログよりも向上したスピードアップを実現する。
論文 参考訳(メタデータ) (2023-04-18T11:57:15Z) - Qafny: A Quantum-Program Verifier [39.47005122712576]
本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。
Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。
我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
論文 参考訳(メタデータ) (2022-11-11T18:50:52Z) - Optimal Stochastic Resource Allocation for Distributed Quantum Computing [50.809738453571015]
本稿では,分散量子コンピューティング(DQC)のためのリソース割り当て方式を提案する。
本評価は,提案手法の有効性と,量子コンピュータとオンデマンド量子コンピュータの両立性を示すものである。
論文 参考訳(メタデータ) (2022-09-16T02:37:32Z) - Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
本稿では,量子状態の知識を必要とせず,量子回路の可換性を検証する回路指向対称性検証を提案する。
特に、従来の量子領域形式を回路指向安定化器に一般化するフーリエ時間安定化器(STS)手法を提案する。
論文 参考訳(メタデータ) (2021-12-27T21:15:35Z) - Formal Verification of Quantum Programs: Theory, Tools and Challenges [0.0]
サーベイは、量子プログラムの形式的検証分野への短い導入を目標としている。
この調査は、この分野が将来直面するであろういくつかの課題、すなわち複雑な量子アルゴリズムの開発について調査する。
論文 参考訳(メタデータ) (2021-10-04T11:00:48Z) - On exploring the potential of quantum auto-encoder for learning quantum systems [60.909817434753315]
そこで我々は,古典的な3つのハードラーニング問題に対処するために,QAEに基づく効果的な3つの学習プロトコルを考案した。
私たちの研究は、ハード量子物理学と量子情報処理タスクを達成するための高度な量子学習アルゴリズムの開発に新たな光を当てています。
論文 参考訳(メタデータ) (2021-06-29T14:01:40Z) - An Application of Quantum Annealing Computing to Seismic Inversion [55.41644538483948]
小型地震インバージョン問題を解決するために,D波量子アニールに量子アルゴリズムを適用した。
量子コンピュータによって達成される精度は、少なくとも古典的コンピュータと同程度である。
論文 参考訳(メタデータ) (2020-05-06T14:18:44Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。