Formal Verification vs. Quantum Uncertainty
Quantum programming is hard: Quantum programs are necessarily probabilistic and impossible to examine without disrupting the execution of a program. In response to this challenge, we and a number of other researchers have written tools to verify quantum programs against their intended semantics. This is not enough. Verifying an idealized semantics against a real world quantum program doesn't allow you to confidently predict the program’s output. In order to have verification that works, you need both an error semantics related to the hardware at hand (this is necessarily low level) and certified compilation to the that same hardware. Once we have these two things, we can talk about an approach to quantum programming where we start by writing and verifying programs at a high level, attempt to verify properties of the compiled code, and repeat as necessary.
Formal Verification
Quantum Computing
Programming Languages
Quantum Error Correction
Certified Compilation
NISQ
Software and its engineering~Formal software verification
Hardware~Quantum error correction and fault tolerance
Hardware~Circuit optimization
12:1-12:11
Regular Paper
All authors are funded by the U.S. Department of Energy, Office of Science, Office of Advanced Scientific Computing Research, Quantum Testbed Pathfinder Program under Award Number DE-SC0019040.
We would like to acknowledge our co-authors on work reviewed here, including Jennifer Paykin, Dong-Ho Lee, Steve Zdancewic, Shih-Han Hung, Shaopeng Zhu, Xiaodi Wu, and Mingsheng Ying. We also thank the anonymous referees for their helpful feedback.
Robert
Rand
Robert Rand
University of Maryland, College Park, USA
http://www.cs.umd.edu/~rrand/
https://orcid.org/0000-0001-6842-5505
Also partly funded by a Victor Basili Postdoctoral Fellowship.
Kesha
Hietala
Kesha Hietala
University of Maryland, College Park, USA
https://www.cs.umd.edu/people/khietala
https://orcid.org/0000-0002-2724-0974
Michael
Hicks
Michael Hicks
University of Maryland, College Park, USA
http://www.cs.umd.edu/~mwh/
https://orcid.org/0000-0002-2759-9223
10.4230/LIPIcs.SNAPL.2019.12
Matthew Amy. Towards Large-scale Functional Verification of Universal Quantum Circuits. In Proceedings of the 15th International Conference on Quantum Physics and Logic, QPL 2018, June 2018.
Matthew Amy, Dmitri Maslov, and Michele Mosca. Polynomial-Time T-Depth Optimization of Clifford+T Circuits Via Matroid Partitioning. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 33, 2013.
Matthew Amy, Martin Roetteler, and Krysta M. Svore. Verified compilation of space-efficient reversible circuits. In Proceedings of the 28th International Conference on Computer Aided Verification (CAV 2017). Springer, July 2017. URL: https://www.microsoft.com/en-us/research/publication/verified-compilation-of-space-efficient-reversible-circuits/.
https://www.microsoft.com/en-us/research/publication/verified-compilation-of-space-efficient-reversible-circuits/
Miriam Backens. The ZX-calculus is complete for stabilizer quantum mechanics. New Journal of Physics, 16(9):093021, 2014.
P Oscar Boykin and Vwani Roychowdhury. Optimal encryption of quantum bits. Physical review A, 67(4):042317, 2003.
Michael Carbin, Sasa Misailovic, and Martin C. Rinard. Verifying Quantitative Reliability for Programs That Execute on Unreliable Hardware. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, pages 33-52, 2013. URL: http://dx.doi.org/10.1145/2509136.2509546.
http://dx.doi.org/10.1145/2509136.2509546
Andrew M. Childs, Dmitri Maslov, Yunseong Nam, Neil J. Ross, and Yuan Su. Toward the first quantum simulation with quantum speedup. Proceedings of the National Academy of Sciences of the United States of America, 115 38:9456-9461, 2018.
Richard Cleve, Artur Ekert, Chiara Macchiavello, and Michele Mosca. Quantum algorithms revisited. In Proceedings of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, volume 454, pages 339-354. The Royal Society, 1998.
Bob Coecke and Ross Duncan. Interacting quantum observables. In International Colloquium on Automata, Languages, and Programming, pages 298-310. Springer, 2008.
Don Coppersmith. An Approximate Fourier Transform Useful in Quantum Factoring. arXiv preprint, 1994. URL: http://arxiv.org/abs/quant-ph/0201067.
http://arxiv.org/abs/quant-ph/0201067
David Deutsch. Quantum theory, the Church-Turing principle and the universal quantum computer. In Proceedings of the Royal Society of London A: Mathematical, Physical and Engineering Sciences, volume 400, pages 97-117. The Royal Society, 1985.
Edsger Wybe Dijkstra. A Discipline of Programming, volume 1. Prentice-Hall, 1976.
Andrew Fagan and Ross Duncan. Optimising Clifford Circuits with Quantomatic. In Proceedings of the 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Nova Scotia, 3-7 June 2018, 2018.
Alexander Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. Quipper: A Scalable Quantum Programming Language. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2013, pages 333-342, 2013.
Lov K. Grover. A Fast Quantum Mechanical Algorithm for Database Search. In Proceedings of the Twenty-eighth Annual ACM Symposium on Theory of Computing, STOC '96, pages 212-219, New York, NY, USA, 1996. ACM. URL: http://dx.doi.org/10.1145/237814.237866.
http://dx.doi.org/10.1145/237814.237866
Luke Heyfron and Earl T. Campbell. An Efficient Quantum Compiler that reduces T count. Quantum Science and Technology, 4, 2017.
Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. Verified Optimization in a Quantum Intermediate Representation. arXiv e-prints, page arXiv:1904.06319, April 2019. URL: http://arxiv.org/abs/1904.06319.
http://arxiv.org/abs/1904.06319
Yipeng Huang and Margaret Martonosi. QDB: from quantum algorithms towards correct quantum programs. arXiv preprint, 2018. URL: http://arxiv.org/abs/1811.05447.
http://arxiv.org/abs/1811.05447
Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. Quantitative Robustness Analysis of Quantum Programs. Proc. ACM Program. Lang., 3(POPL):31:1-31:29, January 2019. URL: http://dx.doi.org/10.1145/3290344.
http://dx.doi.org/10.1145/3290344
IBM. IBM quantum experience, 2017. URL: https://quantumexperience.ng.bluemix.net/qx/devices.
https://quantumexperience.ng.bluemix.net/qx/devices
Ali Javadi-Abhari, Arvin Faruque, Mohammad J Dousti, Lukas Svec, Oana Catu, Amlan Chakrabati, Chen-Fu Chiang, Seth Vanderwilt, John Black, and Fred Chong. Scaffold: Quantum programming language. Technical report, PRINCETON UNIV NJ DEPT OF COMPUTER SCIENCE, 2012.
Aleks Kissinger. Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing. PhD thesis, University of Oxford, 2011.
Xavier Leroy et al. The CompCert verified compiler. Development available at http://compcert. inria. fr, 2009, 2004.
Sam McArdle, Xiao Yuan, and Simon Benjamin. Error mitigated digital quantum simulation. arXiv preprint, 2018. URL: http://arxiv.org/abs/1807.02467.
http://arxiv.org/abs/1807.02467
Prakash Murali, Jonathan M Baker, Ali Javadi Abhari, Frederic T Chong, and Margaret Martonosi. Noise-Adaptive Compiler Mappings for Noisy Intermediate-Scale Quantum Computers. arXiv preprint, 2019. URL: http://arxiv.org/abs/1901.11054.
http://arxiv.org/abs/1901.11054
Yunseong Nam, Neil J Ross, Yuan Su, Andrew M Childs, and Dmitri Maslov. Automated optimization of large quantum circuits with continuous parameters. npj Quantum Information, 4(1):23, 2018.
Jennifer Paykin, Robert Rand, and Steve Zdancewic. QWIRE: A core language for quantum circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 846-858, New York, NY, USA, 2017. ACM. URL: http://dx.doi.org/10.1145/3009837.3009894.
http://dx.doi.org/10.1145/3009837.3009894
John Preskill. Quantum Computing in the NISQ era and beyond. Quantum, 2:79, August 2018. URL: http://dx.doi.org/10.22331/q-2018-08-06-79.
http://dx.doi.org/10.22331/q-2018-08-06-79
Robert Rand. Formally Verified Quantum Programming. PhD thesis, University of Pennsylvania, 2018.
Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic. ReQWIRE: Reasoning about Reversible Quantum Circuits. In Proceedings of the 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Nova Scotia, 3-7 June 2018, 2018.
Robert Rand, Jennifer Paykin, and Steve Zdancewic. QWIRE practice: Formal verification of quantum circuits in Coq. In Proceedings 14th International Conference on Quantum Physics and Logic, QPL 2017, Nijmegen, The Netherlands, 3-7 July 2017., pages 119-132, 2017. URL: http://dx.doi.org/10.4204/EPTCS.266.8.
http://dx.doi.org/10.4204/EPTCS.266.8
Markus Reiher, Nathan Wiebe, Krysta Marie Svore, Dave Wecker, and Matthias Troyer. Elucidating reaction mechanisms on quantum computers. Proceedings of the National Academy of Sciences of the United States of America, 114 29:7555-7560, 2017.
Neil J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, 2015.
Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzotto. From Symmetric Pattern-Matching to Quantum Control. In International Conference on Foundations of Software Science and Computation Structures, pages 348-364. Springer, 2018.
Peter Selinger and Benoît Valiron. Quantum lambda calculus. In Simon Gay and Ian Mackie, editors, Semantic Techniques in Quantum Computation, pages 135-172. Cambridge University Press, 2009.
Krysta Svore, Alan Geller, Matthias Troyer, John Azariah, Christopher Granade, Bettina Heim, Vadym Kliuchnikov, Mariia Mykhailova, Andres Paz, and Martin Roetteler. Q#: Enabling scalable quantum computing and development with a high-level DSL. In Proceedings of the Real World Domain Specific Languages Workshop 2018, page 7. ACM, 2018.
Swamit S. Tannu and Moinuddin K. Qureshi. A Case for Variability-Aware Policies for NISQ-Era Quantum Computers. arXiv e-prints, page arXiv:1805.10224, May 2018. URL: http://arxiv.org/abs/1805.10224.
http://arxiv.org/abs/1805.10224
Dominique Unruh. Quantum Hoare Logic with Ghost Variables. arXiv preprint, 2019. URL: http://arxiv.org/abs/1902.00325.
http://arxiv.org/abs/1902.00325
Dominique Unruh. Quantum Relational Hoare Logic. Proc. ACM Program. Lang., 3(POPL):33:1-33:31, January 2019. URL: http://dx.doi.org/10.1145/3290346.
http://dx.doi.org/10.1145/3290346
Mingsheng Ying. Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 33(6):19, 2011.
Alwin Zulehner, Alexandru Paler, and Robert Wille. Efficient mapping of quantum circuits to the IBM QX architectures. In 2018 Design, Automation & Test in Europe Conference & Exhibition, DATE 2018, Dresden, Germany, March 19-23, 2018, pages 1135-1138, 2018. URL: http://dx.doi.org/10.23919/DATE.2018.8342181.
http://dx.doi.org/10.23919/DATE.2018.8342181
Robert Rand, Kesha Hietala, and Michael Hicks
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode