Document Open Access Logo

Formal Verification vs. Quantum Uncertainty

Authors Robert Rand , Kesha Hietala , Michael Hicks

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2019.12.pdf
  • Filesize: 1.11 MB
  • 11 pages

Document Identifiers

Author Details

Robert Rand
  • University of Maryland, College Park, USA
Kesha Hietala
  • University of Maryland, College Park, USA
Michael Hicks
  • University of Maryland, College Park, USA

Funding

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.
  • Rand, Robert: Also partly funded by a Victor Basili Postdoctoral Fellowship.

Acknowledgements

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.

Cite As Get BibTex

Robert Rand, Kesha Hietala, and Michael Hicks. Formal Verification vs. Quantum Uncertainty. In 3rd Summit on Advances in Programming Languages (SNAPL 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 136, pp. 12:1-12:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.SNAPL.2019.12

Abstract

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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
  • Hardware → Quantum error correction and fault tolerance
  • Hardware → Circuit optimization
Keywords
  • Formal Verification
  • Quantum Computing
  • Programming Languages
  • Quantum Error Correction
  • Certified Compilation
  • NISQ

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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. Google Scholar
  2. 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. Google Scholar
  3. 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/.
  4. Miriam Backens. The ZX-calculus is complete for stabilizer quantum mechanics. New Journal of Physics, 16(9):093021, 2014. Google Scholar
  5. P Oscar Boykin and Vwani Roychowdhury. Optimal encryption of quantum bits. Physical review A, 67(4):042317, 2003. Google Scholar
  6. 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.
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. Bob Coecke and Ross Duncan. Interacting quantum observables. In International Colloquium on Automata, Languages, and Programming, pages 298-310. Springer, 2008. Google Scholar
  10. Don Coppersmith. An Approximate Fourier Transform Useful in Quantum Factoring. arXiv preprint, 1994. URL: http://arxiv.org/abs/quant-ph/0201067.
  11. 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. Google Scholar
  12. Edsger Wybe Dijkstra. A Discipline of Programming, volume 1. Prentice-Hall, 1976. Google Scholar
  13. 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. Google Scholar
  14. 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. Google Scholar
  15. 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.
  16. Luke Heyfron and Earl T. Campbell. An Efficient Quantum Compiler that reduces T count. Quantum Science and Technology, 4, 2017. Google Scholar
  17. 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.
  18. Yipeng Huang and Margaret Martonosi. QDB: from quantum algorithms towards correct quantum programs. arXiv preprint, 2018. URL: http://arxiv.org/abs/1811.05447.
  19. 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.
  20. IBM. IBM quantum experience, 2017. URL: https://quantumexperience.ng.bluemix.net/qx/devices.
  21. 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. Google Scholar
  22. Aleks Kissinger. Pictures of Processes: Automated Graph Rewriting for Monoidal Categories and Applications to Quantum Computing. PhD thesis, University of Oxford, 2011. Google Scholar
  23. Xavier Leroy et al. The CompCert verified compiler. Development available at http://compcert. inria. fr, 2009, 2004. Google Scholar
  24. Sam McArdle, Xiao Yuan, and Simon Benjamin. Error mitigated digital quantum simulation. arXiv preprint, 2018. URL: http://arxiv.org/abs/1807.02467.
  25. 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.
  26. 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. Google Scholar
  27. 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.
  28. 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.
  29. Robert Rand. Formally Verified Quantum Programming. PhD thesis, University of Pennsylvania, 2018. Google Scholar
  30. 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. Google Scholar
  31. 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.
  32. 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. Google Scholar
  33. Neil J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, 2015. Google Scholar
  34. 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. Google Scholar
  35. 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. Google Scholar
  36. 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. Google Scholar
  37. 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.
  38. Dominique Unruh. Quantum Hoare Logic with Ghost Variables. arXiv preprint, 2019. URL: http://arxiv.org/abs/1902.00325.
  39. 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.
  40. Mingsheng Ying. Floyd-Hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 33(6):19, 2011. Google Scholar
  41. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact