research-article

Giallar: push-button verification for the qiskit Quantum compiler

Authors:

Ali Javadi-Abhari,

Andrew W. Cross,

Frederic T. Chong,

Ronghui GuAuthors Info & Claims

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

Pages 641 - 656

https://doi.org/10.1145/3519939.3523431

Published: 09 June 2022 Publication History

Abstract

This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewrite rules for showing the equivalence of symbolic quantum circuits. With Giallar, we implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. Our evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance.

References

[1]

Matthew Amy. 2019. Towards Large-scale Functional Verification of Universal Quantum Circuits. Electronic Proceedings in Theoretical Computer Science, 287 (2019), Jan, 1–21. https://doi.org/10.4204/EPTCS.287.1

[2]

Matthew Amy, Martin Roetteler, and Krysta M Svore. 2017. Verified Compilation of Space-Efficient Reversible Circuits. In Proceedings of the 29th International Conference on Computer Aided Verification (CAV ’17). 3–21. https://doi.org/10.1007/978-3-319-63390-9_1

[3]

Juan Carlos Garcia-Escartin and Pedro Chamorro-Posada. 2011. Equivalent Quantum Circuits. Universidad de Valladolid, Dpto. Teoria de la Senal e Ing. arxiv:1110.2998v1.

[4]

Christophe Chareton, Sébastien Bardin, François Bobot, Valentin Perrelle, and Benoît Valiron. 2021. An Automated Deductive Verification Framework for Circuit-building Quantum Programs. In Proceedings of the 30th European Symposium on Programming (ESOP ’21). 148–177. https://doi.org/10.1007/978-3-030-72019-3_6

Digital Library

[5]

The Coq Development Team. 2012. The Coq Reference Manual, version 8.4. Available electronically at http://coq.inria.fr/doc

[6]

Andrew W Cross, Lev S Bishop, John A Smolin, and Jay M Gambetta. 2017. Open quantum assembly language. arxiv:1707.03429.

[7]

Manjeet Dahiya and Sorav Bansal. 2017. Black-box equivalence checking across compiler optimizations. In Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS ’17). 127–147. https://doi.org/10.1007/978-3-319-71237-6_7

[8]

Leonardo De Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS ’08). 4963, 337–340. https://doi.org/10.1007/978-3-540-78800-3_24

[9]

Philippe Gille and Tamas Szamuely. 2009. Central Simple Algebras and Galois Cohomology. Cambridge University Press. https://doi.org/10.1017/cbo9780511607219

[10]

Daniel M. Greenberger, Michael A. Horne, and Anton Zeilinger. 1989. Going Beyond Bell’s Theorem. Springer Netherlands, Dordrecht. 69–72. https://doi.org/10.1007/978-94-017-0849-4_10

[11]

Ronghui Gu, Jérémie Koenig, Tahina Ramananandro, Zhong Shao, Xiongnan Newman Wu, Shu-Chun Weng, and Haozhong Zhang. 2015. Deep specifications and certified abstraction layers. In Proceedings of the 42nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL ’15). 595–608. https://doi.org/10.1145/2775051.2676975

Digital Library

[12]

Ronghui Gu, Zhong Shao, Jieung Kim, Xiongnan Newman Wu, Jérémie Koenig, Vilhelm Sjöberg, Hao Chen, David Costanzo, and Tahina Ramananandro. 2018. Certified concurrent abstraction layers. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’18). 646–661. https://doi.org/10.1145/3296979.3192381

Digital Library

[13]

Shubhani Gupta, Abhishek Rose, and Sorav Bansal. 2020. Counterexample-guided correlation algorithm for translation validation. Proceedings of the ACM on Programming Languages, 4, OOPSLA (2020), 1–29. https://doi.org/10.1145/3428289

Digital Library

[14]

Thomas Häner, Torsten Hoefler, and Matthias Troyer. 2018. Using Hoare Logic for Quantum Circuit Optimization. arxiv:1810.00375.

[15]

Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. 2021. A Verified Optimizer for Quantum Circuits. Proceedings of the ACM on Programming Languages, 5, POPL (2021), https://doi.org/10.1145/3434318

Digital Library

[16]

C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM, 12, 10 (1969), Oct, 576–580. https://doi.org/10.1145/363235.363259

Digital Library

[17]

Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. 2019. Quantitative robustness analysis of quantum programs. Proceedings of the ACM on Programming Languages, 3, POPL (2019), 1–29. https://doi.org/10.1145/3290344

Digital Library

[18]

Chris Lattner and Vikram Adve. 2003. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. UIUC. http://llvm.cs.uiuc.edu/

[19]

Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM, 52, 7 (2009), 107–115. https://doi.org/10.1145/1538788.1538814

Digital Library

[20]

Ang Li, Samuel Stein, Sriram Krishnamoorthy, and James Ang. 2021. QASMBench: A Low-level QASM Benchmark Suite for NISQ Evaluation and Simulation. arxiv:2005.13018.

[21]

Gushu Li, Yufei Ding, and Yuan Xie. 2019. Tackling the Qubit Mapping Problem for NISQ-era Quantum Devices. In Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’19). 1001–1014. https://doi.org/10.1145/3297858.3304023

Digital Library

[22]

Shusen Liu, Xin Wang, Li Zhou, Ji Guan, Yinan Li, Yang He, Runyao Duan, and Mingsheng Ying. 2018. Q|SI〉 : A Quantum Programming Environment. In Lecture Notes in Computer Science. 11180, Springer, 133–164. https://doi.org/10.1007/978-3-030-01461-2_8

[23]

Nuno P. Lopes, David Menendez, Santosh Nagarakatte, and John Regehr. 2015. Provably Correct Peephole Optimizations with Alive. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’15). 22–32. https://doi.org/10.1145/2737924.2737965

Digital Library

[24]

Dmitri Maslov, Gerhard W. Dueck, Michael Miller, and Camille Negrevergne. 2008. Quantum Circuit Simplification and Level Compaction. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 27, 3 (2008), 436–444. https://doi.org/10.1109/TCAD.2007.911334

Digital Library

[25]

David C. McKay, Thomas Alexander, Luciano Bello, Michael J. Biercuk, Lev Bishop, Jiayin Chen, Jerry M. Chow, Antonio D. Córcoles, Daniel Egger, Stefan Filipp, Juan Gomez, Michael Hush, Ali Javadi-Abhari, Diego Moreda, Paul Nation, Brent Paulovicks, Erick Winston, Christopher J. Wood, James Wootton, and Jay M. Gambetta. 2018. Qiskit Backend Specifications for OpenQASM and OpenPulse Experiments. arxiv:1809.03452.

[26]

Microsoft. 2016. F*. https://github.com/FStarLang/FStar/

[27]

Frank Mueller, Greg Byrd, and Patrick Dreher. 2020. Programming Quantum Computers: A Primer with IBM Q and D-Wave Exercises. https://sites.google.com/ncsu.edu/qc-tutorial

[28]

Prakash Murali, Jonathan M. Baker, Ali Javadi-Abhari, Frederic T. Chong, and Margaret Martonosi. 2019. Noise-Adaptive Compiler Mappings for Noisy Intermediate-Scale Quantum Computers. In Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems (ASLPOS ’19). 1015–1029. https://doi.org/10.1145/3297858.3304075

Digital Library

[29]

Prakash Murali, David C. Mckay, Margaret Martonosi, and Ali Javadi-Abhari. 2020. Software Mitigation of Crosstalk on Noisy Intermediate-Scale Quantum Computers. In Proceedings of the 25th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’20). 1001–1016. https://doi.org/10.1145/3373376.3378477

Digital Library

[30]

Yunseong Nam, Neil J Ross, Yuan Su, Andrew M Childs, and Dmitri Maslov. 2018. Automated Optimization of Large Quantum Circuits with Continuous Parameters. npj Quantum Information, 4, 1 (2018), 1–12.

[31]

George C Necula. 2000. Translation Validation for an Optimizing Compiler. In Proceedings of the 21st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’00). 83–94. https://doi.org/10.1145/349299.349314

Digital Library

[32]

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. 2019. Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP ’19). 225–242. https://doi.org/10.1145/3341301.3359641

Digital Library

[33]

Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. 2017. Hyperkernel: Push-Button Verification of an OS Kernel. In Proceedings of the 26th Symposium on Operating Systems Principles (SOSP ’17). 252–269. https://doi.org/10.1145/3132747.3132748

Digital Library

[34]

Michael A. Nielsen and Isaac L. Chuang. 2011. Quantum Computation and Quantum Information: 10th Anniversary Edition (10th ed.). Cambridge University Press. https://doi.org/10.1017/CBO9780511976667

[35]

Jennifer Paykin, Robert Rand, and Steve Zdancewic. 2017. QWIRE: A Core Language for Quantum Circuits. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (PLDI ’17). 846–858. https://doi.org/10.1145/3009837.3009894

Digital Library

[36]

2021. Available at https://qiskit.org/documentation/index.htm

[37]

2019. Available at https://github.com/Qiskit/qiskit-terra/issues/1871

[38]

2021. Available at https://github.com/Qiskit/qiskit-terra

[39]

2018. Available at https://github.com/Qiskit/qiskit-terra/issues

[40]

Robert Rand, Jennifer Paykin, Dong-Ho Lee, and Steve Zdancewic. 2019. ReQWIRE: Reasoning about Reversible Quantum Circuits. arxiv:1901.10118.

[41]

Gabriel Ryan, Justin Wong, Jianan Yao, Ronghui Gu, and Suman Jana. 2020. CLN2INV: Learning Loop Invariants with Continuous Logic Networks. In Proceedings of the 8th International Conference on Learning Representations (ICLR ’20). https://openreview.net/forum?id=HJlfuTEtvB

[42]

Yunong Shi, Nelson Leung, Pranav Gokhale, Zane Rossi, David I. Schuster, Henry Hoffmann, and Frederic T. Chong. 2019. Optimized Compilation of Aggregated Instructions for Realistic Quantum Computers. In Proceedings of the 24th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS ’19). 1031–1044. https://doi.org/10.1145/3297858.3304018

Digital Library

[43]

Yunong Shi, Runzhou Tao, Xupeng Li, Ali Javadi-Abhari, Andrew W Cross, Frederic T Chong, and Ronghui Gu. 2019. CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler. arxiv:1908.08963.

[44]

Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI ’16). 1–16. https://www.usenix.org/conference/osdi16/technical-sessions/presentation/sigurbjarnarson

[45]

Runzhou Tao, Yunong Shi, Jianan Yao, John Hui, Frederic T Chong, and Ronghui Gu. 2021. Gleipnir: toward practical error analysis for Quantum programs. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI ’21). 48–64. https://doi.org/10.1145/3453483.3454029

Digital Library

[46]

George F. Viamontes, Igor L. Markov, and John P. Hayes. 2007. Checking Equivalence of Quantum Circuits and States. In Proceedings of the 2007 International Conference on Computer-Aided Design (ICCAD ’07). 69–74. https://doi.org/10.1109/ICCAD.2007.4397246

[47]

Jianan Yao, Gabriel Ryan, Justin Wong, Suman Jana, and Ronghui Gu. 2020. Learning nonlinear loop invariants with gated continuous logic networks. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI ’20). 106–120. https://doi.org/10.1145/3385412.3385986

Digital Library

[48]

Vladimir Zamdzhiev. 2016. Quantum Computing: the Good, the bad, and the (not so) Ugly!. Invited Talk at University of Oxford.

[49]

Pengzhan Zhao, Jianjun Zhao, Zhongtao Miao, and Shuhan Lan. 2021. Bugs4Q: A Benchmark of Real Bugs for Quantum Programs. In Proceedings of the 36th IEEE/ACM International Conference on Automated Software Engineering (ASE ’21). 1373–1376. https://doi.org/10.1109/ASE51524.2021.9678908

Cited By

Jiang H(2024)Qubit Recycling RevisitedProceedings of the ACM on Programming Languages10.1145/36564288:PLDI(1264-1287)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656428
Fang WYing M(2024)Symbolic Execution for Quantum Error Correction ProgramsProceedings of the ACM on Programming Languages10.1145/36564198:PLDI(1040-1065)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656419
Deng HTao RPeng YWu X(2024)A Case for Synthesis of Recursive Quantum Unitary ProgramsProceedings of the ACM on Programming Languages10.1145/36329018:POPL(1759-1788)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632901
Show More Cited By

Index Terms

Giallar: push-button verification for the qiskit Quantum compiler
1. Theory of computation
  1. Models of computation
    1. Quantum computation theory
      1. Quantum information theory
  2. Semantics and reasoning
    1. Program reasoning
      1. Program verification

Recommendations

symQV: Automated Symbolic Verification of Quantum Programs
Formal Methods
Abstract
We present symQV, a symbolic execution framework for writing and verifying quantum computations in the quantum circuit model. symQV can automatically verify that a quantum program complies with a first-order specification. We formally introduce a ...
Pervasive Compiler Verification -- From Verified Programs to Verified Systems

We report in this paper on the formal verification of a simple compiler for the C-like programming language C0. The compiler correctness proof meets the special requirements of pervasive system verification and allows to transfer correctness properties ...
Rotational abstractions for verification of quantum Fourier transform circuits
Abstract
With the race to build large‐scale quantum computers and efforts to exploit quantum algorithms for efficient problem solving in science and engineering disciplines, the requirement to have efficient and scalable verification methods are of vital ...

A scalable and efficient formal verification method for quantum Fourier transform circuits, capable of verifying unto 10,000 qubits QFT circuit in less than an hour time is proposed. The work uses rotational abstractions to achieve the verification and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 2022

1038 pages

ISBN:9781450392655

DOI:10.1145/3519939

General Chair:
Ranjit Jhala
University of California at San Diego, USA
,
Program Chair:
Işil Dillig
University of Texas at Austin, USA

Copyright © 2022 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 June 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Conference

PLDI '22

Sponsor:

SIGPLAN

PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation

June 13 - 17, 2022

CA, San Diego, USA

Acceptance Rates

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

12
Total Citations
View Citations
375
Total Downloads

Downloads (Last 12 months)90
Downloads (Last 6 weeks)18

Reflects downloads up to 01 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Jiang H(2024)Qubit Recycling RevisitedProceedings of the ACM on Programming Languages10.1145/36564288:PLDI(1264-1287)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656428
Fang WYing M(2024)Symbolic Execution for Quantum Error Correction ProgramsProceedings of the ACM on Programming Languages10.1145/36564198:PLDI(1040-1065)Online publication date: 20-Jun-2024
https://dl.acm.org/doi/10.1145/3656419
Deng HTao RPeng YWu X(2024)A Case for Synthesis of Recursive Quantum Unitary ProgramsProceedings of the ACM on Programming Languages10.1145/36329018:POPL(1759-1788)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632901
Lewis MZuliani PSoudjani S(2024)Automated Verification of Silq Quantum Programs using SMT Solvers2024 IEEE International Conference on Quantum Software (QSW)10.1109/QSW62656.2024.00027(125-134)Online publication date: 7-Jul-2024
https://doi.org/10.1109/QSW62656.2024.00027
Yan PJiang HYu N(2024)Approximate Relational Reasoning for Quantum ProgramsComputer Aided Verification10.1007/978-3-031-65633-0_22(495-519)Online publication date: 24-Jul-2024
https://dl.acm.org/doi/10.1007/978-3-031-65633-0_22
Quetschlich NBurgholzer LWille R(2023)MQT Bench: Benchmarking Software and Design Automation Tools for Quantum ComputingQuantum10.22331/q-2023-07-20-10627(1062)Online publication date: 20-Jul-2023
https://doi.org/10.22331/q-2023-07-20-1062
Hietala KRand RLi LHung SWu XHicks M(2023)A Verified Optimizer for Quantum CircuitsACM Transactions on Programming Languages and Systems10.1145/360463045:3(1-35)Online publication date: 23-Sep-2023
https://dl.acm.org/doi/10.1145/3604630
Xu AMolavi APick LTannu SAlbarghouthi A(2023)Synthesizing Quantum-Circuit OptimizersProceedings of the ACM on Programming Languages10.1145/35912547:PLDI(835-859)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591254
Wen ZLiu YTan SChen JZhu MHan DYin JXu MChen W(2023)Quantivine: A Visualization Approach for Large-Scale Quantum Circuit Representation and AnalysisIEEE Transactions on Visualization and Computer Graphics10.1109/TVCG.2023.332714830:1(573-583)Online publication date: 25-Oct-2023
https://dl.acm.org/doi/10.1109/TVCG.2023.3327148
Ye JXia SZhang FArcaini PMa LZhao JIshikawa FBissyandé TKlein JBird CSarro F(2023)QuraTest: Integrating Quantum Specific Features in Quantum Program TestingProceedings of the 38th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE56229.2023.00196(1149-1161)Online publication date: 11-Nov-2023
https://dl.acm.org/doi/10.1109/ASE56229.2023.00196
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents