zbMATH — the first resource for mathematics

A modeling and verification framework for optical quantum circuits. (English) Zbl 1425.68250
Summary: Quantum computing systems promise to increase the capabilities for solving problems which classical computers cannot handle adequately, such as integers factorization. In this paper, we present a formal modeling and verification approach for optical quantum circuits, where we build a rich library of optical quantum gates and develop a proof strategy in higher-order logic to reason about optical quantum circuits automatically. The constructed library contains a variety of quantum gates ranging from 1-qubit to 3-qubit gates that are sufficient to model most existing quantum circuits. As real world applications, we present the formal analysis of several quantum circuits including quantum full adders and the Grover’s oracle circuits, for which we have proved the behavioral correctness and calculated the operational success rate, which has never been provided in the literature. We show through several case studies the efficiency of the proposed framework in terms of the scalability and modularity.
68Q60 Specification and verification (program logics, model checking, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
81P68 Quantum computation
81V80 Quantum optics
Full Text: DOI
[1] Barenco, A.; Bennett, CH; Cleve, R.; DiVincenzo, DP; Margolus, N.; Shor, P.; Sleator, T.; Smolin, JA; Weinfurter, H., Elementary gates for quantum computation, Phys Rev A Am Phys Soc, 52, 3457-3467, (1995)
[2] Beillahi SM, Mahmoud MY (2019) HOL-light source code. https://github.com/beillahi/FMV-QC-HOL.git
[3] Beillahi SM, Mahmoud MY, Tahar S (2016) Hierarchical verification of quantum circuits. In: Proceedings of NASA formal methods (NFM 2016), LNCS 9690. Springer, pp 344-352
[4] Beillahi SM, Mahmoud MY, Tahar S (2016) Optical quantumgates formalization in hol light Technical Report, ECED epartment, Concordia University. Montreal, QC, Canada
[5] Bernstein, E.; Vazirani, U., Quantum complexity theory, SIAM J Comput, 26, 1411-1473, (1997) · Zbl 0895.68042
[6] Black PE, Lane AW (2004) Modeling quantum information systems. In: Proceedings of quantum information and computation II. SPIE 5436, pp. 340-347
[7] Boender J, Kammüller F,Nagarajan R(2015) Formalization of quantum protocols using Coq. In: Proceedings of international workshop on quantum physics and logic (QPL 2015), pp 71-83
[8] Bogoliubov, NN, On the theory of superfluidity, J Phys (USSR), 11, 23-32, (1947)
[9] Brown, KL; Munro, WJ; Kendon, VM, Using quantum computers for quantum simulation, Entropy, 12, 2268-2307, (2010) · Zbl 1229.81062
[10] Bruce JW, Thornton MA, Shivakumaraiah L, Kokate PS, Li X (2002) Efficient adder circuits based on a conservative reversible logic gate. In: Proceedings of IEEE computer society annual symposium on VLSI (ISVLSI 2002), pp 83-88
[11] Fowler, AG; Devitt, SJ; Hollenberg, LCL, Implementation of Shor’s algorithm on a linear nearest neighbour qubit array, Quantum Inf Comput, 4, 237-251, (2004) · Zbl 1175.81053
[12] Franke-Arnold S, Gay SJ, Puthoor IV (2013) Quantum process calculus for linear optical quantum computing. In: Proceedings of reversible computation (RC 2013), LNCS 7948. Springer, pp 234-246 · Zbl 1407.81063
[13] Golubitsky O, Falconer SM, Maslov D (2010) Synthesis of the optimal 4-bit reversible circuits. In: Proceedings of design automation conference (DAC 2010), pp. 653-656
[14] Grosse, D.; Wille, R.; Dueck, GW; Drechsler, R., Exact multiple-control toffoli network synthesis with SAT techniques, IEEE Trans Comput Aided Des Integ Circuits Syst, 28, 703-715, (2009)
[15] Häner T, Steiger DS, Smelyanskiy M, Troyer M (2016) High performance emulation of quantum circuits. In: Proceedings of international conference for high performance computing, networking, storage and analysis (SC 2016), pp 866-874
[16] Harrison J (2009) Handbook of practical logic and automated reasoning. Cambridge University Press, Cambridge · Zbl 1178.03001
[17] Harrison J (1996) HOL light: a tutorial introduction. proc. formal methods in computer-aided design (FMCAD1996), LNCS 1166. Springer, pp 265-269
[18] Harrison, J., Binary decision diagrams as a HOL derived rule, Comput J, 38, 162-170, (1995)
[19] Hung, WNN; Song, X.; Yang, G.; Yang, J.; Perkowski, MA, Optimal synthesis of multiple output boolean functions using a set of quantum gates by symbolic reachability analysis, IEEE Trans Comput Aided Des Integr Circuits Syst, 25, 1652-1663, (2006)
[20] Hung WNN, Song X, Yang G, Yang J, Perkowski MA (2004) Quantum logic synthesis by symbolic reachability analysis. In: Proceedings of design automation conference (DAC 2004), pp 838-841
[21] Khammassi N, Ashraf I, Fu X, Almudever CG, Bertels K (2017) QX: a high-performance quantum computer simulation platform. In: Proceedings of design, automation and test in Europe (DATE 2017), pp 464-469
[22] Kok, P.; Munro, WJ; Nemoto, K.; Ralph, TC; Dowling, JP; Milburn, GJ, Linear optical quantum computing with photonic qubits, Rev Mod Phys Am Phys Soc, 79, 135-174, (2007)
[23] Knill, E.; Laflamme, R.; Milburn, GJ, A scheme for efficient quantum computation with linear optics, Nature, 409, 46-52, (2001)
[24] Knill EH (1996) Conventions for quantum pseudocode. Technical Report, LAUR-96-2724, Los Alamos National Laboratory
[25] Liang, L.; Li, C., Realization of quantum SWAP gate between flying and stationary qubits, Phys Rev A Am Phys Soc, 72, 024303, (2005)
[26] Liu T, Li Y, Wang S, Mingsheng Y, Zhan N (2016) A theorem prover for quantum hoare logic and its applications. CoRR. arXiv:1601.03835
[27] Mahmoud MY (2015) Formal analysis of quantum optics. Ph.D. Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec
[28] Mahmoud MY, Panangaden P, Tahar S (2015) On the formal verification of optical quantum gates in HOL. In: Proceedings of formal methods for industrial critical systems (FMICS 2015), LNCS vol 9128. Springer, pp 198-211
[29] Mahmoud MY, Aravantinos V, Tahar S (2014) Formal verification of optical quantum flip gate. In: Proceedings interactive theorem proving (ITP 2014), LNCS vol 8558. Springer, pp 358-373 · Zbl 1416.68170
[30] MahmoudMY, Aravantinos V, Tahar S (2013) Formalization of infinite dimension linear spaces with application to quantum theory. In: Proceedings NASA formal methods (NFM 2013), LNCS vol 7871. Springer, pp 413-427
[31] Mandel L, Wolf E (1995) Optical coherence and quantum optics. Cambridge University Press, Cambridge
[32] Milburn, GJ, Quantum optical Fredkin gate, Phys Rev Lett Am Phys Soc, 62, 2124-2127, (1989)
[33] Nielsen MA, Chuang IL (2010) Quantum computation and quantum information. Cambridge University Press, Cambridge · Zbl 1288.81001
[34] Niemann, P.; Wille, R.; Miller, DM; Thornton, MA; Drechsler, R., QMDDs: efficient quantum function representation and manipulation, IEEE Trans Comput Aided Des Integr Circuits Syst, 35, 86-99, (2016)
[35] Niemann P, Wille R, Drechsler R (2014) Efficient synthesis of quantum circuits implementing Clifford group operations. In: Proceedings of Asia and South Pacific design automation conference (ASP-DAC 2014), pp 483-488
[36] Packel, EW, Hilbert space operators and quantum mechanics, Am Math Mon, 81, 863-873, (1974)
[37] Politi, A.; Matthews, JCF; O’Brien, JL, Shor’s quantum factoring algorithm on a photonic chip, Science, 325, 1221-1221, (2009) · Zbl 1226.81052
[38] Ralph, TC; Resch, KJ; Gilchrist, A., Efficient Toffoli gates using qudits, Phys Rev A Am Phys Soc, 75, 022313, (2007)
[39] Ralph, TC; Gilchrist, A.; Milburn, GJ; Munro, WJ; Glancy, S., Quantum computation with optical coherent states, Phys Rev A Am Phys Soc, 68, 042319, (2003)
[40] Ralph, TC; Langford, NK; Bell, TB; White, AG, Linear optical controlled-NOT gate in the coincidence basis, Phys Rev A Am Phys Soc, 65, 062324, (2002)
[41] RevLib: an online resource for benchmarks within the domain of reversible and quantum circuits. http://www.revlib.org/ 2018.
[42] Rand R, Paykin J, Zdancewic S (2018) QWIRE practice: formal verification of quantum verification in Coq. In: Proceedings of international conference on quantum physics and logic (QPL 2017), EPTCS, vol 266, pp 119-13
[43] Rand R, Paykin J, Zdancewic S (2017) QWIRE: a core language for quantum circuits. In: Proceedings of ACM SIGPLAN symposium on principles of programming languages (POPL 2017), ACM, pp 846-858 · Zbl 1380.68087
[44] Soeken M, Wille R, Hilken C, Przigoda N, Drechsler R (2012) Synthesis of reversible circuits with minimal lines for large functions. In: Proceedings of Asia and South Pacific design automation conference (ASP-DAC 2012), pp 85-92
[45] Sasanian Z, Wille R, Miller DM (2012) Realizing reversible circuits using a new class of quantum gates. In: Proceedings of design automation conference (DAC 2012), pp 36-41
[46] Shende, VV; Bullock, SS; Markov, IL, Synthesis of quantumlogic circuits, IEEE Trans Comput Aided Des Integr Circuits Syst, 25, 1000-1010, (2006)
[47] Shor, PW, Polynomial-time algorithms for prime factorization and discrete logarithms on a quantum computer, SIAM J Comput, 26, 1484-1509, (1997) · Zbl 1005.11065
[48] Smelyanskiy M, Sawaya NPD, Aspuru-Guzik A (2016) qHiPSTER: the quantum high performance software testing environment. CoRR. arXiv:1601.07195
[49] Viamontes GF, Rajagopalan M, Markov IL, Hayes JP (2003) Gate level simulation of quantum circuits. In: Proceedings of Asia and South Pacific design automation conference (ASP-DAC 2003), pp 295-301
[50] Wang, H.; He, Y.; Li, YH; Su, ZE; Li, B.; Huang, HL; Ding, X.; Chen, MC; Liu, C.; Qin, J.; Li, JP; He, YM; Schneider, C.; Kamp, M.; Peng, CZ; Höfling, S.; Lu, CY; Pan, JW, High-efficiency multiphoton Boson sampling, Nat Photon, 11, 361-365, (2017)
[51] Wecker D, Svore KM(2014) LIQUi \({\rangle}\)|: A software design architecture and domain-specific language for quantum computing. CoRR. arXiv:1402.4467
[52] Wille R, Lye A, Drechsler R (2014) Optimal SWAP gate insertion for nearest neighbor quantum circuits. In: Proceedings of Asia and South Pacific design automation conference (ASP-DAC 2014), pp 489-494
[53] Yamashita, S.; Markov, IL, Fast equivalence-checking for quantum circuits, Quantum Inf Comput, 10, 721-734, (2010) · Zbl 1237.81059
[54] Ying, M., Floyd-Hoare logic for quantum programs, ACM Trans Program Lang Syst, 33, 19:1-19:49, (2011)
[55] Zulehner A, Wille R (2017) Advanced simulation of quantum computations. CoRR. arXiv:1707.00865 · Zbl 06850926
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.