An automated deductive verification framework for circuit-building quantum programs. (English) Zbl 1473.68106
Yoshida, Nobuko (ed.), Programming languages and systems. 30th European symposium on programming, ESOP 2021, held as part of the European joint conferences on theory and practice of software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 12648, 148-177 (2021).
Summary: While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor’s integer factoring, quantum phase estimation (QPE) and Grover’s search.
For the entire collection see [Zbl 1471.68023].
For the entire collection see [Zbl 1471.68023].
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q12 | Quantum algorithms and complexity in the theory of computing |
| 81P68 | Quantum computation |
References:
| [1] | M. Amy. Formal Methods in Quantum Circuit Design. PhD thesis, University of Waterloo, Ontario, Canada, 2019. |
| [2] | M. Amy. Towards large-scale functional verification of universal quantum circuits. In P. Selinger and G. Chiribella, editors, Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 1-21, Halifax, Canada, 2019. EPTCS. · Zbl 1483.81038 |
| [3] | M. Amy, M. Roetteler, and K. M. Svore. Verified compilation of space-efficient reversible circuits. In R. Majumdar and V. Kuncak, editors, Proceedings of the 29th International Conference on Computer Aided Verification (CAV 2017), Part II, volume 10427 of Lecture Notes in Computer Science, pages 3-21, Heidelberg, Germany, 2017. Springer. · Zbl 1494.68045 |
| [4] | F. Arute, K. Arya, R. Babbush, D. Bacon, J. C. Bardin, R. Barends, R. Biswas, S. Boixo, F. G. S. L. Brandao, D. A. Buell, et al. Quantum supremacy using a programmable superconducting processor. Nature, 574(7779):505-510, 2019. |
| [5] | S. Beauregard. Circuit for shor’s algorithm using 2n+ 3 qubits. arXiv preprint quant-ph/0205095, 2002. · Zbl 1152.81676 |
| [6] | D. Bhattacharjee, M. Soeken, S. Dutta, A. Chattopadhyay, and G. D. Micheli. Reversible pebble games for reducing qubits in hierarchical quantum circuit synthesis. In Proceedings of the 49th IEEE International Symposium on Multiple-Valued Logic (ISMVL 2019), pages 102-107, Fredericton, NB, Canada, 2019. IEEE. |
| [7] | J. Biamonte, P. Wittek, N. Pancotti, P. Rebentrost, N. Wiebe, and S. Lloyd. Quantum machine learning. Nature, 549(7671):195, 2017. |
| [8] | B. Bichsel, M. Baader, T. Gehr, and M. T. Vechev. Silq: a high-level quantum language with safe uncomputation and intuitive semantics. In A. F. Donaldson and E. Torlak, editors, Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2020, London, UK, June 15-20, 2020, pages 286-300. ACM, 2020. |
| [9] | F. Bobot, J.-C. Filliâtre, C. Marché, and A. Paskevich. Why3: Shepherd Your Herd of Provers. In Proceedings of Boogie 2011: First International Workshop on Intermediate Verification Languages, Wroclaw, Poland, 53-64, 2011. Available online as hal-00790310. |
| [10] | J. Boender, F. Kammüller, and R. Nagarajan. Formalization of quantum protocols using coq. In C. Heunen, P. Selinger, and J. Vicary, editors, Proceedings of the 12th International Workshop on Quantum Physics and Logic (QPL 2015), volume 195 of Electronic Proceedings in Theoretical Computer Science, pages 71-83, Oxford, UK, 2015. EPTCS. · Zbl 1477.68528 |
| [11] | A. Broadbent. How to verify a quantum computation. Theory of Computing, 14(1):1-37, 2018. · Zbl 1395.68142 |
| [12] | T. Carette, D. Horsman, and S. Perdrix. SZX-calculus: Scalable graphical quantum reasoning. In P. Rossmanith, P. Heggernes, and J. Katoen, editors, 44th International Symposium on Mathematical Foundations of Computer Science, MFCS 2019, August 26-30, 2019, Aachen, Germany, volume 138 of LIPIcs, pages 55:1-55:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. |
| [13] | C. Chareton, S. Bardin, F. Bobot, V. Perrelle, and B. Valiron. Toward certified quantum programming. arXiv preprint arXiv:2003.05841, 2020. · Zbl 1473.68106 |
| [14] | I. L. Chuang, N. Gershenfeld, and M. Kubinec. Experimental implementation of fast quantum searching. Physical review letters, 80(15):3408, 1998. |
| [15] | E. M. Clarke and J. M. Wing. Formal methods: State of the art and future directions. ACM Computing Surveys (CSUR), 28(4):626-643, 1996. |
| [16] | R. Cleve, A. Ekert, C. Macchiavello, and M. Mosca. Quantum algorithms revisited. Proceedings of the Royal Society of London. Series A: Mathematical, Physical and Engineering Sciences, 454(1969):339-354, 1998. · Zbl 0915.68050 |
| [17] | B. Coecke and A. Kissinger. Picturing quantum processes. Cambridge University Press, Cambridge, United Kingdom, 2017. · Zbl 1405.81001 |
| [18] | D. Coppersmith. An approximate fourier transform useful in quantum factoring. arXiv preprint quant-ph/0201067, 1994. |
| [19] | T. A. Davidson. Formal verification techniques using quantum process calculus. PhD thesis, University of Warwick, 2012. |
| [20] | N. de Beaudrap, R. Duncan, D. Horsman, and S. Perdrix. Pauli fusion: a computational model to realise quantum transformations from ZX terms. Available online as arXiv:1904.12817, 2019. |
| [21] | A. Fagan and R. Duncan. Optimising Clifford circuits with Quantomatic. In P. Selinger and G. Chiribella, editors, Proceedings of the 15th International Conference on Quantum Physics and Logic (QPL 2018), volume 287 of Electronic Notes In Theoretical Computer Science, pages 85-105, Halifax, Canada, 2018. EPTCS. · Zbl 1486.81014 |
| [22] | E. Farhi, J. Goldstone, and S. Gutmann. A quantum approximate optimization algorithm. Available online as arXiv:1411.4028, 2014. · Zbl 1213.68284 |
| [23] | E. Farhi, J. Goldstone, S. Gutmann, J. Lapan, A. Lundgren, and D. Preda. A quantum adiabatic evolution algorithm applied to random instances of an np-complete problem. Science, 292(5516):472-475, 2001. · Zbl 1226.81046 |
| [24] | J. Filliâtre and C. Marché. The Why/Krakatoa/Caduceus platform for deductive program verification. In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007), volume 4590 of Lecture Notes in Computer Science, pages 173-177, Berlin, Germany, 2007. Springer. |
| [25] | J. Filliâtre and A. Paskevich. Why3 - where programs meet provers. In M. Felleisen and P. Gardner, editors, Proceedings of the 22nd European Symposium on Programming Languages and Systems (ESOP 2013), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2013), volume 7792 of Lecture Notes in Computer Science, pages 125-128, Rome, Italy, 2013. Springer. · Zbl 1435.68366 |
| [26] | J.-C. Filliâtre, L. Gondelman, and A. Paskevich. The spirit of ghost code. Formal Methods in System Design, 48(3):152-174, 2016. · Zbl 1358.68070 |
| [27] | S. J. Gay, R. Nagarajan, and N. Papanikolaou. QMC: a model checker for quantum systems. In A. Gupta and S. Malik, editors, Proceeding of the 20th International Conference on Computer Aided Verification (CAV 2008), volume 5123 of Lecture Notes in Computer Science, pages 543-547, Princeton, NJ, USA, 2008. Springer. |
| [28] | I. M. Georgescu, S. Ashhab, and F. Nori. Quantum simulation. Reviews of Modern Physics, 86(1):153, 2014. |
| [29] | A. Gheorghiu, T. Kapourniotis, and E. Kashefi. Verification of quantum computation: An overview of existing approaches. Theory of Computing Systems, 63(4):715-808, 2019. · Zbl 1423.68281 |
| [30] | A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, and B. Valiron. Quipper: A scalable quantum programming language. In H.-J. Boehm and C. Flanagan, editors, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI’13), pages 333-342, Seattle, WA, USA, 2013. ACM. · Zbl 1406.68013 |
| [31] | L. K. Grover. A fast quantum mechanical algorithm for database search. In G. L. Miller, editor, Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing (STOC), pages 212-219, Philadelphia, Pennsylvania, USA, 1996. ACM. · Zbl 0922.68044 |
| [32] | W. Haaswijk, M. Soeken, A. Mishchenko, and G. De Micheli. SAT-based exact synthesis: Encodings, topology families, and parallelism. To apprear in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, https://doi,org/10.1109/TCAD.2019.2897703, 2019. |
| [33] | A. W. Harrow, A. Hassidim, and S. Lloyd. Quantum algorithm for linear systems of equations. Physical Review Letters, 103:150502, Oct 2009. |
| [34] | K. Hietala, R. Rand, S.-H. Hung, L. Li, and M. Hicks. Proving quantum programs correct. arXiv preprint arXiv:2010.01240, 2020. |
| [35] | K. Hietala, R. Rand, S.-H. Hung, X. Wu, and M. Hicks. A verified optimizer for quantum circuits. Proceedings of the ACM on Programming Languages, 5(POPL):1-29, 2021. |
| [36] | Y. Huang and M. Martonosi. QDB: from quantum algorithms towards correct quantum programs. In T. Barik, J. Sunshine, and S. Chasins, editors, Proceedings of the 9th Workshop on Evaluation and Usability of Programming Languages and Tools (PLATEAU@SPLASH 2018), volume 67 of OpenAccess Series in Informatics (OASIcs), pages 4:1-4:14, Boston, Massachusetts, USA, 2018. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. |
| [37] | Y. Huang and M. Martonosi. Statistical assertions for validating patterns and finding bugs in quantum programs. In S. B. Manne, H. C. Hunter, and E. R. Altman, editors, Proceedings of the 46th International Symposium on Computer Architecture (ISCA 2019), pages 541-553, Phoenix, AZ, USA, 2019. ACM. |
| [38] | IBM Blog. On quantum supremacy. Blog Article (https://www.ibm.com/blogs/research/2019/10/on-quantum-supremacy/), 2019. |
| [39] | A. Kissinger and J. van de Wetering. Reducing t-count with the ZX-calculus. Available online as arXiv:1903.10477, 2019. |
| [40] | A. Kissinger and V. Zamdzhiev. Quantomatic: A proof assistant for diagrammatic reasoning. In A. P. Felty and A. Middeldorp, editors, Proceedings for the 25th International Conference on Automated Deduction (CADE-25), volume 9195 of Lecture Notes in Computer Science, pages 326-336, Berlin, Germany, 2015. Springer. · Zbl 1465.68288 |
| [41] | A. Y. Kitaev. Quantum measurements and the abelian stabilizer problem. Available online as arXiv:quant-ph/9511026, 1995. |
| [42] | E. Knill. Conventions for quantum pseudocode. Technical report, Los Alamos National Lab., NM (United States), 1996. |
| [43] | U. D. Lago, A. Masini, and M. Zorzi. Quantum implicit computational complexity. Theoretical Computer Science, 411(2):377-409, 2010. · Zbl 1186.68209 |
| [44] | G. Li, L. Zhou, N. Yu, Y. Ding, M. Ying, and Y. Xie. Projection-based runtime assertions for testing and debugging quantum programs. Proc. ACM Program. Lang., 4(OOPSLA):150:1-150:29, 2020. |
| [45] | J. Liu, B. Zhan, S. Wang, S. Ying, T. Liu, Y. Li, M. Ying, and N. Zhan. Formal verification of quantum algorithms using quantum hoare logic. In I. Dillig and S. Tasiran, editors, Computer Aided Verification, pages 187-207, Cham, 2019. Springer International Publishing. · Zbl 1533.68169 |
| [46] | T. Liu, Y. Li, S. Wang, M. Ying, and N. Zhan. A theorem prover for quantum hoare logic and its applications. Available as arXiv:1601.03835, 2016. |
| [47] | U. Mahadev. Classical verification of quantum computations. In M. Thorup, editor, Proceedings of the 59th IEEE Annual Symposium on Foundations of Computer Science (FOCS 2018), pages 259-267, Paris, France, 2018. IEEE Computer Society. |
| [48] | G. Meuli, M. Soeken, M. Roetteler, and T. Häner. Enabling accuracy-aware quantum compilers using symbolic resource estimation. Proc. ACM Program. Lang., 4(OOPSLA), 2020. |
| [49] | R. Nagarajan and S. Gay. Formal verification of quantum protocols. Available online as arXiv:quant-ph/0203086, 2002. |
| [50] | M. A. Nielsen and I. Chuang. Quantum computation and quantum information. Cambridge University Press, Cambridge, United Kingdom, 2002. · Zbl 1049.81015 |
| [51] | L. Paolini, M. Piccolo, and M. Zorzi. qPCF: Higher-order languages and quantum circuits. Journal of Automated Reasoning, 63(4):941-966, Dec 2019. · Zbl 1468.68049 |
| [52] | A. Parent, M. Roetteler, and K. M. Svore. REVS: a tool for space-optimized reversible circuit synthesis. In I. Phillips and H. Rahaman, editors, Proceedings of the 9th International Conference on Reversible Computation (RC 2017), volume 10301 of Lecture Notes in Computer Science, pages 90-101, Kolkata, India, 2017. Springer. · Zbl 1487.68108 |
| [53] | J. Paykin, R. Rand, and S. Zdancewic. QWIRE: a core language for quantum circuits. In G. Castagna and A. D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL’17), pages 846-858, Paris, France, 2017. ACM. · Zbl 1380.68087 |
| [54] | Qbricks repository. https://cchareton.github.io/Qbricks. |
| [55] | Quantum Computing Report. List of tools. Available online (https://quantumcomputingreport.com/resources/tools/), 2019. |
| [56] | R. Rand. Formally Verified Quantum Programming. PhD thesis, University of Pennsylvania, 2018. |
| [57] | R. Rand, J. Paykin, D. Lee, and S. Zdancewic. ReQWIRE: Reasoning about reversible quantum circuits. In P. Selinger and G. Chiribella, editors, Proceedings 15th International Conference on Quantum Physics and Logic (QPL 2018), volume 287 of Electronic Proceedings in Theoretical Computer Science, pages 299-312, Halifax, Canada, 2018. EPTCS. · Zbl 1486.81064 |
| [58] | R. Rand, J. Paykin, and S. Zdancewic. QWIRE practice: Formal verification of quantum circuits in coq. In B. Coecke and A. Kissinger, editors, Proceedings 14th International Conference on Quantum Physics and Logic (QPL 2017), volume 266 of Electronic Proceedings in Theoretical Computer Science, pages 119-132, Nijmegen, The Netherlands, 2017. EPTCS. · Zbl 1380.68087 |
| [59] | N. J. Ross. Algebraic and Logical Methods in Quantum Computation. PhD thesis, Dalhousie University, 2015. |
| [60] | P. Selinger and B. Valiron. A lambda calculus for quantum computation with classical control. Mathematical Structures in Computer Science, 16:527-552, 2006. · Zbl 1122.68033 |
| [61] | P. W. Shor. Algorithms for quantum computation: Discrete log and factoring. In Proceedings of the 35th Annual Symposium on Foundations of Computer Science (FOCS’94), pages 124-134, Santa Fe, New Mexico, US., 1994. IEEE, IEEE Computer Society Press. |
| [62] | M. Soeken, T. Häner, and M. Roetteler. Programming quantum computers using design automation. Available online as arXiv:1803.01022, 2018. |
| [63] | D. S. Steiger, T. Häner, and M. Troyer. ProjectQ: an open source software framework for quantum computing. Quantum, 2:49, Jan. 2018. |
| [64] | K. M. Svore, A. Geller, M. Troyer, J. Azariah, C. Granade, B. Heim, V. Kliuchnikov, M. Mykhailova, A. Paz, and M. Roetteler. Q#: Enabling scalable quantum computing and development with a high-level domain-specific language. Available online as arXiv:1803.00652, 2018. |
| [65] | K. M. Svore and M. Troyer. The quantum future of computation. IEEE Computer, 49(9):21-030, 2016. |
| [66] | B. Valiron, N. J. Ross, P. Selinger, D. S. Alexander, and J. M. Smith. Programming the quantum future. Communications of the ACM, 58(8):52-61, 2015. |
| [67] | D. Wecker and K. M. Svore. LIQUi \(|\rangle \): A software design architecture and domain-specific language for quantum computing. Available online as arXiv:1402.4467, 2014. |
| [68] | M. Ying. Floyd-hoare logic for quantum programs. ACM Transactions on Programming Languages and Systems (TOPLAS), 33(6):19:1-19:49, 2011. |
| [69] | M. Ying. Toward automatic verification of quantum programs. Formal Aspects of Computing, 31(1):3-25, 2019. · Zbl 1425.68271 |
| [70] | M. Ying, Y. Li, N. Yu, and Y. Feng. Model-checking linear-time properties of quantum systems. ACM Transactions on Computational Logic, 15(3):22:1-22:31, 2014. · Zbl 1354.68090 |
| [71] | M. Ying, S. Ying, and X. Wu. Invariants of quantum programs: characterisations and generation. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017), pages 818-832, Paris, France, 2017. ACM. · Zbl 1380.68135 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
