01581nas a2200181 4500008004100000245006200041210006200103260001100165490000600176520106100182100002701243700002301270700001901293700001701312700001801329700001501347856003701362 2023 eng d00aQuantum algorithm for estimating volumes of convex bodies0 aQuantum algorithm for estimating volumes of convex bodies c4/20230 v43 a

Estimating the volume of a convex body is a central problem in convex geometry and can be viewed as a continuous version of counting. We present a quantum algorithm that estimates the volume of an n-dimensional convex body within multiplicative error ε using O~(n3.5+n2.5/ε) queries to a membership oracle and O~(n5.5+n4.5/ε) additional arithmetic operations. For comparison, the best known classical algorithm uses O~(n4+n3/ε2) queries and O~(n6+n5/ε2) additional arithmetic operations. To the best of our knowledge, this is the first quantum speedup for volume estimation. Our algorithm is based on a refined framework for speeding up simulated annealing algorithms that might be of independent interest. This framework applies in the setting of "Chebyshev cooling", where the solution is expressed as a telescoping product of ratios, each having bounded variance. We develop several novel techniques when implementing our framework, including a theory of continuous-space quantum walks with rigorous bounds on discretization error.

1 aChakrabarti, Shouvanik1 aChilds, Andrew, M.1 aHung, Shih-Han1 aLi, Tongyang1 aWang, Chunhao1 aWu, Xiaodi uhttps://arxiv.org/abs/1908.0390301381nas a2200205 4500008004100000245004900041210004700090260001400137520077400151100002000925700001900945700001500964700002400979700001901003700001901022700002301041700001501064700001301079856008301092 2021 eng d00aEasyPQC: Verifying Post-Quantum Cryptography0 aEasyPQC Verifying PostQuantum Cryptography c9/20/20213 a

EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post-quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption.

1 aBarbosa, Manuel1 aBarthe, Gilles1 aFan, Xiong1 aGrégoire, Benjamin1 aHung, Shih-Han1 aKatz, Jonathan1 aStrub, Pierre-Yves1 aWu, Xiaodi1 aZhou, Li uhttps://quics.umd.edu/publications/easypqc-verifying-post-quantum-cryptography01160nas a2200157 4500008004100000245003700041210003700078260001400115520074900129100001900878700001700897700001900914700001300933700001900946856003700965 2021 eng d00aProving Quantum Programs Correct0 aProving Quantum Programs Correct c7/13/20213 a

As quantum computing steadily progresses from theory to practice, programmers are faced with a common problem: How can they be sure that their code does what they intend it to do? This paper presents encouraging results in the application of mechanized proof to the domain of quantum programming in the context of the SQIR development. It verifies the correctness of a range of a quantum algorithms including Simon's algorithm, Grover's algorithm, and quantum phase estimation, a key component of Shor's algorithm. In doing so, it aims to highlight both the successes and challenges of formal verification in the quantum context and motivate the theorem proving community to target quantum computing as an application domain.

1 aHietala, Kesha1 aRand, Robert1 aHung, Shih-Han1 aLi, Liyi1 aHicks, Michael uhttps://arxiv.org/abs/2010.0124001245nas a2200157 4500008004100000245005700041210005600098260001400154300001500168490000800183520080000191100002300991700001901014700001701033856003701050 2021 eng d00aQuantum query complexity with matrix-vector products0 aQuantum query complexity with matrixvector products c3/14/2021 a55:1-55:190 v1983 a

We study quantum algorithms that learn properties of a matrix using queries that return its action on an input vector. We show that for various problems, including computing the trace, determinant, or rank of a matrix or solving a linear system that it specifies, quantum computers do not provide an asymptotic speedup over classical computation. On the other hand, we show that for some problems, such as computing the parities of rows or columns or deciding if there are two identical rows or columns, quantum computers provide exponential speedup. We demonstrate this by showing equivalence between models that provide matrix-vector products, vector-matrix products, and vector-matrix-vector products, whereas the power of these models can vary significantly for classical computation.

1 aChilds, Andrew, M.1 aHung, Shih-Han1 aLi, Tongyang uhttps://arxiv.org/abs/2102.1134901145nas 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.0225001889nas a2200169 4500008004100000245006600041210006500107260001300172300001200185490004400197520136000241100001901601700002301620700002001643700001901663856003701682 2020 eng d00aNon-interactive classical verification of quantum computation0 aNoninteractive classical verification of quantum computation c3/9/2020 a153-1800 vLecture Notes in Computer Science 125523 a

In a recent breakthrough, Mahadev constructed an interactive protocol that enables a purely classical party to delegate any quantum computation to an untrusted quantum prover. In this work, we show that this same task can in fact be performed non-interactively and in zero-knowledge.
Our protocols result from a sequence of significant improvements to the original four-message protocol of Mahadev. We begin by making the first message instance-independent and moving it to an offline setup phase. We then establish a parallel repetition theorem for the resulting three-message protocol, with an asymptotically optimal rate. This, in turn, enables an application of the Fiat-Shamir heuristic, eliminating the second message and giving a non-interactive protocol. Finally, we employ classical non-interactive zero-knowledge (NIZK) arguments and classical fully homomorphic encryption (FHE) to give a zero-knowledge variant of this construction. This yields the first purely classical NIZK argument system for QMA, a quantum analogue of NP.
We establish the security of our protocols under standard assumptions in quantum-secure cryptography. Specifically, our protocols are secure in the Quantum Random Oracle Model, under the assumption that Learning with Errors is quantumly hard. The NIZK construction also requires circuit-private FHE.

1 aAlagic, Gorjan1 aChilds, Andrew, M.1 aGrilo, Alex, B.1 aHung, Shih-Han uhttps://arxiv.org/abs/1911.0810101867nas a2200145 4500008004100000245007000041210006300111260001300174520141800187100001801605700001901623700002701642700001501669856003701684 2020 eng d00aOn the Principles of Differentiable Quantum Programming Languages0 aPrinciples of Differentiable Quantum Programming Languages c4/2/20203 a

Variational Quantum Circuits (VQCs), or the so-called quantum neural-networks, are predicted to be one of the most important near-term quantum applications, not only because of their similar promises as classical neural-networks, but also because of their feasibility on near-term noisy intermediate-size quantum (NISQ) machines. The need for gradient information in the training procedure of VQC applications has stimulated the development of auto-differentiation techniques for quantum circuits. We propose the first formalization of this technique, not only in the context of quantum circuits but also for imperative quantum programs (e.g., with controls), inspired by the success of differentiable programming languages in classical machine learning. In particular, we overcome a few unique difficulties caused by exotic quantum features (such as quantum no-cloning) and provide a rigorous formulation of differentiation applied to bounded-loop imperative quantum programs, its code-transformation rules, as well as a sound logic to reason about their correctness. Moreover, we have implemented our code transformation in OCaml and demonstrated the resource-efficiency of our scheme both analytically and empirically. We also conduct a case study of training a VQC instance with controls, which shows the advantage of our scheme over existing auto-differentiation for quantum circuits without controls.

1 aZhu, Shaopeng1 aHung, Shih-Han1 aChakrabarti, Shouvanik1 aWu, Xiaodi uhttps://arxiv.org/abs/2004.0112200982nas 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.0631901816nas a2200193 4500008004100000245007600041210006900117260001400186300001500200490000600215520125400221100001901475700001901494700001801513700002001531700001901551700001501570856003701585 2018 eng d00aQuantitative Robustness Analysis of Quantum Programs (Extended Version)0 aQuantitative Robustness Analysis of Quantum Programs Extended Ve c2018/12/1 aArticle 310 v33 a

Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called ε-robustness, which characterizes possible "distance" between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF.

1 aHung, Shih-Han1 aHietala, Kesha1 aZhu, Shaopeng1 aYing, Mingsheng1 aHicks, Michael1 aWu, Xiaodi uhttps://arxiv.org/abs/1811.0358501497nas a2200145 4500008004100000245006400041210006400105260001500169490000800184520103000192100001801222700002301240700001901263856006901282 2018 eng d00aQuantum algorithm for multivariate polynomial interpolation0 aQuantum algorithm for multivariate polynomial interpolation c2018/01/170 v4743 a

How many quantum queries are required to determine the coefficients of a degree-d polynomial in n variables? We present and analyze quantum algorithms for this multivariate polynomial interpolation problem over the fields Fq, R, and C. We show that kC and 2kC queries suffice to achieve probability 1 for C and R, respectively, where kC = ⌈ 1 n+1 ( n+d d )⌉ except for d = 2 and four other special cases. For Fq, we show that ⌈ d n+d ( n+d d )⌉ queries suffice to achieve probability approaching 1 for large field order q. The classical query complexity of this problem is ( n+d d ), so our result provides a speedup by a factor of n + 1, n+1 2 , and n+d d for C, R, and Fq, respectively. Thus we find a much larger gap between classical and quantum algorithms than the univariate case, where the speedup is by a factor of 2. For the case of Fq, we conjecture that 2kC queries also suffice to achieve probability approaching 1 for large field order q, although we leave this as an open problem.

1 aChen, Jianxin1 aChilds, Andrew, M.1 aHung, Shih-Han uhttp://rspa.royalsocietypublishing.org/content/474/2209/2017048001532nas a2200193 4500008004100000020002200041022001400063245005900077210005900136260001500195300001600210490000700226520098400233100002301217700001701240700001901257700002601276856003601302 2016 eng d a978-3-95977-013-2 a1868-896900aOptimal quantum algorithm for polynomial interpolation0 aOptimal quantum algorithm for polynomial interpolation c2016/03/01 a16:1--16:130 v553 a

We consider the number of quantum queries required to determine the coefficients of a degree-d polynomial over GF(q). A lower bound shown independently by Kane and Kutin and by Meyer and Pommersheim shows that d/2+1/2 quantum queries are needed to solve this problem with bounded error, whereas an algorithm of Boneh and Zhandry shows that d quantum queries are sufficient. We show that the lower bound is achievable: d/2+1/2 quantum queries suffice to determine the polynomial with bounded error. Furthermore, we show that d/2+1 queries suffice to achieve probability approaching 1 for large q. These upper bounds improve results of Boneh and Zhandry on the insecurity of cryptographic protocols against quantum attacks. We also show that our algorithm's success probability as a function of the number of queries is precisely optimal. Furthermore, the algorithm can be implemented with gate complexity poly(log q) with negligible decrease in the success probability.

1 aChilds, Andrew, M.1 avan Dam, Wim1 aHung, Shih-Han1 aShparlinski, Igor, E. uhttp://arxiv.org/abs/1509.09271