The simulation of quantum programs by classical computers is a critical endeavor for several reasons: it provides proof-of-concept validation of quantum algorithms; it provides opportunities to experiment with new programming abstractions suitable for the quantum domain; and most significantly it is a way to explore the elusive boundary at which a quantum advantage may materialize. Here, we show that traditional techniques of symbolic evaluation and partial evaluation yield surprisingly efficient classical simulations for some instances of textbook quantum algorithms that include the Deutsch, Deutsch-Jozsa, Bernstein-Vazirani, Simon, Grover, and Shor's algorithms. The success of traditional partial evaluation techniques in this domain is due to one simple insight: the quantum bits used in these algorithms can be modeled by a symbolic boolean variable while still keeping track of the correlations due to superposition and entanglement. More precisely, the system of constraints generated over the symbolic variables contains all the necessary quantum correlations and hence the answer to the quantum algorithms. With a few programming tricks explained in the paper, quantum circuits with millions of gates can be symbolically executed in seconds. Paradoxically, other circuits with as few as a dozen gates take exponential time. We reflect on the significance of these results in the conclusion.
The simulation of quantum programs by classical computers is a critical endeavor for several reasons: it provides proof-of-concept validation of quantum algorithms; it provides opportunities to experiment with new programming abstractions suitable for the quantum domain; and most significantly it is a way to explore the elusive boundary at which a quantum advantage may materialize. Here, we show that traditional techniques of symbolic evaluation and partial evaluation yield surprisingly efficient classical simulations for some instances of textbook quantum algorithms that include the Deutsch, Deutsch-Jozsa, Bernstein-Vazirani, Simon, Grover, and Shor's algorithms. The success of traditional partial evaluation techniques in this domain is due to one simple insight: the quantum bits used in these algorithms can be modeled by a symbolic boolean variable while still keeping track of the correlations due to superposition and entanglement. More precisely, the system of constraints generated over the symbolic variables contains all the necessary quantum correlations and hence the answer to the quantum algorithms. With a few programming tricks explained in the paper, quantum circuits with millions of gates can be symbolically executed in seconds. Paradoxically, other circuits with as few as a dozen gates take exponential time. We reflect on the significance of these results in the conclusion.
Quantum models of computation are widely believed to be more powerful than classical ones. Efforts center on proving that, for a given problem, quantum algorithms are more resource efficient than any classical one. All this, however, assumes a standard predictive paradigm of reasoning where, given initial conditions, the future holds the answer. How about bringing information from the future to the present and exploit it to one's advantage? This is a radical new approach for reasoning, so-called Retrodictive Computation, that benefits from the specific form of the computed functions. We demonstrate how to use tools of symbolic computation to realize retrodictive quantum computing at scale and exploit it to efficiently, and classically, solve instances of the quantum Deutsch-Jozsa, Bernstein-Vazirani, Simon, Grover, and Shor's algorithms.
Quantum circuit simulation is the basic tool for reasoning over quantum programs. Despite the tremendous advance in the simulator technology in the recent years, the performance of simulators is still unsatisfactory on non-trivial circuits, which slows down the development of new quantum systems. In this work, we develop a loop summarizing simulator based on multi-terminal binary decision diagrams (MTBDDs) with efficiently customized quantum gate operations. The simulator is capable of automatic loop summarization using symbolic execution, which saves repetitive computation for circuits with iterative structures. Experimental results show the simulator outperforms state-of-the-art simulators on some standard circuits, such as Grover's algorithm, by several orders of magnitude.
Abstract Quantum evolution is time-reversible and yet little advantage is gained from this in the circuit model of quantum computing. Indeed, most quantum algorithms expressed in the circuit model compute strictly from the present to the future, preparing initial states and proceeding forward with unitary transformations and measurements. We may call this predictive computation. In contrast, retrodictive quantum theory, retrocausality, and the time-symmetry of physical laws all suggest that quantum computation embodies richer --untapped-- modes of computation, which could exploit knowledge about the future for a computational advantage. We demonstrate that by using symbolic partial evaluation, retrodictive reasoning can indeed be used as a computational resource that exhibits richer modes of computation at the boundary of the classical/quantum divide. Specifically, instead of fully specifying the initial conditions of a quantum circuit and computing forward, it is possible to compute, classically, in both the forward and backward directions starting from partially-specified initial and final conditions. Furthermore, this mixed mode of computation (i) can solve problems with fewer resources than the conventional forward mode of execution, sometimes even purely classically (de-quantization), (ii) can be expressed in a symbolic representation that immediately exposes global relational properties of the wavefunction that are needed for quantum algorithms and (iii) reveals that the entanglement patterns inherent in genuine quantum algorithms with no known classical counterparts are artifacts of the chosen symbolic representation.
These notes begin in Chapter 1 with a review of linear algebra and the postulates of quantum mechanics, leading to an explanation of single- and multi-qubit gates. Chapter 2 explores the challenge of constructing arbitrary quantum states from given initial states, and introduces circuits for building oracles. Chapter 3 presents foundational algorithms such as entanglement creation, quantum teleportation, Deutsch-Jozsa, Bernstein-Vazirani, and Simon's algorithm. Chapters 4 and 5 cover algorithms based on the quantum Fourier transform, including phase estimation, period finding, factoring, and logarithm computation. These chapters also include complexity analysis and detailed quantum circuits suitable for implementation in code. Chapter 6 introduces Grover's algorithm for quantum search and amplitude amplification, including its realization via Hamiltonian simulation and a method for derandomization. Chapter 7 discusses basic techniques for Hamiltonian simulation, such as Lie-Trotter decomposition, sparse Hamiltonians, and the linear combination of unitaries. It also provides example circuits for simulating Hamiltonians expressed as linear combinations of Pauli operators. Chapter 8 introduces variational quantum algorithms, and Chapter 9 presents an algorithm for simulating fermionic many-particle systems, with an emphasis on molecular Hamiltonians. It also outlines the key transformations needed to map a molecular Hamiltonian to a form suitable for simulation on a quantum computer.
With the rapid development of quantum computing, automatic verification of quantum circuits becomes more and more important. While several decision diagrams (DDs) have been introduced in quantum circuit simulation and verification, none of them supports symbolic computation. Algorithmic manipulations of symbolic objects, however, have been identified as crucial, if not indispensable, for several verification tasks. This paper proposes the first decision-diagram approach for operating symbolic objects and verifying quantum circuits with symbolic terms. As a notable example, our symbolic tensor decision diagrams (symbolic TDD) could verify the functionality of the 160-qubit quantum Fourier transform circuit within three minutes. Moreover, as demonstrated on Bernstein-Vazirani algorithm, Grover's algorithm, and the bit-flip error correction code, the symbolic TDD enables efficient verification of quantum circuits with user-supplied oracles and/or classical controls.
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 O(f(n)) time and O(g(n)) space requires no more than O(f(n)⋅g(n)) quantum bits to execute, even symbolically, on a quantum computer. With O(1)≤O(g(n))≤O(f(n)) for all n, the quantum bits required to execute A may therefore not exceed O(f(n)2) and may come down to 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.