Verified Compilation of Quantum Oracles
- URL: http://arxiv.org/abs/2112.06700v2
- Date: Wed, 20 Apr 2022 13:33:45 GMT
- Title: Verified Compilation of Quantum Oracles
- Authors: Liyi Li, Finn Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu,
Michael Hicks
- Abstract summary: VQO is a high-assurance quantum programming framework.
OQASM is the oracle quantum assembly language.
VQO's versions were on par with or better than (in terms of both qubit and gate counts) oracles produced by Quipper.
- Score: 10.942063551929914
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Quantum algorithms often apply classical operations, such as arithmetic or
predicate checks, over a quantum superposition of classical data; these
so-called oracles are often the largest components of a quantum program. To
ease the construction of efficient, correct oracle functions, this paper
presents VQO, a high-assurance framework implemented with the Coq proof
assistant. The core of VQO is OQASM, the oracle quantum assembly language.
OQASM operations move qubits between two different bases via the quantum
Fourier transform, thus admitting important optimizations, but without inducing
entanglement and the exponential blowup that comes with it. OQASM's design
enabled us to prove correct VQO's compilers -- from a simple imperative
language called OQIMP to OQASM, and from OQASM to SQIR, a general-purpose
quantum assembly language -- and allowed us to efficiently test properties of
OQASM programs using the QuickChick property-based testing framework. We have
used VQO to implement a variety of arithmetic and geometric operators that are
building blocks for important oracles, including those used in Shor's and
Grover's algorithms. We found that VQO's QFT-based arithmetic oracles require
fewer qubits, sometimes substantially fewer, than those constructed using
"classical" gates; VQO's versions of the latter were nevertheless on par with
or better than (in terms of both qubit and gate counts) oracles produced by
Quipper, a state-of-the-art but unverified quantum programming platform.
Related papers
- Quantum Interactive Oracle Proofs [2.0482700732041397]
We introduce the study of quantum Interactive Oracle Proofs (qIOPs)<n>We show two main constructions of qIOPs, both of which are unconditional.<n>We introduce a novel single prover of many-qubits test, which may be of independent interest.
arXiv Detail & Related papers (2026-01-19T09:30:38Z) - 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) - Bayesian Optimization Priors for Efficient Variational Quantum Algorithms [0.0]
Quantum computers currently rely on a quantum-classical approach known as Variational Quantum Algorithms (VQAs) to solve problems.
We propose a hybrid framework for basic computational optimization that reduces the number of shots per time is charged.
Using both proposed features, we show that using both proposed features statistically outperforms an implementation within VQAs for simulations.
arXiv Detail & Related papers (2024-06-20T18:00:12Z) - Quantum Subroutine for Variance Estimation: Algorithmic Design and Applications [80.04533958880862]
Quantum computing sets the foundation for new ways of designing algorithms.
New challenges arise concerning which field quantum speedup can be achieved.
Looking for the design of quantum subroutines that are more efficient than their classical counterpart poses solid pillars to new powerful quantum algorithms.
arXiv Detail & Related papers (2024-02-26T09:32:07Z) - Unifying (Quantum) Statistical and Parametrized (Quantum) Algorithms [65.268245109828]
We take inspiration from Kearns' SQ oracle and Valiant's weak evaluation oracle.
We introduce an extensive yet intuitive framework that yields unconditional lower bounds for learning from evaluation queries.
arXiv Detail & Related papers (2023-10-26T18:23:21Z) - Automatic oracle generation in Microsoft's Quantum Development Kit using
QIR and LLVM passes [1.4902915966744057]
oracle generation techniques can find optimized quantum circuits for classical components in quantum algorithms.
We implement LLVM passes that can automatically generate QIR functions representing classical Q# functions into QIR code implementing such functions quantumly.
arXiv Detail & Related papers (2022-12-04T04:07:05Z) - Succinct Classical Verification of Quantum Computation [30.91621630752802]
We construct a classically succinct interactive argument for quantum computation (BQP)
Our protocol is secure assuming the post-quantum security of indistinguishability obfuscation (iO) and Learning Errors (LWE)
arXiv Detail & Related papers (2022-06-29T22:19:12Z) - 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) - Resource Optimisation of Coherently Controlled Quantum Computations with
the PBS-calculus [55.2480439325792]
Coherent control of quantum computations can be used to improve some quantum protocols and algorithms.
We refine the PBS-calculus, a graphical language for coherent control inspired by quantum optics.
arXiv Detail & Related papers (2022-02-10T18:59:52Z) - Oracle separations of hybrid quantum-classical circuits [68.96380145211093]
Two models of quantum computation: CQ_d and QC_d.
CQ_d captures the scenario of a d-depth quantum computer many times; QC_d is more analogous to measurement-based quantum computation.
We show that, despite the similarities between CQ_d and QC_d, the two models are intrinsically, i.e. CQ_d $nsubseteq$ QC_d and QC_d $nsubseteq$ CQ_d relative to an oracle.
arXiv Detail & Related papers (2022-01-06T03:10:53Z) - Accelerating variational quantum algorithms with multiple quantum
processors [78.36566711543476]
Variational quantum algorithms (VQAs) have the potential of utilizing near-term quantum machines to gain certain computational advantages.
Modern VQAs suffer from cumbersome computational overhead, hampered by the tradition of employing a solitary quantum processor to handle large data.
Here we devise an efficient distributed optimization scheme, called QUDIO, to address this issue.
arXiv Detail & Related papers (2021-06-24T08:18:42Z) - Ansatz-Independent Variational Quantum Classifier [0.0]
We show that variational quantum classifiers (VQCs) fit inside the well-known kernel method.
We also propose a variational circuit realization (VCR) for designing efficient quantum circuits for a given unitary operator.
arXiv Detail & Related papers (2021-02-02T21:25:39Z) - Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow [7.619626059034881]
We propose an efficient scheme for quantum circuit equivalence checking.
The proposed scheme allows to verify even large circuit instances with tens of thousands of operations within seconds or even less.
arXiv Detail & Related papers (2020-09-04T19:58:53Z)
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.