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.
The Grover search algorithm is one of the two key algorithms in the field of quantum computing, and hence it is of significant interest to describe it in the most efficient mathematical formalism. We show firstly, that Clifford's formalism of geometric algebra, provides a significantly more efficient representation than the conventional Bra-ket notation, and secondly, that the basis defined by the states of maximum and minimum weight in the Grover search space, allows a simple visualization of the Grover search as the precession of a spin-1/2 particle. Using this formalism we efficiently solve…
It has been shown in recent years that quantum information has a topological nature (\cite{AC}, \cite{Co}, \cite{Co2}). In \cite{V}, Vicary undergoes the study of quantum algorithms using this new topological approach. The advantage of this new formalism is that it allows new proofs of correctness of the algorithms such as Deutsch-Jozsa, hidden subgroup and single-shot Grover algorithms. It also provide more clear insight to the generalizations of these algorithms. In this paper, we consider (multi-step) Grover algorithm from this new perspective.
Symbolic Analysis of Grover Search Algorithm via Chain-of-Thought Reasoning and Quantum-Native Tokenization
Department of Computer Science, The University of Pittsburgh（匹兹堡大学计算机科学系）；Department of Computer Science, The University of North Carolina at Chapel Hill（北卡罗来纳大学教堂山分校计算机科学系）
Grover's search algorithm was originally proposed for circuit-based quantum computers. A crucial part of it is to query an oracle -- a black-box unitary operation. Generation of this oracle is formally beyond the original algorithm design. Here, we propose a realization of Grover's oracle for a large class of searching problems using a quantum annealing step. The time of this step grows only logarithmically with the size of the database. This suggests an efficient path to application of Grover's algorithm to practically important problems, such as finding the ground state of a Hamiltonian with…
In this article, we discuss the implementation of a quantum recommendation system that uses a quantum variant of the k-nearest neighbours algorithm and the Grover algorithm to search for a specific element in unstructured database. In addition to the presentation of the recommendation system as an algorithm, the article also shows a main steps in construction of a suitable quantum circuit for realisation of a given recommendation system. The computational complexity of individual calculation steps during recommendation system was also indicated. The verification correctness of a proposed recom…
Multi-dimensional quantum walks usually require large coin spaces. Here we show that the non-localized case of the spatial density probability of the two-dimensional Grover walk can be obtained using only a two-dimensional coin space and a quantum walk in alternate directions. We present a formal proof of this correspondence and analyze the behavior of the coin-position entanglement as well as the x-y spatial entanglement in our scheme with respect to the Grover one. We show that our experimentally simpler scheme allows to entangle the two orthogonal directions of the walk more efficiently.
A proof-of-concept application of a quantum algorithm to multiloop Feynman integrals in the Loop-Tree Duality (LTD) framework is applied to a representative four-loop topology. Bootstrapping causality in the LTD formalism, is a suitable problem to address with quantum computers given the straightforward possibility to encode the two on-shell states of a propagator on the two states of a qubit. A modification of Grover's quantum search algorithm is developed and the quantum algorithm is successfully implemented on IBM Quantum and QUTE simulators.
We propose the physical implementation of a Grover-like search problem by means of Frenkel exciton trapping at a shallow isotopic impurity against a background of competing mechanisms. The search culminating at the impurity molecule, designated the "winner" site, is marked by its enhanced interaction with acoustic phonons at low temperatures. The quantum search proceeds with the assistance of an Oracle-like exciton-phonon interaction which addresses only the impurity site, via the Dyson propagator within the Green's function formalism. The optimum parameters of a graph lattice with long-range …
The search for "a quantum needle in a quantum haystack" is a metaphor for the problem of finding out which one of a permissible set of unitary mappings---the oracles---is implemented by a given black box. Grover's algorithm solves this problem with quadratic speed-up as compared with the analogous search for "a classical needle in a classical haystack." Since the outcome of Grover's algorithm is probabilistic---it gives the correct answer with high probability, not with certainty---the answer requires verification. For this purpose we introduce specific test states, one for each oracle. These …
We present a space-efficient implementation of the quantum verification of matrix products (QVMP) algorithm and demonstrate its functionality by running it on the Aer simulator with two simulation methods: statevector and matrix product state (MPS). We report circuit metrics (gate count, qubit count, circuit depth), transpilation time, simulation time, and a proof of Grover oracle correctness. Our study concludes that while QVMP can be simulated on moderately sized inputs, it cannot scale to a degree where we can observe any quantum advantage on current quantum hardware due to circuit depth an…
It is well known that Grover's algorithm asymptotically transforms an equal superposition state into an eigenstate (of a given basis). Here, we demonstrate a verification algorithm based on weak measurement which can achieve the same purpose even if the qubit is not in an equal superposition state. The proposed algorithm highlights the distinguishability between any arbitrary single qubit superposition state and an eigenstate. We apply this algorithm to propose the scheme of a Quantum Locker, a protocol in which any legitimate party can verify his/her authenticity by using a newly developed qu…
This paper presents a new formal method for verification of quantum communication protocols. By extending the symbolic system of Petri nets, we can define quantum pure states in Petri-net settings. Therefore, it is possible to emerge a framework from formalizing basic quantum phenomena, which are utilized to achieve communication tasks. We also present an example of applying this framework to the modeling and analyzing quantum communication protocols to show how it works.
This paper is a gentle but rigorous introduction to quantum computing intended for discrete mathematicians. Starting from a small set of assumptions on the behavior of quantum computing devices, we analyze their main characteristics, stressing the differences with classical computers, and finally describe two well-known algorithms (Simon's algorithm and Grover's algorithm) using the formalism developed in previous sections. This paper does not touch on the physics of the devices, and therefore does not require any notion of quantum mechanics. Numerical examples on an implementation of Grover's…
We propose to analyse quantum protocols by applying formal verification techniques developed in classical computing for the analysis of communicating concurrent systems. One area of successful application of these techniques is that of classical security protocols, exemplified by Lowe's discovery and fix of a flaw in the well-known Needham-Schroeder authentication protocol. Secure quantum cryptographic protocols are also notoriously difficult to design. Quantum cryptography is therefore an interesting target for formal verification, and provides our first example; we expect the approach to be …
