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.

%8 04/12/2019 %G eng %U https://arxiv.org/abs/1904.06319 %0 Journal Article %J Proc. ACM Program. Lang. %D 2018 %T Quantitative Robustness Analysis of Quantum Programs (Extended Version) %A Shih-Han Hung %A Kesha Hietala %A Shaopeng Zhu %A Mingsheng Ying %A Michael Hicks %A Xiaodi Wu %XQuantum 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.

%B Proc. ACM Program. Lang. %V 3 %P Article 31 %8 2018/12/1 %G eng %U https://arxiv.org/abs/1811.03585 %N POPL %R https://doi.org/10.1145/3290344 %0 Journal Article %J Proceedings of The Royal Society A %D 2018 %T Quantum algorithm for multivariate polynomial interpolation %A Jianxin Chen %A Andrew M. Childs %A Shih-Han Hung %XHow 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.

%B Proceedings of The Royal Society A %V 474 %8 2018/01/17 %G eng %U http://rspa.royalsocietypublishing.org/content/474/2209/20170480 %N 2209 %R 10.1098/rspa.2017.0480 %0 Journal Article %J 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016) %D 2016 %T Optimal quantum algorithm for polynomial interpolation %A Andrew M. Childs %A Wim van Dam %A Shih-Han Hung %A Igor E. Shparlinski %XWe 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.

%B 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016) %V 55 %P 16:1--16:13 %8 2016/03/01 %@ 978-3-95977-013-2 %G eng %U http://arxiv.org/abs/1509.09271 %R http://dx.doi.org/10.4230/LIPIcs.ICALP.2016.16