CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler

Abstract

We present CertiQ, a verification framework for writing and verifying compiler passes of Qiskit, the most widely-used quantum compiler. To our knowledge, CertiQ is the first effort enabling the verification of real-world quantum compiler passes in a mostly-automated manner. Compiler passes written in the CertiQ interface with annotations can be used to generate verification conditions, as well as the executable code that can be integrated into Qiskit. CertiQ introduces the quantum circuit calculus to enable the efficient checking of equivalence of quantum circuits by encoding such a checking procedure into an SMT problem. CertiQ also provides a verified library of widely-used data structures, transformation functions for circuits, and conversion functions for different quantum data representations. This verified library not only enables modular verification but also sheds light on future quantum compiler design. We have re-implemented and verified 26 (out of 30) Qiskit compiler passes in CertiQ, during which three bugs are detected in the Qiskit implementation. Our verified compiler pass implementations passed all of Qiskit's regression tests without showing noticeable performance loss.

References in corpus (15)

• Quantum Computing in the NISQ era and beyond
• Validating quantum computers using randomized model circuits
• Resource-Aware Quantum Programming with General Recursion and Quantum Control
• Quantum Circuit Simplification and Level Compaction
• Software Mitigation of Crosstalk on Noisy Intermediate-Scale Quantum Computers
• Optimized Compilation of Aggregated Instructions for Realistic Quantum Computers
• Towards Large-scale Functional Verification of Universal Quantum Circuits
• Qiskit Backend Specifications for OpenQASM and OpenPulse Experiments
• QWIRE Practice: Formal Verification of Quantum Circuits in Coq
• Verified compilation of space-efficient reversible circuits
• ReQWIRE: Reasoning about Reversible Quantum Circuits
• Identity check is QMA-complete
• Equivalent Quantum Circuits
• Verified Optimization in a Quantum Intermediate Representation
• Model Checking Quantum Systems --- A Survey

Cited by in corpus (6)

• A Verified Optimizer for Quantum Circuits
• Bugs in Quantum Computing Platforms: An Empirical Study
• Formal Verification of Quantum Programs: Theory, Tools and Challenges
• symQV: Automated Symbolic Verification of Quantum Programs
• Twist: Sound Reasoning for Purity and Entanglement in Quantum Programs
• Gleipnir: Toward Practical Error Analysis for Quantum Programs (Extended Version)