Giallar: Push-button Verification for the Qiskit Quantum Compiler
Fri 17 Jun 2022 03:50 - 04:10 at Toucan - Quantum
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 rewriting rules for reducing 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.
Thu 16 JunDisplayed time zone: Pacific Time (US & Canada) change
15:30 - 16:50 | |||
15:30 20mTalk | Quartz: Superoptimization of Quantum Circuits PLDI Mingkuan Xu Carnegie Mellon University, Zikun Li University of California, Los Angeles (UCLA), Oded Padon VMware Research, Sina Lin Microsoft, Jessica Pointing University of Oxford, Auguste Hirth University of California, Los Angeles (UCLA), Henry Ma University of California, Los Angeles (UCLA), Jens Palsberg University of California, Los Angeles (UCLA), Alex Aiken Stanford Univeristy, Umut A. Acar Carnegie Mellon University, Zhihao Jia Carnegie Mellon University DOI | ||
15:50 20mTalk | Giallar: Push-button Verification for the Qiskit Quantum Compiler PLDI Runzhou Tao Columbia University, Yunong Shi Amazon, Jianan Yao Columbia University, Xupeng Li Columbia University, Ali Javadi-Abhari IBM, Andrew Cross IBM T.J Watson Research Center, Frederic T. Chong University of Chicago, Ronghui Gu Columbia University DOI | ||
16:10 20mTalk | Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra PLDI Yuxiang Peng University of Maryland, Mingsheng Ying Tsinghua University, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD DOI | ||
16:30 20mTalk | PyLSE: A Pulse-Transfer Level Language for Superconductor Electronics PLDI Michael Christensen University of California at Santa Barbara, Georgios Tzimpragos UC Santa Barbara, Harlan Kringen UC Santa Barbara, Jennifer Volk UC Santa Barbara, Timothy Sherwood UC Santa Barbara, Ben Hardekopf UC Santa Barbara DOI | ||
Fri 17 JunDisplayed time zone: Pacific Time (US & Canada) change
03:30 - 04:50 | |||
03:30 20mTalk | Quartz: Superoptimization of Quantum Circuits PLDI Mingkuan Xu Carnegie Mellon University, Zikun Li University of California, Los Angeles (UCLA), Oded Padon VMware Research, Sina Lin Microsoft, Jessica Pointing University of Oxford, Auguste Hirth University of California, Los Angeles (UCLA), Henry Ma University of California, Los Angeles (UCLA), Jens Palsberg University of California, Los Angeles (UCLA), Alex Aiken Stanford Univeristy, Umut A. Acar Carnegie Mellon University, Zhihao Jia Carnegie Mellon University DOI | ||
03:50 20mTalk | Giallar: Push-button Verification for the Qiskit Quantum Compiler PLDI Runzhou Tao Columbia University, Yunong Shi Amazon, Jianan Yao Columbia University, Xupeng Li Columbia University, Ali Javadi-Abhari IBM, Andrew Cross IBM T.J Watson Research Center, Frederic T. Chong University of Chicago, Ronghui Gu Columbia University DOI | ||
04:10 20mTalk | Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra PLDI Yuxiang Peng University of Maryland, Mingsheng Ying Tsinghua University, Xiaodi Wu Department of Computer Science, Institute for Advanced Computer Studies, and Joint Center for Quantum Information and Computer Science, University of Maryland, MD DOI | ||
04:30 20mTalk | PyLSE: A Pulse-Transfer Level Language for Superconductor Electronics PLDI Michael Christensen University of California at Santa Barbara, Georgios Tzimpragos UC Santa Barbara, Harlan Kringen UC Santa Barbara, Jennifer Volk UC Santa Barbara, Timothy Sherwood UC Santa Barbara, Ben Hardekopf UC Santa Barbara DOI | ||