論文の概要: Formal Modeling and Verification of Grover's Algorithm

• arxiv url: http://arxiv.org/abs/2601.02435v1
• Date: Mon, 05 Jan 2026 06:56:21 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-07 17:02:12.663834
• Title: Formal Modeling and Verification of Grover's Algorithm
• Title（参考訳）: グローバーアルゴリズムの形式的モデリングと検証
• Authors: H. Sun, Z. Shi, S. Chen, G. Wang, X. Li, Y. Guan, Q. Zhang, Z. Shao,
• Abstract要約: グローバーのアルゴリズムは量子力学の重ね合わせと干渉に依存している。 我々は、HOL Light定理証明器において、Groverのアルゴリズムを正式にモデル化し、検証する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Grover's algorithm relies on the superposition and interference of quantum mechanics, which is more efficient than classical computing in specific tasks such as searching an unsorted database. Due to the high complexity of quantum mechanics, the correctness of quantum algorithms is difficult to guarantee through traditional simulation methods. By contrast, the fundamental concepts and mathematical structure of Grover's algorithm can be formalized into logical expressions and verified by higher-order logical reasoning. In this paper, we formally model and verify Grover's algorithm in the HOL Light theorem prover. We focus on proving key properties such as the unitarity of its oracle and diffusion operators, the monotonicity of the success probability with respect to the number of iterations, and an exact expression for the optimal iteration count. By analyzing a concrete application to integer factorization, we demonstrate the practicality and prospects of our work.
• Abstract（参考訳）: グロバーのアルゴリズムは量子力学の重ね合わせと干渉に依存しており、非分類データベースの探索のような特定のタスクにおいて古典的な計算よりも効率的である。 量子力学の複雑さが高いため、従来のシミュレーション手法によって量子アルゴリズムの正確性を保証することは困難である。 対照的に、グローバーのアルゴリズムの基本概念と数学的構造は論理式に形式化され、高階論理的推論によって検証される。 本稿では,HOL光定理証明器において,Groverのアルゴリズムを形式的にモデル化し,検証する。 オラクルと拡散作用素のユニタリ性、反復数に対する成功確率の単調性、最適反復数に対する正確な表現など、重要な性質の証明に焦点をあてる。 整数分解への具体的な応用を解析することにより、本研究の実用性と展望を実証する。

関連論文リスト

• End-to-End Quantum Algorithm for Topology Optimization in Structural Mechanics [1.6943815984028532]
  位相最適化のためのエンドツーエンドのフォールトトレラント量子アルゴリズムを提案する。 提案した量子ワークフローは、量子アルゴリズムが計算科学と工学の分野をいかに前進させるかを示す。
  論文  参考訳（メタデータ） (2025-10-08T17:42:28Z)
• Efficient Learning for Linear Properties of Bounded-Gate Quantum Circuits [62.46800898243033]
  量子学習理論の最近の進歩は、様々な古典的な入力によって生成された測定データから、大きな量子ビット回路の線形特性を効率的に学習できるのか? 我々は、小さな予測誤差を達成するためには、$d$で線形にスケーリングするサンプルの複雑さが必要であることを証明し、それに対応する計算複雑性は、dで指数関数的にスケールする可能性がある。 そこで本研究では,古典的影と三角展開を利用したカーネルベースの手法を提案し,予測精度と計算オーバーヘッドとのトレードオフを制御可能とした。
  論文  参考訳（メタデータ） (2024-08-22T08:21:28Z)
• Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs [3.444844635251667]
  確率的振る舞いに関する局所的推論のための新しい量子ホア論理を提案する。 論理学における証明規則は意味論的意味論に関して健全であることを示す。 結果として得られる論理フレームワークは、CoqQLRと呼ばれ、古典量子プログラムに関する半自動推論を容易にする。
  論文  参考訳（メタデータ） (2023-08-09T07:23:22Z)
• Opening the Black Box Inside Grover's Algorithm [0.0]
  グロバーのアルゴリズムは、量子コンピュータが古典的コンピュータよりも有利であることを示す主要なアルゴリズムである。 我々は,古典的コンピュータ上で動作可能な量子インスパイアされたアルゴリズムを構築し,Groverのタスクを,オラクルへの(シミュレーションの)呼び出し数で線形に実行する。
  論文  参考訳（メタデータ） (2023-03-20T17:56:20Z)
• General quantum algorithms for Hamiltonian simulation with applications to a non-Abelian lattice gauge theory [44.99833362998488]
  複数の量子数の相関変化からなる相互作用のクラスを効率的にシミュレートできる量子アルゴリズムを導入する。 格子ゲージ理論は、1+1次元のSU(2)ゲージ理論であり、1つのスタッガードフェルミオンに結合する。 これらのアルゴリズムは、アベリアおよび非アベリアゲージ理論と同様に高次元理論にも適用可能であることが示されている。
  論文  参考訳（メタデータ） (2022-12-28T18:56:25Z)
• Automatic and effective discovery of quantum kernels [41.61572387137452]
  量子コンピューティングは、カーネルマシンが量子カーネルを利用してデータ間の類似度を表現できるようにすることで、機械学習モデルを強化することができる。 本稿では,ニューラルアーキテクチャ検索やAutoMLと同じような最適化手法を用いて,この問題に対するアプローチを提案する。 その結果、高エネルギー物理問題に対する我々のアプローチを検証した結果、最良のシナリオでは、手動設計のアプローチに関して、テストの精度を一致または改善できることが示された。
  論文  参考訳（メタデータ） (2022-09-22T16:42:14Z)
• Entanglement and coherence in Bernstein-Vazirani algorithm [58.720142291102135]
  Bernstein-Vaziraniアルゴリズムは、オラクルに符号化されたビット文字列を決定できる。 我々はベルンシュタイン・ヴァジラニアルゴリズムの量子資源を詳細に分析する。 絡み合いがない場合、初期状態における量子コヒーレンス量とアルゴリズムの性能が直接関係していることが示される。
  論文  参考訳（メタデータ） (2022-05-26T20:32:36Z)
• Synthesis of Quantum Circuits with an Island Genetic Algorithm [44.99833362998488]
  特定の演算を行うユニタリ行列が与えられた場合、等価な量子回路を得るのは非自明な作業である。 量子ウォーカーのコイン、トフォリゲート、フレドキンゲートの3つの問題が研究されている。 提案したアルゴリズムは量子回路の分解に効率的であることが証明され、汎用的なアプローチとして、利用可能な計算力によってのみ制限される。
  論文  参考訳（メタデータ） (2021-06-06T13:15:25Z)

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

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