Formal Modeling and Verification of Grover's Algorithm

• URL: http://arxiv.org/abs/2601.02435v1
• Date: Mon, 05 Jan 2026 06:56:21 GMT
• Title: Formal Modeling and Verification of Grover's Algorithm
• Authors: H. Sun, Z. Shi, S. Chen, G. Wang, X. Li, Y. Guan, Q. Zhang, Z. Shao,
• Abstract summary: Grover's algorithm relies on the superposition and interference of quantum mechanics.<n>We formally model and verify Grover's algorithm in the HOL Light theorem prover.
• Score: 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.

Related papers

• Quantum automated theorem proving [15.134110328567838]
  We propose a generic framework for quantum automated theorem proving.<n>We introduce quantum representations of knowledge bases and propose corresponding reasoning algorithms for a variety of tasks.<n>We show how automated reasoning can be achieved with quantum resolution in both propositional and first-order logic.
  arXiv  Detail & Related papers  (2026-01-12T19:39:33Z)
• End-to-End Quantum Algorithm for Topology Optimization in Structural Mechanics [1.6943815984028532]
  We present an end-to-end, fault-tolerant quantum algorithm for topology optimization.<n>The proposed quantum workflow demonstrates how quantum algorithms can advance the field of computational science and engineering.
  arXiv  Detail & Related papers  (2025-10-08T17:42:28Z)
• QCircuitBench: A Large-Scale Dataset for Benchmarking Quantum Algorithm Design [63.02824918725805]
  Quantum computing is recognized for the significant speedup it offers over classical computing through quantum algorithms.<n>QCircuitBench is the first benchmark dataset designed to evaluate AI's capability in designing and implementing quantum algorithms.
  arXiv  Detail & Related papers  (2024-10-10T14:24:30Z)
• Efficient Learning for Linear Properties of Bounded-Gate Quantum Circuits [62.46800898243033]
  Recent progress in quantum learning theory prompts a question: can linear properties of a large-qubit circuit be efficiently learned from measurement data generated by varying classical inputs?<n>We prove that the sample complexity scaling linearly in $d$ is required to achieve a small prediction error, while the corresponding computational complexity may scale exponentially in d.<n>We propose a kernel-based method leveraging classical shadows and truncated trigonometric expansions, enabling a controllable trade-off between prediction accuracy and computational overhead.
  arXiv  Detail & Related papers  (2024-08-22T08:21:28Z)
• Unified framework for efficiently computable quantum circuits [0.0]
  Quantum circuits consisting of Clifford and matchgates are two classes of circuits that are known to be efficiently simulatable on a classical computer. We introduce a unified framework that shows in a transparent way the special structure that allows these circuits can be efficiently simulatable.
  arXiv  Detail & Related papers  (2024-01-16T08:04:28Z)
• Generalized quantum Arimoto-Blahut algorithm and its application to quantum information bottleneck [55.22418739014892]
  We generalize the quantum Arimoto-Blahut algorithm by Ramakrishnan et al. We apply our algorithm to the quantum information bottleneck with three quantum systems. Our numerical analysis shows that our algorithm is better than their algorithm.
  arXiv  Detail & Related papers  (2023-11-19T00:06:11Z)
• Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs [3.444844635251667]
  We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour.<n>We show that the proof rules in the logic are sound with respect to a denotational semantics.<n>The resulting logical framework, called CoqQLR, can facilitate semi-automated reasoning about classical--quantum programs.
  arXiv  Detail & Related papers  (2023-08-09T07:23:22Z)
• Opening the Black Box Inside Grover's Algorithm [0.0]
  Grover's algorithm is a primary algorithm offered as evidence that quantum computers can provide an advantage over classical computers. We construct a quantum-inspired algorithm, executable on a classical computer, that performs Grover's task in a linear number of calls to (simulations of) the oracle.
  arXiv  Detail & Related papers  (2023-03-20T17:56:20Z)
• General quantum algorithms for Hamiltonian simulation with applications to a non-Abelian lattice gauge theory [44.99833362998488]
  We introduce quantum algorithms that can efficiently simulate certain classes of interactions consisting of correlated changes in multiple quantum numbers. The lattice gauge theory studied is the SU(2) gauge theory in 1+1 dimensions coupled to one flavor of staggered fermions. The algorithms are shown to be applicable to higher-dimensional theories as well as to other Abelian and non-Abelian gauge theories.
  arXiv  Detail & Related papers  (2022-12-28T18:56:25Z)
• Exploring the role of parameters in variational quantum algorithms [59.20947681019466]
  We introduce a quantum-control-inspired method for the characterization of variational quantum circuits using the rank of the dynamical Lie algebra. A promising connection is found between the Lie rank, the accuracy of calculated energies, and the requisite depth to attain target states via a given circuit architecture.
  arXiv  Detail & Related papers  (2022-09-28T20:24:53Z)
• Automatic and effective discovery of quantum kernels [41.61572387137452]
  Quantum computing can empower machine learning models by enabling kernel machines to leverage quantum kernels for representing similarity measures between data.<n>We present an approach to this problem, which employs optimization techniques, similar to those used in neural architecture search and AutoML.<n>The results obtained by testing our approach on a high-energy physics problem demonstrate that, in the best-case scenario, we can either match or improve testing accuracy with respect to the manual design approach.
  arXiv  Detail & Related papers  (2022-09-22T16:42:14Z)
• Entanglement and coherence in Bernstein-Vazirani algorithm [58.720142291102135]
  Bernstein-Vazirani algorithm allows one to determine a bit string encoded into an oracle. We analyze in detail the quantum resources in the Bernstein-Vazirani algorithm. We show that in the absence of entanglement, the performance of the algorithm is directly related to the amount of quantum coherence in the initial state.
  arXiv  Detail & Related papers  (2022-05-26T20:32:36Z)
• Synthesis of Quantum Circuits with an Island Genetic Algorithm [44.99833362998488]
  Given a unitary matrix that performs certain operation, obtaining the equivalent quantum circuit is a non-trivial task. Three problems are explored: the coin for the quantum walker, the Toffoli gate and the Fredkin gate. The algorithm proposed proved to be efficient in decomposition of quantum circuits, and as a generic approach, it is limited only by the available computational power.
  arXiv  Detail & Related papers  (2021-06-06T13:15:25Z)
• Quantum-Inspired Algorithms from Randomized Numerical Linear Algebra [53.46106569419296]
  We create classical (non-quantum) dynamic data structures supporting queries for recommender systems and least-squares regression. We argue that the previous quantum-inspired algorithms for these problems are doing leverage or ridge-leverage score sampling in disguise.
  arXiv  Detail & Related papers  (2020-11-09T01:13:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.