02171nas a2200289 4500008004100000245007500041210006900116260001400185520131000199100002201509700002001531700002001551700002401571700002401595700002001619700001901639700002001658700002901678700001801707700002001725700001801745700002301763700001701786700001701803700002401820856003701844 2023 eng d00aVerifiable measurement-based quantum random sampling with trapped ions0 aVerifiable measurementbased quantum random sampling with trapped c7/26/20233 a

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.

1 aRingbauer, Martin1 aHinsche, Marcel1 aFeldker, Thomas1 aFaehrmann, Paul, K.1 aBermejo-Vega, Juani1 aEdmunds, Claire1 aPostler, Lukas1 aStricker, Roman1 aMarciniak, Christian, D.1 aMeth, Michael1 aPogorelov, Ivan1 aBlatt, Rainer1 aSchindler, Philipp1 aEisert, Jens1 aMonz, Thomas1 aHangleiter, Dominik uhttps://arxiv.org/abs/2307.1442401742nas a2200169 4500008004100000245004400041210004400085260001500129520128400144100001301428700002301441700001901464700001801483700001501501700001901516856003701535 2021 eng d00aVerified Compilation of Quantum Oracles0 aVerified Compilation of Quantum Oracles c12/13/20213 a

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'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 oracles used in Shor's and Grover's algorithms, as well as several common arithmetic operators. VQO's oracles have performance comparable to those produced by Quipper, a state-of-the-art but unverified quantum programming platform.

1 aLi, Liyi1 aVoichick, Finnegan1 aHietala, Kesha1 aPeng, Yuxiang1 aWu, Xiaodi1 aHicks, Michael uhttps://arxiv.org/abs/2112.0670001145nas a2200169 4500008004100000245004600041210004400087260001500131490000600146520069700152100001900849700001700868700001900885700001500904700001900919856003700938 2021 eng d00aA Verified Optimizer for Quantum Circuits0 aVerified Optimizer for Quantum Circuits c11/12/20200 v53 a

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's verified optimizations on a series of benchmarks, and it performs comparably to industrial-strength compilers. VOQC'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's Qiskit compiler.

1 aHietala, Kesha1 aRand, Robert1 aHung, Shih-Han1 aWu, Xiaodi1 aHicks, Michael uhttps://arxiv.org/abs/1912.0225001015nas a2200133 4500008004100000245004800041210004800089260001400137490000700151520064300158100001600801700002700817856003700844 2019 eng d00aValidating and Certifying Stabilizer States0 aValidating and Certifying Stabilizer States c9/16/20190 v993 a

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.

1 aKalev, Amir1 aKyrillidis, Anastasios uhttps://arxiv.org/abs/1808.1078601313nas a2200145 4500008004100000245005400041210005400095260001500149490000600164520090100170100001901071700001801090700002201108856003701130 2019 eng d00aVariational Quantum Computation of Excited States0 aVariational Quantum Computation of Excited States c06/28/20190 v33 a

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

1 aHiggott, Oscar1 aWang, Daochen1 aBrierley, Stephen uhttps://arxiv.org/abs/1805.0813800869nas a2200097 4500008004100000245004500041210004500086520058600131100001700717856003700734 2019 eng d00aVerification Logics for Quantum Programs0 aVerification Logics for Quantum Programs3 a

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.

1 aRand, Robert uhttps://arxiv.org/abs/1904.0430400982nas a2200157 4500008004100000245006700041210006700108260001500175520050800190100001900698700001700717700001900734700001500753700001900768856003700787 2019 eng d00aVerified Optimization in a Quantum Intermediate Representation0 aVerified Optimization in a Quantum Intermediate Representation c04/12/20193 a

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 `quantum assembly' 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's use as a tool for general verification by proving several quantum programs correct.

1 aHietala, Kesha1 aRand, Robert1 aHung, Shih-Han1 aWu, Xiaodi1 aHicks, Michael uhttps://arxiv.org/abs/1904.0631901858nas a2200169 4500008004100000245004400041210004400085520137000129100002401499700002201523700002101545700002301566700001801589700002001607700002401627856003701651 2018 eng d00aVerified Quantum Information Scrambling0 aVerified Quantum Information Scrambling3 a

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.

1 aLandsman, Kevin, A.1 aFiggatt, Caroline1 aSchuster, Thomas1 aLinke, Norbert, M.1 aYoshida, Beni1 aYao, Norman, Y.1 aMonroe, Christopher uhttps://arxiv.org/abs/1806.0280701580nas a2200181 4500008004100000245005200041210005200093260001500145300001100160490000700171520107600178100002301254700002101277700001901298700002001317700002401337856003701361 2017 eng d00aValley Blockade in a Silicon Double Quantum Dot0 aValley Blockade in a Silicon Double Quantum Dot c2017/11/13 a2053020 v963 a

Electrical transport in double quantum dots (DQDs) illuminates many interesting features of the dots' 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.

1 aPerron, Justin, K.1 aGullans, Michael1 aTaylor, J., M.1 aStewart, M., D.1 aZimmerman, Neil, M. uhttps://arxiv.org/abs/1607.0610701422nas a2200133 4500008004100000245006200041210005700103260001400160300001600174490000700190520103700197100001701234856003701251 2010 eng d00aVon Neumann's 'No Hidden Variables' Proof: A Re-Appraisal0 aVon Neumanns No Hidden Variables Proof A ReAppraisal c2010/6/11 a1333 - 13400 v403 a Since the analysis by John Bell in 1965, the consensus in the literature is that von Neumann's 'no hidden variables' 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 'like Bohm's theory.' His seminal result provides a positive answer to the question. I argue that Bell's analysis misconstrues von Neumann'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 'beables' of the theory, to use Bell'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'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. 1 aBub, Jeffrey uhttp://arxiv.org/abs/1006.0499v1