@article {2448, title = {Quantum algorithm for estimating volumes of convex bodies}, journal = {ACM Transactions on Quantum Computing}, volume = {4}, year = {2023}, month = {4/2023}, chapter = {20}, abstract = {

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.

}, url = {https://arxiv.org/abs/1908.03903}, author = {Shouvanik Chakrabarti and Andrew M. Childs and Shih-Han Hung and Tongyang Li and Chunhao Wang and Xiaodi Wu} } @article {2881, title = {EasyPQC: Verifying Post-Quantum Cryptography}, journal = {ACM CCS 2021}, year = {2021}, month = {9/20/2021}, abstract = {

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.

}, doi = {https://dx.doi.org/10.1145/3460120.3484567}, author = {Manuel Barbosa and Gilles Barthe and Xiong Fan and Benjamin Gr{\'e}goire and Shih-Han Hung and Jonathan Katz and Pierre-Yves Strub and Xiaodi Wu and Li Zhou} } @article {2729, title = {Proving Quantum Programs Correct}, journal = {Schloss Dagstuhl}, year = {2021}, month = {7/13/2021}, abstract = {

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\&$\#$39;s algorithm, Grover\&$\#$39;s algorithm, and quantum phase estimation, a key component of Shor\&$\#$39;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.

}, doi = {https://doi.org/10.4230/LIPIcs.ITP.2021.21}, url = {https://arxiv.org/abs/2010.01240}, author = {Kesha Hietala and Robert Rand and Shih-Han Hung and Liyi Li and Michael Hicks} } @article {2886, title = {Quantum query complexity with matrix-vector products}, journal = {Proceedings of the 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), Leibniz International Proceedings in Informatics}, volume = {198}, year = {2021}, month = {3/14/2021}, pages = {55:1-55:19}, abstract = {

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.

}, doi = {https://arxiv.org/ct?url=https\%3A\%2F\%2Fdx.doi.org\%2F10.4230\%2FLIPIcs.ICALP.2021.55\&v=2de93347}, url = {https://arxiv.org/abs/2102.11349}, author = {Andrew M. Childs and Shih-Han Hung and Tongyang Li} } @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 {2485, title = {Non-interactive classical verification of quantum computation}, journal = {Theory of Cryptography Conference (TCC)}, volume = {Lecture Notes in Computer Science 12552}, year = {2020}, month = {3/9/2020}, pages = {153-180}, abstract = {

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.

}, url = {https://arxiv.org/abs/1911.08101}, author = {Gorjan Alagic and Andrew M. Childs and Alex B. Grilo and Shih-Han Hung} } @article {2558, title = {On the Principles of Differentiable Quantum Programming Languages}, year = {2020}, month = {4/2/2020}, abstract = {

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.

}, doi = {https://doi.org/10.1145/3385412.3386011}, url = {https://arxiv.org/abs/2004.01122}, author = {Shaopeng Zhu and Shih-Han Hung and Shouvanik Chakrabarti and Xiaodi Wu} } @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 {2306, title = {Quantitative Robustness Analysis of Quantum Programs (Extended Version)}, journal = {Proc. ACM Program. Lang.}, volume = {3}, year = {2018}, month = {2018/12/1}, pages = {Article 31}, abstract = {

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.

}, doi = {https://doi.org/10.1145/3290344}, url = {https://arxiv.org/abs/1811.03585}, author = {Shih-Han Hung and Kesha Hietala and Shaopeng Zhu and Mingsheng Ying and Michael Hicks and Xiaodi Wu} } @article {1922, title = {Quantum algorithm for multivariate polynomial interpolation}, journal = {Proceedings of The Royal Society A}, volume = {474}, year = {2018}, month = {2018/01/17}, abstract = {

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.

}, doi = {10.1098/rspa.2017.0480}, url = {http://rspa.royalsocietypublishing.org/content/474/2209/20170480}, author = {Jianxin Chen and Andrew M. Childs and Shih-Han Hung} } @article {1554, title = {Optimal quantum algorithm for polynomial interpolation}, journal = {43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)}, volume = {55}, year = {2016}, month = {2016/03/01}, pages = {16:1--16:13}, abstract = {

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\&$\#$39;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.

}, isbn = {978-3-95977-013-2}, issn = {1868-8969}, doi = {http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.16}, url = {http://arxiv.org/abs/1509.09271}, author = {Andrew M. Childs and Wim van Dam and Shih-Han Hung and Igor E. Shparlinski} }