Document Open Access Logo

Proving Quantum Programs Correct

Authors Kesha Hietala , Robert Rand , Shih-Han Hung , Liyi Li , Michael Hicks

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.21.pdf
  • Filesize: 0.83 MB
  • 19 pages

Document Identifiers

Author Details

Kesha Hietala
  • University of Maryland, College Park, MD, USA
Robert Rand
  • University of Chicago, IL, USA
Shih-Han Hung
  • University of Maryland, College Park, MD, USA
Liyi Li
  • University of Maryland, College Park, MD, USA
Michael Hicks
  • University of Maryland, College Park, MD, USA

Funding

This material is based upon work supported 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 and the Air Force Office of Scientific Research under Grant No. FA95502110051.

Acknowledgements

We thank Yuxiang Peng for ongoing contributions to the SQIR codebase and pointing out a bug in our original specification for QPE. We thank Xiaodi Wu for discussions about SQIR and follow-on projects.

Cite AsGet BibTex

Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. Proving Quantum Programs Correct. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 21:1-21:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.21

Abstract

As quantum computing progresses steadily from theory into practice, programmers will face 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 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.

Subject Classification

ACM Subject Classification
  • Hardware → Quantum computation
  • Software and its engineering → Formal software verification
Keywords
  • Formal Verification
  • Quantum Computing
  • Proof Engineering

Metrics

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

Related Versions

Supplementary Materials

References

  1. Matt Amy. Formal Methods in Quantum Circuit Design. PhD thesis, University of Waterloo, 2019. Google Scholar
  2. 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
  3. Adriano Barenco, Charles H. Bennett, Richard Cleve, David P. DiVincenzo, Norman Margolus, Peter Shor, Tycho Sleator, John A. Smolin, and Harald Weinfurter. Elementary gates for quantum computation. Phys. Rev. A, 52:3457-3467, November 1995. URL: https://doi.org/10.1103/PhysRevA.52.3457.
  4. Benjamin Bichsel, Maximilian Baader, Timon Gehr, and Martin Vechev. Silq: A high-level quantum language with safe uncomputation and intuitive semantics. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020, 2020. Google Scholar
  5. Jaap Boender, Florian Kammüller, and Rajagopal Nagarajan. Formalization of quantum protocols using coq. In Chris Heunen, Peter Selinger, and Jamie Vicary, editors, Proceedings of the 12th International Workshop on Quantum Physics and Logic, Oxford, U.K., July 15-17, 2015, volume 195 of Electronic Proceedings in Theoretical Computer Science, pages 71-83. Open Publishing Association, 2015. URL: https://doi.org/10.4204/EPTCS.195.6.
  6. Anthony Bordg, Hanna Lachnitt, and Yijun He. Certified quantum computation in Isabelle/HOL. Journal of Automated Reasoning, 2020. URL: https://doi.org/10.1007/s10817-020-09584-7.
  7. Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoit Valiron. Toward certified quantum programming. arXiv e-prints, 2020. URL: http://arxiv.org/abs/2003.05841.
  8. The Coq Development Team. The coq proof assistant, version 8.10.0, 2019. URL: https://doi.org/10.5281/zenodo.3476303.
  9. Andrew W. Cross, Lev S. Bishop, John A. Smolin, and Jay M. Gambetta. Open Quantum Assembly Language. arXiv e-prints, July 2017. URL: http://arxiv.org/abs/1707.03429.
  10. David Deutsch and Richard Jozsa. Rapid solution of problems by quantum computation. Proceedings of the Royal Society of London. Series A: Mathematical and Physical Sciences, 439(1907):553-558, 1992. Google Scholar
  11. Jean-Christophe Filliâtre and Andrei Paskevich. Why3 - where programs meet provers. In Proceedings of the 22nd European Symposium on Programming, Lecture Notes in Computer Science, 2013. Google Scholar
  12. Daniel Gottesman. An introduction to quantum error correction and fault-tolerant quantum computation. In Quantum information science and its contributions to mathematics, Proceedings of Symposia in Applied Mathematics, volume 68, pages 13-58, 2010. Google Scholar
  13. 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
  14. Alexander S Green. Towards a formally verified functional quantum programming language. PhD thesis, University of Nottingham, 2010. Google Scholar
  15. Daniel M. Greenberger, Michael A. Horne, and Anton Zeilinger. Going Beyond Bell’s Theorem, pages 69-72. Springer Netherlands, Dordrecht, 1989. URL: https://doi.org/10.1007/978-94-017-0849-4_10.
  16. Lov K Grover. A fast quantum mechanical algorithm for database search. In Proceedings of the twenty-eighth annual ACM Symposium on Theory of Computing, pages 212-219, 1996. Google Scholar
  17. Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for quantum circuits. Proceedings of the ACM on Programming Languages, 5(37), 2021. Google Scholar
  18. Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Formal verification of quantum algorithms using quantum hoare logic. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part II, pages 187-207, 2019. URL: https://doi.org/10.1007/978-3-030-25543-5_12.
  19. Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. Quantum hoare logic. Archive of Formal Proofs, March 2019. , Formal proof development. URL: http://isa-afp.org/entries/QHLProver.html.
  20. Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, and Naijun Zhan. A theorem prover for quantum hoare logic and its applications. arXiv preprint arXiv:1601.03835, 2016. Google Scholar
  21. Guillaume Melquiond. Interval package for coq, 2020. URL: https://gitlab.inria.fr/coqinterval/interval.
  22. Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2000. Google Scholar
  23. Tobias Nipkow, Markus Wenzel, and Lawrence C. Paulson. Isabelle/HOL: A Proof Assistant for Higher-order Logic. Springer-Verlag, Berlin, Heidelberg, 2002. Google Scholar
  24. Adam Paetznick and Krysta M Svore. Repeat-until-success: non-deterministic decomposition of single-qubit unitaries. Quantum Information & Computation, 14(15-16):1277-1301, 2014. Google Scholar
  25. 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: https://doi.org/10.1145/3009837.3009894.
  26. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, PLDI '88, pages 199-208, New York, NY, USA, 1988. ACM. URL: https://doi.org/10.1145/53990.54010.
  27. Robert Rand. Formally Verified Quantum Programming. PhD thesis, University of Pennsylvania, 2018. Google Scholar
  28. 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: https://doi.org/10.4204/EPTCS.266.8.
  29. Robert Rand, Jennifer Paykin, and Steve Zdancewic. Phantom types for quantum programs. The Fourth International Workshop on Coq for Programming Languages, January 2018. Google Scholar
  30. Peter Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527-586, August 2004. Google Scholar
  31. P. W. Shor. Algorithms for quantum computation: discrete logarithms and factoring. In Proceedings 35th Annual Symposium on Foundations of Computer Science, FOCS '94, 1994. Google Scholar
  32. DR Simon. On the power of quantum computation. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science, pages 116-123, 1994. Google Scholar
  33. 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
  34. Mingsheng Ying. Floyd-hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 33(6):19, 2011. Google Scholar
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 Imprint Privacy Contact