AI Chat Paper
Note: Please note that the following content is generated by AMiner AI. SciOpen does not take any responsibility related to this content.
{{lang === 'zh_CN' ? '文章概述' : 'Summary'}}
{{lang === 'en_US' ? '中' : 'Eng'}}
Chat more with AI
Powered by AMiner. Clicking this button will take you away from SciOpen.
Home Journal of Computer Science and Technology Article
Article Link
Cite
EndNote(RIS) BibTeX
Collect
Submit Manuscript
Show Outline
Outline
Show full outline
Hide outline
Outline
Show full outline
Hide outline
Regular Paper

Symbolic Reasoning About Quantum Circuits in Coq

Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, 200062, China
John Hopcroft Center of Computer Science, Shanghai Jiao Tong University, Shanghai, 200240, China
Yanqi Lake Beijing Institute of Mathematical Sciences and Applications, Beijing, 101408, China
Centre for Quantum Software and Information, University of Technology Sydney, Sydney, NSW, 2007, Australia
Show Author Information

Abstract

A quantum circuit is a computational unit that transforms an input quantum state to an output state. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.

Keywords

quantum circuitsymbolic reasoningDirac notationCoq

Electronic Supplementary Material

Download File(s)
jcst-36-6-1291-Highlights.pdf (81.5 KB)

References

[1]
Nielsen M A, Chuang I L. Quantum Computation and Quantum Information: 10th Anniversary Edition. Cambridge University Press, 2010. DOI: 10.1017/CBO9780511976667.
Crossref
[2]
Paykin J, Rand R, Zdancewic S. QWIRE: A core language for quantum circuits. In Proc. the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan. 2017, pp.846-858. DOI: 10.1145/3009837.3009894.
Crossref
[3]

Dirac P. A new notation for quantum mechanics. Mathematical Proceedings of the Cambridge Philosophical Society, 1939, 35(3): 416-418. DOI: 10.1017/S0305004100021162.
Crossref Google Scholar
[4]
Shi W, Cao Q, Deng Y, Jiang H, Feng Y. Symbolic reasoning about quantum circuits in Coq. arXiv: 2005.11023, 2021. https://arxiv.org/abs/2005.11023, Sept. 2021.
[5]

Kafatos M. Bell’s Theorem, Quantum Theory, and Conceptions of the Universe. Kluwer Academics, 1989.
Crossref Google Scholar
[6]

Bennett C H, Brassard G, Crépeau C, Jozsa R, Peres A, Wootters W. Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Physical Review Letters, 1993, 70(13): 1895-1899. DOI: 10.1103/PhysRevLett.70.1895.
Crossref Google Scholar
[7]

Deutsch D, Jozsa R. Rapid solutions of problems by quantum computation. Proceedings of the Royal Society A: Mathematical and Physical Sciences, 1992, 439(1907): 553-558. DOI: 10.1098/rspa.1992.0167.
Crossref Google Scholar
[8]
Boender J, Kammüller F, Nagarajan R. Formalization of quantum protocols using Coq. In Proc. the 12th International Workshop on Quantum Physics and Logic, Jul. 2015, pp.71-83. DOI: 10.4204/EPTCS.195.6.
Crossref
[9]
Cruz-Filipe L, Geuvers H, Wiedijk F. C-CoRN, the constructive Coq repository at Nijmegen. In Proc. the 3rd Int. Conf. Mathematical Knowledge Management, Sept. 2004, pp.88-103. DOI: 10.1007/978-3-540-27818-4_7.
Crossref
[10]

Cano G, Cohen C, Déenès M, Mörtberg A, Vincent S. Formalized linear algebra over elementary divisor rings in Coq. Logical Methods in Computer Science, 2016, 12(2): Article No. 7. DOI: 10.2168/LMCS-12(2:7)2016.
Crossref Google Scholar
[11]
Rand R, Paykin J, Zdancewic S. QWIRE practice: Formal verification of quantum circuits in Coq. In Proc. the 14th Int. Conf. Quantum Physics and Logic, Jul. 2018, pp.119-132. DOI: 10.4204/EPTCS.266.8.
Crossref
[12]
Rand R, Paykin J, Lee D, Zdancewic S. ReQWIRE: Reasoning about reversible quantum circuits. In Proc. the 15th Int. Conf. Quantum Physics and Logic, Jun. 2018, pp.299-312. DOI: 10.4204/EPTCS.287.17.
Crossref
[13]
Hietala K, Rand R, Hung S, Wu X, Hicks M. Verified optimization in a quantum intermediate representation. arXiv: 1904.06319, 2019. https://arxiv.org/abs/1904.06319, Sept. 2021.
[14]

Nam Y, Ross N, Su Y, Childs A, Maslov D. Automated optimization of large quantum circuits with continuous parameters. npj Quantum Information, 2018, 4(1): Article No. 23. DOI: 10.1038/s41534-018-0072-4.
Crossref Google Scholar
[15]

Mahmoud M Y, Felty A P. Formalization of metatheory of the Quipper quantum programming language in a linear logic. Journal of Automated Reasoning, 2019, 63(4): 967-1002. DOI: 10.1007/s10817-019-09527-x.
Crossref Google Scholar
[16]

Felty A P, Momigliano A. Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. Journal of Automated Reasoning, 2012, 48(1): 43-105. DOI: 10.1007/s10817-010-9194-x.
Crossref Google Scholar
[17]
Green A S, Lumsdaine P L, Ross N J, Selinger P, Valiron B. Quipper: A scalable quantum programming language. In Proc. the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, Jun. 2013, pp.333-342. DOI: 10.1145/2491956.2462177.
Crossref
[18]
Liu J, Zhan B, Wang S, Ying S, Liu T, Li Y, Ying M, Zhan N. Formal verification of quantum algorithms using quantum Hoare logic. In Proc. the 31st Int. Conf. Computer Aided Verification, Jul. 2019, pp.187-207. DOI: 10.1007/978-3-030-25543-5_12.
Crossref
[19]
Nipkow T, Paulson L, Wenzel M. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002. DOI: 10.1007/3-540-45949-9.
Crossref
[20]

Ying M. Foundations of Quantum Programming. Morgan Kaufmann, 2016.
Crossref Google Scholar
[21]

Unruh D. Quantum relational Hoare logic. Proceedings of the ACM on Programming Languages, 2019, 3(POPL): Article No. 33. DOI: 10.1145/3290346.
Crossref Google Scholar
[22]

Beillahi S M, Mahmoud M Y, Tahar S. A modeling and verification framework for optical quantum circuits. Formal Aspects of Computing, 2019, 31(3): 321-351. DOI: 10.1007/s00165-019-00480-5.
Crossref Google Scholar
[23]
Mahmoud M Y, Aravantinos Y, Tahar S. Formalization of infinite dimension linear spaces with application to quantum theory. In Proc. the 5th Int. Symp. NASA Formal Methods, May 2013, pp.413-427. DOI: 10.1007/978-3-642-38088-4_28.
Crossref
[24]
Chareton C, Bardin S, Bobot F, Perrelle V, Valiron B. An automated deductive verification framework for circuit-building quantum programs. In Proc. the 30th European Symposium on Programming, March 27-April 1, 2021, pp.148-177. DOI: 10.1007/978-3-030-72019-3_6.
Crossref
[25]
Amy M. Towards large-scale functional verification of universal quantum circuits. In Proc. the 15th Int. Conf. Quantum Physics and Logic, Jun. 2018, pp.1-21. DOI: 10.4204/EPTCS.287.1.
Crossref
[26]
Shor P W. Algorithms for quantum computation: Discrete log and factoring. In Proc. the 35th Annual Symposium on Foundations of Computer Science, Nov. 1994, pp.124-133. DOI: 10.1109/SFCS.1994.365700.
Crossref
Journal of Computer Science and Technology
Volume 36 Issue 6,
November 2021
Pages 1291-1306
DOI: 10.1007/s11390-021-1637-9
Cite this article:
Shi W-J, Cao Q-X, Deng Y-X, et al. Symbolic Reasoning About Quantum Circuits in Coq. Journal of Computer Science and Technology, 2021, 36(6): 1291-1306. https://doi.org/10.1007/s11390-021-1637-9

458

Views

3

Crossref

4

Web of Science

4

Scopus

0

CSCD

Altmetrics
Received: 31 May 2021
Accepted: 07 November 2021
Published: 30 November 2021
© Institute of Computing Technology, Chinese Academy of Sciences 2021
Return