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

ACM/IEEE Design Automation Conference (DAC)

ZXNet: ZX Calculus-Driven Graph Neural Network Framework for Quantum Circuit Equivalence Checking

Navnil Choudhury, Ameya Bhave, Kanad Basu

Published Jun 22, 2025• 0 citations
Publisher

Abstract

Quantum circuit execution often requires transpilation into hardware-compatible instructions, which can significantly alter the original design, making equivalence checking essential. However, existing approaches struggle with scalability and computational overhead. In this paper, we present ZXNet, a transformative framework for quantum circuit equivalence checking using $\mathbf{Z X}$ calculus-based graph abstractions. Leveraging graph neural networks, ZXNet captures complex equivalence patterns by integrating critical local and global circuit features. ZXNet achieves 99.4% validation accuracy, and up to $62 \times$ speedup over state-of-the-art methods, furnishing improvements of 45.83% in scalability, 42.22% in per-qubit verification time, and 5.94% in accuracy, outperforming state-of-the-art approaches.

DOI
10.1109/dac63849.2025.11133226

Related papers

ZX-DB: A Graph Database for Quantum Circuit Simplification and Rewriting via the ZX-Calculus

Valter Uotila, Cong Yu, Bo Zhao

Quantum computing is an emerging computational paradigm with the potential to outperform classical computers in solving a variety of problems. To achieve this, quantum programs are typically represented as quantum circuits, which must be optimized and adapted for target hardware through quantum circuit compilation. We introduce ZX-DB, a data-driven system that performs quantum circuit simplification and rewriting inside a graph database using ZX-calculus, a complete graphical formalism for quantum mechanics. ZX-DB encodes ZX-calculus rewrite rules as standard openCypher queries and executes them on an example graph database engine, Memgraph, enabling efficient, database-native transformations of large-scale quantum circuits. ZX-DB integrates correctness validation via tensor and graph equivalence checks and is evaluated against the state-of-the-art PyZX framework. Experimental results show that ZX-DB achieves up to an order-of-magnitude speedup for independent rewrites, while exposing pattern-matching bottlenecks in current graph database engines. By uniting quantum compilation and graph data management, ZX-DB opens a new systems direction toward scalable, database-supported quantum computing pipelines.

quant-pharXiv:2511.13033•Nov 18, 2025•0 citations

Quantum Circuit Verification via Graph Neural Networks

Jincheng Zhang

The verification of quantum circuits is a critical step in ensuring the reliable execution of quantum computations. Traditional methods often struggle with the exponential complexity arising from the superposition and entanglement inherent in quantum mechanics. This work proposes a novel approach utilizing Graph Neural Networks (GNNs) to address this challenge. Quantum circuits are represented as graphs, where nodes correspond to quantum gates and edges represent data flow. The GNN learns to identify patterns within these graph representations that signify potential errors or deviations from the intended circuit behavior. This automated verification process offers a scalable solution compared to exhaustive simulation or analytical methods. The core of this approach lies in leveraging the expressive power of GNNs to capture complex correlations within the circuit structure, ultimately leading to more efficient and accurate verification. We demonstrate the feasibility and effectiveness of this methodology through a theoretical framework and outline future research directions.

•Sep 1, 2026•0 citations

Equivalence Checking of Quantum Circuits With the ZX-Calculus

Tom Peham, Lukas Burgholzer, Robert Wille

As state-of-the-art quantum computers are capable of running increasingly complex algorithms, the need for automated methods to design and test potential applications rises. Equivalence checking of quantum circuits is an important, yet hardly automated, task in the development of the quantum software stack. Recently, new methods have been proposed that tackle this problem from widely different perspectives. One of them is based on the ZX-calculus, a graphical rewriting system for quantum computing. However, the power and capability of this equivalence checking method has barely been explored. The aim of this work is to evaluate the ZX-calculus as a tool for equivalence checking of quantum circuits. To this end, it is demonstrated how the ZX-calculus based approach for equivalence checking can be expanded in order to verify the results of compilation flows and optimizations on quantum circuits. It is also shown that the ZX-calculus based method is not complete—especially for quantum circuits with ancillary qubits. In order to properly evaluate the proposed method, we conduct a detailed case study by comparing it to two other state-of-the-art methods for equivalence checking: one based on path-sums and another based on decision diagrams. The proposed methods have been integrated into the publicly available QCEC tool (https://github.com/cda-tum/qcec) which is part of the Munich Quantum Toolkit (MQT).

arXiv:2208.12820•IEEE Journal on Emerging and Selected Topics in Circuits and Systems•Aug 26, 2022•46 citations

Optimizing Quantum Circuits via ZX Diagrams using Reinforcement Learning and Graph Neural Networks

Alexander Mattick, Maniraman Periyasamy, Christian Ufrecht +4 more

Quantum computing is currently strongly limited by the impact of noise, in particular introduced by the application of two-qubit gates. For this reason, reducing the number of two-qubit gates is of paramount importance on noisy intermediate-scale quantum hardware. To advance towards more reliable quantum computing, we introduce a framework based on ZX calculus, graph-neural networks and reinforcement learning for quantum circuit optimization. By combining reinforcement learning and tree search, our method addresses the challenge of selecting optimal sequences of ZX calculus rewrite rules. Instead of relying on existing heuristic rules for minimizing circuits, our method trains a novel reinforcement learning policy that directly operates on ZX-graphs, therefore allowing us to search through the space of all possible circuit transformations to find a circuit significantly minimizing the number of CNOT gates. This way we can scale beyond hard-coded rules towards discovering arbitrary optimization rules. We demonstrate our method's competetiveness with state-of-the-art circuit optimizers and generalization capabilities on large sets of diverse random circuits.

arXiv:2504.03429•Apr 4, 2025•0 citations

Quantum architecture search with neural predictor based on ZX-calculus

Shanchuan Li, Daisuke Tsukayama, Jun‐ichi Shirakashi +2 more

Abstract With the ongoing advances in noisy intermediate-scale quantum hardware, variational quantum algorithms have demonstrated significant potential in a range of quantum applications. However, obtaining high-performance, shallow-parameterized quantum circuits typically requires repeated optimization of the gate parameters over a large set of candidate circuits, resulting in prohibitively high evaluation costs. To address this challenge, this study proposes a novel predictor-based quantum architecture search (PQAS-ZX) method that leverages ZX-calculus. In this approach, a quantum circuit is first represented as a ZX diagram that supports multi-step equivalent simplifications at the diagram level. By applying these equivalence transformations, multiple circuit variants that share the same performance metric are generated, thereby significantly expanding the training dataset and enhancing the ability of the predictor to manage diverse circuit structures. ZX diagrams offer more flexible characterizations of multi-qubit entanglement and phase interactions, as well as higher-level equivalent transformations, compared with the state-of-the-art predictor-based quantum architecture search with graph measures (PQAS-GM). Numerical simulations of three variational quantum eigensolver tasks, namely the transverse-field Ising, Heisenberg, and BeH2 molecular models, demonstrated that PQAS-ZX required only approximately 80.9%, 82.9%, and 76.1% of the queries required by PQAS-GM, respectively, to achieve the same probability of reaching the target ground-state energy. These results highlight the advantage of using ZX diagrams to identify high-quality circuits efficiently and alleviate the evaluation burden of quantum architecture searches.

EPJ Quantum Technology•Sep 2, 2025•5 citations

Graph Rewriting Language as a Platform for Quantum Diagrammatic Calculi

Tei, Kayo, Mishina, Haruto, Yamamoto, Naoki +1 more

Systematic discovery of optimization paths in quantum circuit simplification remains a challenge. Today, ZX-calculus, a computing model for quantum circuit transformation, is attracting attention for its highly abstract graph-based approach. Whereas existing tools such as PyZX and Quantomatic offer domain-specific support for quantum circuit optimization, visualization and theorem-proving, we present a complementary approach using LMNtal, a general-purpose hierarchical graph rewriting language, to establish a diagrammatic transformation and verification platform with model checking. Our methodology shows three advantages: (1) manipulation of ZX-diagrams through native graph transformation rules, enabling direct implementation of basic rules; (2) quantified pattern matching via QLMNtal extensions, greatly simplifying rule specification; and (3) interactive visualization and validation of optimization paths through state space exploration. Through case studies, we demonstrate how our framework helps understand optimization paths and design new algorithms and strategies. This suggests that the declarative language LMNtal and its toolchain could serve as a new platform to investigate quantum circuit transformation from a different perspective.

arXiv:2511.15581•Nov 19, 2025•0 citations
Quantum circuit execution often requires transpilation into hardware-compatible instructions, which can significantly alter the original design, making equivalence checking essential. However, existing approaches struggle with scalability and computational overhead. In this paper, we present ZXNet, a transformative framework for quantum circuit equivalence checking using ZX\mathbf{Z X}ZX calculus-based graph abstractions. Leveraging graph neural networks, ZXNet captures complex equivalence patterns by integrating critical local and global circuit features. ZXNet achieves 99.4% validation accuracy, and up to 62×62 \times62× speedup over state-of-the-art methods, furnishing improvements of 45.83% in scalability, 42.22% in per-qubit verification time, and 5.94% in accuracy, outperforming state-of-the-art approaches.
Quantum computing is an emerging computational paradigm with the potential to outperform classical computers in solving a variety of problems. To achieve this, quantum programs are typically represented as quantum circuits, which must be optimized and adapted for target hardware through quantum circuit compilation. We introduce ZX-DB, a data-driven system that performs quantum circuit simplification and rewriting inside a graph database using ZX-calculus, a complete graphical formalism for quantum mechanics. ZX-DB encodes ZX-calculus rewrite rules as standard openCypher queries and executes them on an example graph database engine, Memgraph, enabling efficient, database-native transformations of large-scale quantum circuits. ZX-DB integrates correctness validation via tensor and graph equivalence checks and is evaluated against the state-of-the-art PyZX framework. Experimental results show that ZX-DB achieves up to an order-of-magnitude speedup for independent rewrites, while exposing pattern-matching bottlenecks in current graph database engines. By uniting quantum compilation and graph data management, ZX-DB opens a new systems direction toward scalable, database-supported quantum computing pipelines.
The verification of quantum circuits is a critical step in ensuring the reliable execution of quantum computations. Traditional methods often struggle with the exponential complexity arising from the superposition and entanglement inherent in quantum mechanics. This work proposes a novel approach utilizing Graph Neural Networks (GNNs) to address this challenge. Quantum circuits are represented as graphs, where nodes correspond to quantum gates and edges represent data flow. The GNN learns to identify patterns within these graph representations that signify potential errors or deviations from the intended circuit behavior. This automated verification process offers a scalable solution compared to exhaustive simulation or analytical methods. The core of this approach lies in leveraging the expressive power of GNNs to capture complex correlations within the circuit structure, ultimately leading to more efficient and accurate verification. We demonstrate the feasibility and effectiveness of this methodology through a theoretical framework and outline future research directions.
As state-of-the-art quantum computers are capable of running increasingly complex algorithms, the need for automated methods to design and test potential applications rises. Equivalence checking of quantum circuits is an important, yet hardly automated, task in the development of the quantum software stack. Recently, new methods have been proposed that tackle this problem from widely different perspectives. One of them is based on the ZX-calculus, a graphical rewriting system for quantum computing. However, the power and capability of this equivalence checking method has barely been explored. The aim of this work is to evaluate the ZX-calculus as a tool for equivalence checking of quantum circuits. To this end, it is demonstrated how the ZX-calculus based approach for equivalence checking can be expanded in order to verify the results of compilation flows and optimizations on quantum circuits. It is also shown that the ZX-calculus based method is not complete—especially for quantum circuits with ancillary qubits. In order to properly evaluate the proposed method, we conduct a detailed case study by comparing it to two other state-of-the-art methods for equivalence checking: one based on path-sums and another based on decision diagrams. The proposed methods have been integrated into the publicly available QCEC tool (https://github.com/cda-tum/qcec) which is part of the Munich Quantum Toolkit (MQT).
Quantum computing is currently strongly limited by the impact of noise, in particular introduced by the application of two-qubit gates. For this reason, reducing the number of two-qubit gates is of paramount importance on noisy intermediate-scale quantum hardware. To advance towards more reliable quantum computing, we introduce a framework based on ZX calculus, graph-neural networks and reinforcement learning for quantum circuit optimization. By combining reinforcement learning and tree search, our method addresses the challenge of selecting optimal sequences of ZX calculus rewrite rules. Instead of relying on existing heuristic rules for minimizing circuits, our method trains a novel reinforcement learning policy that directly operates on ZX-graphs, therefore allowing us to search through the space of all possible circuit transformations to find a circuit significantly minimizing the number of CNOT gates. This way we can scale beyond hard-coded rules towards discovering arbitrary optimization rules. We demonstrate our method's competetiveness with state-of-the-art circuit optimizers and generalization capabilities on large sets of diverse random circuits.
Abstract With the ongoing advances in noisy intermediate-scale quantum hardware, variational quantum algorithms have demonstrated significant potential in a range of quantum applications. However, obtaining high-performance, shallow-parameterized quantum circuits typically requires repeated optimization of the gate parameters over a large set of candidate circuits, resulting in prohibitively high evaluation costs. To address this challenge, this study proposes a novel predictor-based quantum architecture search (PQAS-ZX) method that leverages ZX-calculus. In this approach, a quantum circuit is first represented as a ZX diagram that supports multi-step equivalent simplifications at the diagram level. By applying these equivalence transformations, multiple circuit variants that share the same performance metric are generated, thereby significantly expanding the training dataset and enhancing the ability of the predictor to manage diverse circuit structures. ZX diagrams offer more flexible characterizations of multi-qubit entanglement and phase interactions, as well as higher-level equivalent transformations, compared with the state-of-the-art predictor-based quantum architecture search with graph measures (PQAS-GM). Numerical simulations of three variational quantum eigensolver tasks, namely the transverse-field Ising, Heisenberg, and BeH2 molecular models, demonstrated that PQAS-ZX required only approximately 80.9%, 82.9%, and 76.1% of the queries required by PQAS-GM, respectively, to achieve the same probability of reaching the target ground-state energy. These results highlight the advantage of using ZX diagrams to identify high-quality circuits efficiently and alleviate the evaluation burden of quantum architecture searches.
Systematic discovery of optimization paths in quantum circuit simplification remains a challenge. Today, ZX-calculus, a computing model for quantum circuit transformation, is attracting attention for its highly abstract graph-based approach. Whereas existing tools such as PyZX and Quantomatic offer domain-specific support for quantum circuit optimization, visualization and theorem-proving, we present a complementary approach using LMNtal, a general-purpose hierarchical graph rewriting language, to establish a diagrammatic transformation and verification platform with model checking. Our methodology shows three advantages: (1) manipulation of ZX-diagrams through native graph transformation rules, enabling direct implementation of basic rules; (2) quantified pattern matching via QLMNtal extensions, greatly simplifying rule specification; and (3) interactive visualization and validation of optimization paths through state space exploration. Through case studies, we demonstrate how our framework helps understand optimization paths and design new algorithms and strategies. This suggests that the declarative language LMNtal and its toolchain could serve as a new platform to investigate quantum circuit transformation from a different perspective.