Quantum Advantage for All

TL;DR

This paper demonstrates that classical algorithms' complexity bounds can be translated into quantum resource requirements, enabling symbolic execution on quantum computers with potential quadratic speedup, bridging classical and quantum computing.

Contribution

It introduces a method to encode classical algorithm execution into quantum models, allowing symbolic execution on quantum hardware with resource bounds related to classical complexity.

Findings

Quantum bits required are bounded by classical time and space complexity.

Quantum models can execute symbolic code with potential quadratic speedup.

Feasibility of using quantum annealers and gate-model quantum computers for symbolic execution.

Abstract

We show that the algorithmic complexity of any classical algorithm written in a Turing-complete programming language polynomially bounds the number of quantum bits that are required to run and even symbolically execute the algorithm on a quantum computer. In particular, we show that any classical algorithm $A$ that runs in $\mathcal{O}(f(n))$ time and $\mathcal{O}(g(n))$ space requires no more than $\mathcal{O}(f(n)\cdot g(n))$ quantum bits to execute, even symbolically, on a quantum computer. With $\mathcal{O}(1)\leq\mathcal{O}(g(n))\leq\mathcal{O}(f(n))$ for all $n$, the quantum bits required to execute $A$ may therefore not exceed $\mathcal{O}(f(n)^2)$ and may come down to $\mathcal{O}(f(n))$ if memory consumption by $A$ is bounded by a constant. Our construction works by encoding symbolic execution of machine code in a finite state machine over the satisfiability-modulo-theory (SMT) of bitvectors, for modeling CPU registers, and arrays of bitvectors, for modeling main memory. The FSM is linear in the size of the code, independent of execution time and space, and represents the reachable machine states for any given input. The FSM may be explored by bounded model checkers using SMT and SAT solvers as backend. However, for the purpose of this paper, we focus on quantum computing by unrolling and bit-blasting the FSM into (1)~satisfiability-preserving quadratic unconstrained binary optimization (QUBO) models targeting adiabatic forms of quantum computing such as quantum annealing, and (2)~semantics-preserving quantum circuits (QCs) targeting gate-model quantum computers. With our compact QUBOs, real quantum annealers can now execute simple but real code even symbolically, yet only with potential but no guarantee for exponential speedup, and with our QCs as oracles, Grover's algorithm applies to symbolic execution of arbitrary code, guaranteeing at least in theory a quadratic speedup.