Giallar: Push-Button Verification for the Qiskit Quantum Compiler
Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari,, Andrew W. Cross, Frederic T. Chong, Ronghui Gu

TL;DR
Giallar is an automated, specification-free verification toolkit for quantum compiler passes, capable of handling complex semantics and unbounded loops, demonstrated on Qiskit with effective bug detection and minimal performance impact.
Contribution
Giallar introduces a novel automated verification approach for quantum compilers that requires no manual invariants or proofs, handling unbounded loops and complex semantics.
Findings
Verified 44 out of 56 Qiskit compiler passes
Detected and confirmed 3 bugs in Qiskit
Most passes verified within seconds with modest overhead
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.…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsQuantum Computing Algorithms and Architecture · Parallel Computing and Optimization Techniques · Logic, programming, and type systems
