Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Communications in computer and information science

Automating the Comparison of Quantum Compilers for Quantum Circuits

Marie Salm, Johanna Barzen, Frank Leymann, Benjamin Weder, Karoline Wild

Published Jan 1, 2021• 30 citations
Publisher
DOI
10.1007/978-3-030-87568-8_4

Related papers

Automated Reasoning in Quantum Circuit Compilation

Dimitrios Thanos, Alejandro Villoria, Sebastiaan Brand +4 more

Lecture notes in computer science•Oct 12, 2024•4 citations

Quantum Circuit Compilation: An Emerging Application for Automated Reasoning

Davide Venturelli, N. Minh, Bryan O’Gorman +6 more

•Apr 11, 2019•29 citations

Prediction of Compilation Options for Quantum Circuits via Adaptive Deep Residual Neural Network

Shouli He, Liu Wen, Yangzhi Li +3 more

Abstract Quantum circuit compilation is an indispensable part of executing quantum circuits on quantum devices. It translates logical quantum circuits into physical quantum circuits that meet the device constraints. However, nonspecialist users require extensive expertise to effectively select and evaluate quantum circuit compilation processes. Therefore, this paper proposes a quantum circuit compilation option prediction method based on Deep Residual Attention Neural Network. The method aims to automate the selection of the best compilation scheme and enhance the efficiency and accuracy of quantum circuit compilation. Firstly, a quantum circuit feature extraction algorithm based on Time-Weighted Interaction Graph is proposed. This algorithm can effectively represent quantum circuits using fixed-length vectors, making the model input scalable. Secondly, for existing one-dimensional features, a quantum circuit compilation option prediction model based on Deep Residual Attention Neural Network is designed and trained. This model is capable of quickly and accurately predicting the optimal compilation option combination. Extensive experimental evaluations and comparisons are carried out on the MQT (Munich Quantum Toolkit) quantum circuit compilation dataset. These evaluations verify the effectiveness and advancement of the proposed method. Compared with the current state-of-the-art method (Random Forest), the proposed method improves the accuracy by 5.44%, the Top-3 accuracy by 2.6%, and the F1 by 2.05%.

Quantum Information and Computation•Mar 1, 2026•0 citations

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

Yunong Shi, Runzhou Tao, Li, Xupeng +4 more

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.

arXiv:1908.08963•Aug 23, 2019•10 citations

Efficient Verification of Results from Quantum Circuit Compilation Flows

Lukas Burgholzer, Robert Wille

Springer eBooks•Jan 1, 2026•0 citations

Giallar: push-button verification for the qiskit Quantum compiler

Runzhou Tao, Yunong Shi, Jianan Yao +5 more

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.

arXiv:2205.00661•ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)•Jun 2, 2022•47 citations
Abstract Quantum circuit compilation is an indispensable part of executing quantum circuits on quantum devices. It translates logical quantum circuits into physical quantum circuits that meet the device constraints. However, nonspecialist users require extensive expertise to effectively select and evaluate quantum circuit compilation processes. Therefore, this paper proposes a quantum circuit compilation option prediction method based on Deep Residual Attention Neural Network. The method aims to automate the selection of the best compilation scheme and enhance the efficiency and accuracy of quantum circuit compilation. Firstly, a quantum circuit feature extraction algorithm based on Time-Weighted Interaction Graph is proposed. This algorithm can effectively represent quantum circuits using fixed-length vectors, making the model input scalable. Secondly, for existing one-dimensional features, a quantum circuit compilation option prediction model based on Deep Residual Attention Neural Network is designed and trained. This model is capable of quickly and accurately predicting the optimal compilation option combination. Extensive experimental evaluations and comparisons are carried out on the MQT (Munich Quantum Toolkit) quantum circuit compilation dataset. These evaluations verify the effectiveness and advancement of the proposed method. Compared with the current state-of-the-art method (Random Forest), the proposed method improves the accuracy by 5.44%, the Top-3 accuracy by 2.6%, and the F1 by 2.05%.
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.
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.