PyZX: Large Scale Automated Diagrammatic Reasoning

Abstract

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.

In Proceedings QPL 2019, arXiv:2004.14750

References in corpus (1)

• Optimising Clifford Circuits with Quantomatic

Cited by in corpus (48)

• Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus
• Yao.jl: Extensible, Efficient Framework for Quantum Algorithm Design
• A Verified Optimizer for Quantum Circuits
• There and back again: A circuit extraction tale
• Equivalence Checking of Quantum Circuits with the ZX-Calculus
• Formal Verification of Quantum Programs: Theory, Tools and Challenges
• DisCoPy: Monoidal Categories in Python
• Distributing circuits over heterogeneous, modular quantum computing network architectures
• A High Performance Compiler for Very Large Scale Surface Code Computations
• Benchmarking Quantum Computer Simulation Software Packages: State Vector Simulators
• Reducing 2-QuBit Gate Count for ZX-Calculus based Quantum Circuit Optimization
• Shallow unitary decompositions of quantum Fredkin and Toffoli gates for connectivity-aware equivalent circuit averaging
• Hypergraph Simplification: Linking the Path-sum Approach to the ZH-calculus
• Operads for complex system design specification, analysis and synthesis
• Robust Qubit Mapping Algorithm via Double-Source Optimal Routing on Large Quantum Circuits
• Efficient Formal Verification of Quantum Error Correcting Programs
• A compiler for universal photonic quantum computers
• SuperNOVA: Design Strategies and Opportunities for Interactive Visualization in Computational Notebooks
• Hybrid quantum-classical circuit simplification with the ZX-calculus
• Annealing Optimisation of Mixed ZX Phase Circuits
• Reinforcement Learning Based Quantum Circuit Optimization via ZX-Calculus
• The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation
• How to Sum and Exponentiate Hamiltonians in ZXW Calculus
• Linear and non-linear relational analyses for Quantum Program Optimization
• Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation
• Unitary Synthesis of Clifford+T Circuits with Reinforcement Learning
• The Qupit Stabiliser ZX-travaganza: Simplified Axioms, Normal Forms and Graph-Theoretic Simplification
• Quantum Linear Optics via String Diagrams
• AND-gates in ZX-calculus: Spider Nest Identities and QBC-completeness
• Diagrammatic Analysis for Parameterized Quantum Circuits
• Application of ZX-calculus to Quantum Architecture Search
• Multi-controlled Phase Gate Synthesis with ZX-calculus applied to Neutral Atom Hardware
• Procedurally Optimised ZX-Diagram Cutting for Efficient T-Decomposition in Classical Simulation
• Automating Equational Proofs in Dirac Notation
• Qsyn: A Developer-Friendly Quantum Circuit Synthesis Framework for NISQ Era and Beyond
• Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
• Improving Qubit Routing by Using Entanglement Mediated Remote Gates
• Quantum Circuit Unoptimization
• Fast Classical Simulation of Quantum Circuits via Parametric Rewriting in the ZX-Calculus
• ViCAR: Visualizing Categories with Automated Rewriting in Coq
• ZX Graphical Calculus for Continuous-Variable Quantum Processes
• Type-Based Verification of Connectivity Constraints in Lattice Surgery
• High-Precision Multi-Qubit Clifford+T Synthesis by Unitary Diagonalization
• String Diagrams for Defect-Based Surface Code Computing
• Quantum phase estimation with optimal confidence interval using three control qubits
• Unleashing Optimizations in Dynamic Circuits through Branch Expansion
• Nontrivial multi-product commutation relation toward reducing T-count in sequential Pauli-based computation
• Formal Verification of Quantum Ancilla Safety