Source-linked AI summary
PyZX: Large Scale Automated Diagrammatic Reasoning
Aleks Kissinger, John van de Wetering
TL;DR
Large-scale reasoning with ZX-diagrams requires practical tools beyond the calculus itself. PyZX addresses this gap with automated rewriting, verification, circuit extraction, and visualisation, and demonstrates fast processing of large circuits while identifying extraction and gate-language limitations.
Problem
Practical applications of the ZX-calculus require tools that can reason with ZX-diagrams on a large scale.
Method
PyZX is an open-source Python library combining rewrite strategies, linear-map verification, circuit extraction heuristics, and interoperability features for quantum circuits and ZX-diagrams.
Results
PyZX handles tens of thousands of vertices in seconds, including a 15-qubit, 2500-gate reduction in under 5 seconds and a 567-to-279 T-gate optimisation in under a second.
Takeaways & Limitations
PyZX provides a practical platform for automated diagrammatic reasoning, circuit optimisation, correctness validation, visualisation, and integration with other software.
Takeaways & Limitations
Circuit extraction remains incompletely understood, and the ZX-calculus is less natural for directly reasoning about Toffoli and CCZ gates.
Abstract
from arXiv · showhide
The ZX-calculus is a graphical language for reasoning about ZX-diagrams, a type of tensor networks that can represent arbitrary linear maps between qubits. Using the ZX-calculus, we can intuitively reason about quantum theory, and optimise and validate quantum circuits. In this paper we introduce PyZX, an open source library for automated reasoning with large ZX-diagrams. We give a brief introduction to the ZX-calculus, then show how PyZX implements methods for circuit optimisation, equality validation, and visualisation and how it can be used in tandem with other software. We end with a set of challenges that when solved would enhance the utility of automated diagrammatic reasoning.
1 Introduction
PyZX is an open-source Python library for large-scale reasoning with quantum circuits and ZX-diagrams. It combines diagram rewriting, verification, visualisation, interoperability, and interactive or command-line use, while highlighting challenges for automated diagrammatic reasoning.
- 1 Introduction: PyZX is a free and open-source Python library designed for reasoning with large quantum circuits and ZX-diagrams.The project is hosted on GitHub and licensed under GPLv3.
- 1 Introduction: Built-in rewrite strategies simplify ZX-diagrams, reduce Clifford diagrams to pseudo-normal form, optimise T-count, and verify optimised-circuit correctness.These capabilities are presented as core functionality of the library.
- 1 Introduction: PyZX supports circuit and diagram visualisation plus input and output in QASM, QC, Quipper, TikZ, and Quantomatic qGraph formats.It can also be used with TikZiT and other software workflows.
- 1 Introduction: Users can run PyZX interactively in Jupyter Notebooks or as a command-line tool for optimising many circuits and combining it with other procedures.Jupyter supports on-the-fly visualisation, while the command-line interface supports circuit-to-circuit optimisation.
- 1 Introduction: The paper focuses on PyZX itself, describing its capabilities, uses, and implementation details before presenting community challenges.The challenges concern expanding automated diagrammatic reasoning and understanding its limitations.
2 The ZX-calculus
The ZX-calculus represents linear maps with diagrams built from wires, spiders, and Hadamard structures. Quantum circuits are translated into these diagrams, which can be equated through graphical rewrite rules while ignoring global scalar factors here.
- 2 The ZX-calculus: A ZX-diagram consists of wires and spiders, with left wires as inputs and right wires as outputs; diagrams compose by joining wires or stacking tensor products.The diagram denotes a linear map assembled through composition and tensor product.
- 2 The ZX-calculus: Z spiders are green dots and X spiders are red dots, and each spider can have any number of input or output wires.Diagrams may also include SWAPs represented by wire crossings.
- 2 The ZX-calculus: Hadamard gates are represented either by yellow boxes or by blue dashed Hadamard edges between spiders, with both notations translatable back into spiders.PyZX treats the Hadamard gate as an edge type rather than an additional generator.
- 2 The ZX-calculus: ZX-calculus rewrite rules equate diagrams representing the same linear map up to a non-zero global scalar factor in this paper.The rules are presented for phases α,β ∈[0,2π), with colour-interchanged versions also valid through specified rules.
- 2 The ZX-calculus: Quantum circuits are translated gate by gate into equivalent ZX-diagrams and composed according to circuit structure; gates such as Toffoli are first expressed in Clifford+T form.The starting circuits use a specified universal gate set, whose gates have convenient spider representations.
3 Core functionality
PyZX provides Python data structures and visualization tools for constructing, importing, manipulating, and displaying ZX-diagrams and circuits. Its hierarchical rewrite system supports simplification, circuit extraction, and conventional circuit-to-circuit optimisation.
- 3.1 ZX-diagrams and circuits: PyZX represents circuits with Circuit objects and ZX-diagrams with Graph objects, whose typed vertices, edges, and phases encode diagram structure.Graphs abstract their implementation through BaseGraph, while the default GraphS backend can handle diagrams with hundreds of thousands of vertices.
- 3.1 ZX-diagrams and circuits: PyZX uses Jupyter and Matplotlib to construct and visualise ZX-diagrams interactively, while also supporting command-line circuit-to-circuit optimisation.Figure 3 illustrates creating a diagram from scratch and visualising it in a notebook.
- 3.1 ZX-diagrams and circuits: The Circuit class imports and exports QASM, Quipper, and QC/TFC circuits and supports gate-level transformations and optimisation schemes.It can convert Toffoli circuits into Clifford+T form and take gate adjoints.
- 3.2 Simplification and verification: Its hierarchical simplification system combines matchers, rewriters, basic simplifiers, and compound strategies that repeatedly apply reductions.Matchers find non-overlapping rule applications, rewriters apply graph changes, and compound simplifiers combine lower-level procedures in a chosen order.
- 3.2 Simplification and verification: The top-level strategies reduce Clifford circuits to GS-LC pseudo-normal form and perform significant T-count optimisation.These capabilities are implemented by clifford_simp and full_reduce, respectively, with local complementation and pivoting-based rewrites also included.
- 3.3 Circuit-to-circuit optimisation: Because simplification can produce non-circuit-like diagrams, PyZX provides heuristic circuit extraction and phase teleportation for in-place optimisation, alongside the TODD optimiser.Extraction has no known guarantee for arbitrary heuristic inputs, whereas diagrams produced by full_reduce have so far always appeared extractable.
4 TikZiT and Quantomatic integration
PyZX connects ZX-diagrams with TikZ, TikZiT, and Quantomatic for editing, storage, visualisation, and theorem-proving workflows. These integrations support both document-oriented diagram export and interactive external editing.
- TikZiT integration: PyZX exports ZX-diagrams as TikZ figures for import into LaTeX and direct editing in TikZiT.It can also launch TikZiT with a loaded diagram or generate TikZ output from a circuit on the command line.
- Quantomatic integration: PyZX supports Quantomatic’s qGraph format, allowing non-circuit ZX-diagrams to be stored and read.When Quantomatic is installed, PyZX can open diagrams in its GUI and receive the edited result.
- Quantomatic integration: Quantomatic can use PyZX’s rewrite strategies by importing PyZX as a Python module.This extends the external graphical theorem prover with PyZX’s rewriting functionality.
5 Performance
PyZX simplifies large ZX-diagrams quickly, with performance advantages attributed partly to its hand-written rewrite rules. It supports Clifford normal-form reduction and practical T-count optimisation.
- Scalability: PyZX simplifies ZX-diagrams with tens of thousands of vertices in seconds.A 15-qubit, 2500-gate circuit takes less than 5 seconds to reduce.
- Clifford simplification: PyZX's Clifford normal-form runtime appears to follow a power-law whose constant depends on the number of qubits.Figure 5 benchmarks the procedure on a consumer laptop and shows a least-squares power-law fit.
- Comparison with Quantomatic: Hand-written Python rewrite rules let PyZX avoid Quantomatic's strict bang-box matching, potentially making simplification much faster.This speed comes with a need for more validation to ensure implementation correctness.
- Comparison with Quantomatic: Quantomatic took upwards of half an hour for a 5-qubit circuit with fewer than 100 gates, whereas PyZX handles larger Clifford circuits in seconds.The comparison concerns bringing Clifford circuits to normal form.
- T-count optimisation: PyZX reduced the 9-qubit nth prime6.tfc circuit from 567 T gates to 279 in less than a second.The original circuit contains 1241 gates, and the example comes from the Reversible Circuit Benchmark page.
6 Challenges
The paper identifies several open challenges for extending PyZX and automated diagrammatic reasoning, including ancilla-aware optimisation, circuit extraction, routing, alternative calculi, simulation, and lattice-surgery compilation.
- Open challenges: PyZX remains a capable general-purpose circuit optimiser, but the authors identify many ways it could be improved.These improvements are presented as challenges for future contributors and collaborators.
- Challenge 1: Ancillae: Existing ZX-calculus optimisation results concern only ancilla-free optimisation; ancilla-assisted optimisation remains unknown.The challenge is to exploit ancillae when optimising ZX-diagrams.
- Challenge 2: Circuit extraction: Circuit extraction remains limited, although PyZX has a heuristic that always seems to work on diagrams produced by simplification.Better understanding could enable extraction of smaller circuits, while the general problem is believed to be complexity-theoretically hard.
- Challenge 3: Circuit routing: Circuit routing should be combined with the ZX-calculus because physical and logical quantum circuits restrict two-qubit interactions to adjacent qubits.Circuit extraction provides a natural place for routing to occur.
- Challenge 4: ZH-calculus: The ZH-calculus may improve optimisation for Toffoli and CCZ circuits because ZX handles those gates only indirectly.ZX is described as especially well-suited to Clifford and phase gates.
- Challenge 5: Circuit simulation: ZX-diagrams could support strong quantum-circuit simulation by simplifying scalar ZX-diagrams before calculating specific output probabilities.This is proposed as a possible efficiency improvement over other tensor-network approaches.
- Challenge 6: Lattice surgery: The ZX-calculus could automate compilation from quantum circuits to lattice-surgery operations for surface-code computation.The proposal follows from ZX's suitability for describing lattice surgery.