@article {3363, title = {Verifiable measurement-based quantum random sampling with trapped ions}, year = {2023}, month = {7/26/2023}, abstract = {

Quantum computers are now on the brink of outperforming their classical counterparts. One way to demonstrate the advantage of quantum computation is through quantum random sampling performed on quantum computing devices. However, existing tools for verifying that a quantum device indeed performed the classically intractable sampling task are either impractical or not scalable to the quantum advantage regime. The verification problem thus remains an outstanding challenge. Here, we experimentally demonstrate efficiently verifiable quantum random sampling in the measurement-based model of quantum computation on a trapped-ion quantum processor. We create random cluster states, which are at the heart of measurement-based computing, up to a size of 4 x 4 qubits. Moreover, by exploiting the structure of these states, we are able to recycle qubits during the computation to sample from entangled cluster states that are larger than the qubit register. We then efficiently estimate the fidelity to verify the prepared states--in single instances and on average--and compare our results to cross-entropy benchmarking. Finally, we study the effect of experimental noise on the certificates. Our results and techniques provide a feasible path toward a verified demonstration of a quantum advantage.

}, doi = {https://doi.org/10.48550/arXiv.2307.14424}, url = {https://arxiv.org/abs/2307.14424}, author = {Martin Ringbauer and Marcel Hinsche and Thomas Feldker and Paul K. Faehrmann and Juani Bermejo-Vega and Claire Edmunds and Lukas Postler and Roman Stricker and Christian D. Marciniak and Michael Meth and Ivan Pogorelov and Rainer Blatt and Philipp Schindler and Jens Eisert and Thomas Monz and Dominik Hangleiter} } @article {2912, title = {Verified Compilation of Quantum Oracles}, year = {2021}, month = {12/13/2021}, 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 algorithm. 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 among three different bases via the Quantum Fourier Transform and Hadamard operations, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM\&$\#$39;s design enabled us to prove correct VQO\&$\#$39;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 oracles used in Shor\&$\#$39;s and Grover\&$\#$39;s algorithms, as well as several common arithmetic operators. VQO\&$\#$39;s oracles have performance comparable to those produced by Quipper, a state-of-the-art but unverified quantum programming platform.

}, url = {https://arxiv.org/abs/2112.06700}, author = {Liyi Li and Finnegan Voichick and Kesha Hietala and Yuxiang Peng and Xiaodi Wu and Michael Hicks} } @article {2491, title = {A Verified Optimizer for Quantum Circuits}, journal = {Proceedings of the ACM on Programming Languages}, volume = {5}, year = {2021}, month = {11/12/2020}, abstract = {

We present VOQC, the first fully verified compiler for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. We evaluate VOQC\&$\#$39;s verified optimizations on a series of benchmarks, and it performs comparably to industrial-strength compilers. VOQC\&$\#$39;s optimizations reduce total gate counts on average by 17.7\% on a benchmark of 29 circuit programs compared to a 10.7\% reduction when using IBM\&$\#$39;s Qiskit compiler.

}, doi = {https://doi.org/10.1145/3434318}, url = {https://arxiv.org/abs/1912.02250}, author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks} } @article {2208, title = {Validating and Certifying Stabilizer States}, journal = {Phys. Rev. A }, volume = {99}, year = {2019}, month = {9/16/2019}, abstract = {

We propose a measurement scheme that validates the preparation of a target n-qubit stabilizer state. The scheme involves a measurement of n Pauli observables, a priori determined from the target stabilizer and which can be realized using single-qubit gates. Based on the proposed validation scheme, we derive an explicit expression for the worse-case fidelity, i.e., the minimum fidelity between the target stabilizer state and any other state consistent with the measured data. We also show that the worse-case fidelity can be certified, with high probability, using O(n) copies of the state of the system per measured observable.

}, doi = {https://doi.org/10.1103/PhysRevA.99.042337}, url = {https://arxiv.org/abs/1808.10786}, author = {Amir Kalev and Anastasios Kyrillidis} } @article {2416, title = {Variational Quantum Computation of Excited States}, journal = {Quantum }, volume = {3}, year = {2019}, month = {06/28/2019}, abstract = {

The calculation of excited state energies of electronic structure Hamiltonians has many important applications, such as the calculation of optical spectra and reaction rates. While low-depth quantum algorithms, such as the variational quantum eigenvalue solver (VQE), have been used to determine ground state energies, methods for calculating excited states currently involve the implementation of high-depth controlled-unitaries or a large number of additional samples. Here we show how overlap estimation can be used to deflate eigenstates once they are found, enabling the calculation of excited state energies and their degeneracies. We propose an implementation that requires the same number of qubits as VQE and at most twice the circuit depth. Our method is robust to control errors, is compatible with error-mitigation strategies and can be implemented on near-term quantum compute

}, doi = {https://doi.org/10.22331/q-2019-07-01-156}, url = {https://arxiv.org/abs/1805.08138}, author = {Oscar Higgott and Daochen Wang and Stephen Brierley} } @article {2384, title = {Verification Logics for Quantum Programs}, year = {2019}, type = {Originally submitted in March 2016 as a qualifying examination (WPE-II) for the PhD program at the University of Pennsylvania}, abstract = {

We survey the landscape of Hoare logics for quantum programs. We review three papers: \"Reasoning about imperative quantum programs\" by Chadha, Mateus and Sernadas; \"A logic for formal verification of quantum programs\" by Yoshihiko Kakutani; and \"Floyd-hoare logic for quantum programs\" by Mingsheng Ying. We compare the mathematical foundations of the logics, their underlying languages, and the expressivity of their assertions. We also use the languages to verify the Deutsch-Jozsa Algorithm, and discuss their relative usability in practice.

}, url = {https://arxiv.org/abs/1904.04304}, author = {Robert Rand} } @article {2404, title = {Verified Optimization in a Quantum Intermediate Representation}, year = {2019}, month = {04/12/2019}, abstract = {

We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing {\textquoteleft}quantum assembly\&$\#$39; languages and simplifying the verification process. We demonstrate the power of sqire as an intermediate representation of quantum programs by verifying a number of useful optimizations, and we demonstrate sqire\&$\#$39;s use as a tool for general verification by proving several quantum programs correct.

}, url = {https://arxiv.org/abs/1904.06319}, author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Xiaodi Wu and Michael Hicks} } @article {2252, title = {Verified Quantum Information Scrambling}, year = {2018}, abstract = {

Quantum scrambling is the dispersal of local information into many-body quantum entanglements and correlations distributed throughout the entire system. This concept underlies the dynamics of thermalization in closed quantum systems, and more recently has emerged as a powerful tool for characterizing chaos in black holes. However, the direct experimental measurement of quantum scrambling is difficult, owing to the exponential complexity of ergodic many-body entangled states. One way to characterize quantum scrambling is to measure an out-of-time-ordered correlation function (OTOC); however, since scrambling leads to their decay, OTOCs do not generally discriminate between quantum scrambling and ordinary decoherence. Here, we implement a quantum circuit that provides a positive test for the scrambling features of a given unitary process. This approach conditionally teleports a quantum state through the circuit, providing an unambiguous litmus test for scrambling while projecting potential circuit errors into an ancillary observable. We engineer quantum scrambling processes through a tunable 3-qubit unitary operation as part of a 7-qubit circuit on an ion trap quantum computer. Measured teleportation fidelities are typically \∼80\%, and enable us to experimentally bound the scrambling-induced decay of the corresponding OTOC measurement.

}, url = {https://arxiv.org/abs/1806.02807}, author = {Kevin A. Landsman and Caroline Figgatt and Thomas Schuster and Norbert M. Linke and Beni Yoshida and Norman Y. Yao and Christopher Monroe} } @article {1816, title = {Valley Blockade in a Silicon Double Quantum Dot}, journal = {Physical Review B}, volume = {96}, year = {2017}, month = {2017/11/13}, pages = {205302}, abstract = {

Electrical transport in double quantum dots (DQDs) illuminates many interesting features of the dots\&$\#$39; carrier states. Recent advances in silicon quantum information technologies have renewed interest in the valley states of electrons confined in silicon. Here we show measurements of DC transport through a mesa-etched silicon double quantum dot. Comparing bias triangles (i.e., regions of allowed current in DQDs) at positive and negative bias voltages we find a systematic asymmetry in the size of the bias triangles at the two bias polarities. Asymmetries of this nature are associated with blocking of tunneling events due to the occupation of a metastable state. Several features of our data lead us to conclude that the states involved are not simple spin states. Rather, we develop a model based on selective filling of valley states in the DQD that is consistent with all of the qualitative features of our data.

}, doi = {10.1103/PhysRevB.96.205302}, url = {https://arxiv.org/abs/1607.06107}, author = {Justin K. Perron and Michael Gullans and J. M. Taylor and M. D. Stewart, Jr. and Neil M. Zimmerman} } @article {1317, title = {Von Neumann{\textquoteright}s {\textquoteright}No Hidden Variables{\textquoteright} Proof: A Re-Appraisal}, journal = {Foundations of Physics}, volume = {40}, year = {2010}, month = {2010/6/11}, pages = {1333 - 1340}, abstract = { Since the analysis by John Bell in 1965, the consensus in the literature is that von Neumann{\textquoteright}s {\textquoteright}no hidden variables{\textquoteright} proof fails to exclude any significant class of hidden variables. Bell raised the question whether it could be shown that any hidden variable theory would have to be nonlocal, and in this sense {\textquoteright}like Bohm{\textquoteright}s theory.{\textquoteright} His seminal result provides a positive answer to the question. I argue that Bell{\textquoteright}s analysis misconstrues von Neumann{\textquoteright}s argument. What von Neumann proved was the impossibility of recovering the quantum probabilities from a hidden variable theory of dispersion free (deterministic) states in which the quantum observables are represented as the {\textquoteright}beables{\textquoteright} of the theory, to use Bell{\textquoteright}s term. That is, the quantum probabilities could not reflect the distribution of pre-measurement values of beables, but would have to be derived in some other way, e.g., as in Bohm{\textquoteright}s theory, where the probabilities are an artefact of a dynamical process that is not in fact a measurement of any beable of the system. }, doi = {10.1007/s10701-010-9480-9}, url = {http://arxiv.org/abs/1006.0499v1}, author = {Jeffrey Bub} }