論文の概要: A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm

• arxiv url: http://arxiv.org/abs/2204.07112v1
• Date: Thu, 14 Apr 2022 17:02:34 GMT
• ステータス: 処理完了
• システム内更新日: 2023-02-16 23:58:27.481804
• Title: A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm
• Title（参考訳）: shorの因数化アルゴリズムの形式的エンドツーエンド実装
• Authors: Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, Xiaodi Wu
• Abstract要約: そこで我々はShorの素因数分解アルゴリズムのエンド・ツー・エンド実装を初めて公式に認定した。 私たちのフレームワークを活用することで、ヒューマンエラーの影響を著しく低減できます。
• 参考スコア（独自算出の注目度）: 9.349616752756024
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful if computed answers are correct. While hardware-level decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors -- "bugs". Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside their program, and semi-automatically proves the program correct with respect to it. The proof's validity is automatically confirmed -- certified -- by a "proof assistant". Formal methods have successfully yielded high-assurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present the first formally certified end-to-end implementation of Shor's prime factorization algorithm, developed as part of a novel framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way.
• Abstract（参考訳）: 量子コンピューティング技術は間もなくアルゴリズム性能の革命的な改善をもたらすかもしれないが、計算された答えが正しい場合に限り有用である。 ハードウェアレベルのデコヒーレンスエラーは大きな注目を集めているが、正確性に対する認識されていない障害は、人間のプログラミングエラー -- "バグ" である。 バグを回避、発見、診断するために、古典的なドメインから多くのプログラマになじみのあるテクニックは、そのユニークな特性のため、大規模に、簡単に量子ドメインに移行できない。 この問題に対処するため、我々は量子プログラミングへの形式的手法の適用に取り組んできた。 このような方法で、プログラマはプログラムと一緒に数学的仕様を書き、それに関してプログラムが正しいことを半自動で証明する。 証明の有効性は "proof assistant" によって自動的に確認される。 形式的手法は高保証の古典的ソフトウェアアーティファクトを獲得し、基礎となる技術は主要な数学的定理の証明を生み出した。 量子プログラミングに形式的手法を適用することの実現可能性の実証として、Shorの素因数分解アルゴリズムのエンド・ツー・エンド実装を初めて正式に認定し、一般応用に適用するための新しいフレームワークの一部として開発する。 我々のフレームワークを利用することで、人間のエラーの影響を著しく低減し、原理化された方法で大規模量子アプリケーションの高保証実装を得ることができる。

関連論文リスト

• Towards Classical Software Verification using Quantum Computers [0.0]
  量子コンピュータを用いた古典的プログラムの形式的検証を高速化する可能性を探る。 アウトオブバウンドやオーバーフローのような一般的なエラーの最小例は、異なるソルバでテストされ、量子デバイスで試される。
  論文  参考訳（メタデータ） (2024-04-29T08:43:58Z)
• Quantum Annealing for Single Image Super-Resolution [86.69338893753886]
  単一画像超解像(SISR)問題を解くために,量子コンピューティングに基づくアルゴリズムを提案する。 提案したAQCアルゴリズムは、SISRの精度を維持しつつ、古典的なアナログよりも向上したスピードアップを実現する。
  論文  参考訳（メタデータ） (2023-04-18T11:57:15Z)
• Fault Tolerant Non-Clifford State Preparation for Arbitrary Rotations [3.47670594338385]
  ゲートテレポーテーションのための資源状態を効率的に作成するためのポストセレクションに基づくアルゴリズムを提案する。 提案アルゴリズムは,符号距離による論理誤差の指数的抑制を実証し,耐故障性を実現する。 提案手法は,誤り訂正型およびノイズの多い中間規模量子コンピュータにおいて,量子アルゴリズムのリソース要求を削減するための有望な経路を示す。
  論文  参考訳（メタデータ） (2023-03-30T13:46:52Z)
• Deep Quantum Error Correction [73.54643419792453]
  量子誤り訂正符号(QECC)は、量子コンピューティングのポテンシャルを実現するための鍵となる要素である。 本研究では,新しいエンペンド・ツー・エンドの量子誤りデコーダを効率的に訓練する。 提案手法は,最先端の精度を実現することにより,QECCのニューラルデコーダのパワーを実証する。
  論文  参考訳（メタデータ） (2023-01-27T08:16:26Z)
• Automatic Implementation and Evaluation of Error-Correcting Codes for Quantum Computing: An Open-Source Framework for Quantum Error Correction [2.1801327670218855]
  実際の量子コンピュータは、計算中にエラーを引き起こす頻繁なノイズ効果に悩まされている。 量子エラー訂正コードは、対応するエラーを識別し修正する手段を提供することで、この問題に対処する。 本稿では, あるアプリケーションに対してエラー訂正コードを自動的に適用し, その後に自動ノイズ対応量子回路シミュレーションを行うオープンソースフレームワークを提案する。
  論文  参考訳（メタデータ） (2023-01-13T19:12:22Z)
• Qafny: A Quantum-Program Verifier [39.47005122712576]
  本稿では,量子プログラムの自動検証システムであるQafnyを紹介する。 Qafnyの核心は、量子演算を古典的な配列演算に変換する型誘導量子証明システムである。 我々はQafnyが量子ウォークアルゴリズム、Groverのアルゴリズム、Shorのアルゴリズムを含む重要な量子アルゴリズムを効率的に検証する方法を示す。
  論文  参考訳（メタデータ） (2022-11-11T18:50:52Z)
• Quantum circuit debugging and sensitivity analysis via local inversions [62.997667081978825]
  本稿では,回路に最も影響を及ぼす量子回路の断面をピンポイントする手法を提案する。 我々は,IBM量子マシン上に実装されたアルゴリズム回路の例に応用して,提案手法の実用性と有効性を示す。
  論文  参考訳（メタデータ） (2022-04-12T19:39:31Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  本稿では,量子状態の知識を必要とせず,量子回路の可換性を検証する回路指向対称性検証を提案する。 特に、従来の量子領域形式を回路指向安定化器に一般化するフーリエ時間安定化器(STS)手法を提案する。
  論文  参考訳（メタデータ） (2021-12-27T21:15:35Z)
• Hardware-Efficient, Fault-Tolerant Quantum Computation with Rydberg Atoms [55.41644538483948]
  我々は中性原子量子コンピュータにおいてエラー源の完全な特徴付けを行う。 計算部分空間外の状態への原子量子ビットの崩壊に伴う最も重要なエラーに対処する,新しい,明らかに効率的な手法を開発した。 我々のプロトコルは、アルカリ原子とアルカリ原子の両方にエンコードされた量子ビットを持つ最先端の中性原子プラットフォームを用いて、近い将来に実装できる。
  論文  参考訳（メタデータ） (2021-05-27T23:29:53Z)
• 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)

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

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