Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation

Benjamin Bichsel, Anouk Paradis, Maximilian Baader, and Martin Vechev

ETH Zurich, Switzerland

Find this paper interesting or want to discuss? Scite or leave a comment on SciRate.


Stabilizer simulation can efficiently simulate an important class of quantum circuits consisting exclusively of Clifford gates. However, all existing extensions of this simulation to arbitrary quantum circuits including non-Clifford gates suffer from an exponential runtime.
To address this challenge, we present a novel approach for efficient stabilizer simulation on arbitrary quantum circuits, at the cost of lost precision. Our key idea is to compress an exponential sum representation of the quantum state into a single $abstract$ summand covering (at least) all occurring summands. This allows us to introduce an $\textit{abstract stabilizer simulator}$ that efficiently manipulates abstract summands by $over-approximating$ the effect of circuit operations including Clifford gates, non-Clifford gates, and (internal) measurements.
We implemented our abstract simulator in a tool called Abstraqt and experimentally demonstrate that Abstraqt can establish circuit properties intractable for existing techniques.

► BibTeX data

► References

[1] Daniel Gottesman. ``The Heisenberg Representation of Quantum Computers''. Technical Report arXiv:quant-ph/​9807006. arXiv (1998).

[2] Scott Aaronson and Daniel Gottesman. ``Improved Simulation of Stabilizer Circuits''. Physical Review A 70, 052328 (2004).

[3] Robert Rand, Aarthi Sundaram, Kartik Singhal, and Brad Lackey. ``Extending gottesman types beyond the clifford group''. In The Second International Workshop on Programming Languages for Quantum Computing (PLanQC 2021). (2021). url: https:/​/​pldi21.sigplan.org/​details/​planqc-2021-papers/​9/​Extending-Gottesman-Types-Beyond-the-Clifford-Group.

[4] Aleks Kissinger and John van de Wetering. ``Simulating quantum circuits with ZX-calculus reduced stabiliser decompositions''. Quantum Science and Technology 7, 044001 (2022).

[5] Sergey Bravyi, Dan Browne, Padraic Calpin, Earl Campbell, David Gosset, and Mark Howard. ``Simulation of quantum circuits by low-rank stabilizer decompositions''. Quantum 3, 181 (2019).

[6] Hakop Pashayan, Oliver Reardon-Smith, Kamil Korzekwa, and Stephen D. Bartlett. ``Fast estimation of outcome probabilities for quantum circuits''. PRX Quantum 3, 020361 (2022).

[7] ``Classical simulation of quantum circuits with partial and graphical stabiliser decompositions''. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022).

[8] Patrick Cousot and Radhia Cousot. ``Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints''. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. Pages 238–252. POPL '77New York, NY, USA (1977). ACM.

[9] Patrick Cousot and Radhia Cousot. ``Abstract interpretation frameworks''. Journal of logic and computation 2, 511–547 (1992).

[10] Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. ``A static analyzer for large safety-critical software''. ACM SIGPLAN Notices 38, 196–207 (2003).

[11] Francesco Logozzo and Manuel Fähndrich. ``Pentagons: A weakly relational abstract domain for the efficient validation of array accesses''. Science of Computer Programming 75, 796–807 (2010).

[12] Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. ``AI2: Safety and Robustness Certification of Neural Networks with Abstract Interpretation''. In 2018 IEEE Symposium on Security and Privacy (SP). Pages 3–18. San Francisco, CA (2018). IEEE.

[13] Michael A. Nielsen and Isaac L. Chuang. ``Quantum computation and quantum information: 10th anniversary edition''. Cambridge University Press. (2010).

[14] Gadi Aleksandrowicz, Thomas Alexander, Panagiotis Barkoutsos, Luciano Bello, Yael Ben-Haim, David Bucher, Francisco Jose Cabrera-Hernández, Jorge Carballo-Franquis, Adrian Chen, Chun-Fu Chen, Jerry M. Chow, Antonio D. Córcoles-Gonzales, Abigail J. Cross, Andrew Cross, Juan Cruz-Benito, Chris Culver, Salvador De La Puente González, Enrique De La Torre, Delton Ding, Eugene Dumitrescu, Ivan Duran, Pieter Eendebak, Mark Everitt, Ismael Faro Sertage, Albert Frisch, Andreas Fuhrer, Jay Gambetta, Borja Godoy Gago, Juan Gomez-Mosquera, Donny Greenberg, Ikko Hamamura, Vojtech Havlicek, Joe Hellmers, Łukasz Herok, Hiroshi Horii, Shaohan Hu, Takashi Imamichi, Toshinari Itoko, Ali Javadi-Abhari, Naoki Kanazawa, Anton Karazeev, Kevin Krsulich, Peng Liu, Yang Luh, Yunho Maeng, Manoel Marques, Francisco Jose Martín-Fernández, Douglas T. McClure, David McKay, Srujan Meesala, Antonio Mezzacapo, Nikolaj Moll, Diego Moreda Rodríguez, Giacomo Nannicini, Paul Nation, Pauline Ollitrault, Lee James O'Riordan, Hanhee Paik, Jesús Pérez, Anna Phan, Marco Pistoia, Viktor Prutyanov, Max Reuter, Julia Rice, Abdón Rodríguez Davila, Raymond Harry Putra Rudy, Mingi Ryu, Ninad Sathaye, Chris Schnabel, Eddie Schoute, Kanav Setia, Yunong Shi, Adenilton Silva, Yukio Siraichi, Seyon Sivarajah, John A. Smolin, Mathias Soeken, Hitomi Takahashi, Ivano Tavernelli, Charles Taylor, Pete Taylour, Kenso Trabing, Matthew Treinish, Wes Turner, Desiree Vogt-Lee, Christophe Vuillot, Jonathan A. Wildstrom, Jessica Wilson, Erick Winston, Christopher Wood, Stephen Wood, Stefan Wörner, Ismail Yunus Akhalwaya, and Christa Zoufal. ``Qiskit: An open-source framework for quantum computing'' (2019).

[15] Charles R. Harris, K. Jarrod Millman, Stéfan J. van der Walt, Ralf Gommers, Pauli Virtanen, David Cournapeau, Eric Wieser, Julian Taylor, Sebastian Berg, Nathaniel J. Smith, Robert Kern, Matti Picus, Stephan Hoyer, Marten H. van Kerkwijk, Matthew Brett, Allan Haldane, Jaime Fernández del Río, Mark Wiebe, Pearu Peterson, Pierre Gérard-Marchant, Kevin Sheppard, Tyler Reddy, Warren Weckesser, Hameer Abbasi, Christoph Gohlke, and Travis E. Oliphant. ``Array programming with NumPy''. Nature 585, 357–362 (2020).

[16] Siu Kwan Lam, Antoine Pitrou, and Stanley Seibert. ``Numba: a LLVM-based Python JIT compiler''. In Proceedings of the Second Workshop on the LLVM Compiler Infrastructure in HPC. Pages 1–6. LLVM '15New York, NY, USA (2015). Association for Computing Machinery.

[17] Craig Gidney. ``Stim: a fast stabilizer circuit simulator''. Quantum 5, 497 (2021).

[18] Henry S. Warren. ``Hacker's delight''. Addison-Wesley Professional. (2012). 2nd edition.

[19] Aleks Kissinger and John van de Wetering. ``PyZX: Large Scale Automated Diagrammatic Reasoning''. In Bob Coecke and Matthew Leifer, editors, Proceedings 16th International Conference on Quantum Physics and Logic, Chapman University, Orange, CA, USA., 10-14 June 2019. Volume 318 of Electronic Proceedings in Theoretical Computer Science, pages 229–241. Open Publishing Association (2020).

[20] Matthew Amy. ``Towards Large-scale Functional Verification of Universal Quantum Circuits''. Electronic Proceedings in Theoretical Computer Science 287, 1–21 (2019).

[21] Nengkun Yu and Jens Palsberg. ``Quantum abstract interpretation''. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation. Pages 542–558. PLDI 2021New York, NY, USA (2021). Association for Computing Machinery.

[22] Antoine Miné. ``Weakly Relational Numerical Abstract Domains''. PhD Thesis (2004). url: https:/​/​www-apr.lip6.fr/​ mine/​these/​these-color.pdf.

[23] Simon Perdrix. ``Quantum Entanglement Analysis Based on Abstract Interpretation''. In Proceedings of the 15th International Symposium on Static Analysis. Pages 270–282. SAS '08Berlin, Heidelberg (2008). Springer-Verlag.

[24] Kentaro Honda. ``Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism''. Electronic Proceedings in Theoretical Computer Science 195 (2015).

[25] Kesha Hietala, Robert Rand, Shih-Han Hung, Liyi Li, and Michael Hicks. ``Proving Quantum Programs Correct''. Leibniz International Proceedings in Informatics (LIPIcs) 193, 21:1–21:19 (2021).

[26] Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoît Valiron. ``An automated deductive verification framework for circuit-building quantum programs''. In Programming Languages and Systems. Pages 148–177. Springer International Publishing (2021).

[27] Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. ``Invariants of quantum programs: Characterisations and generation''. SIGPLAN Not. 52, 818–832 (2017).

Cited by

On Crossref's cited-by service no data on citing works was found (last attempt 2023-12-07 04:31:38). On SAO/NASA ADS no data on citing works was found (last attempt 2023-12-07 04:31:39).