VyZX: Formal Verification of a Graphical Quantum Language
This work addresses the problem of formal verification for quantum computing researchers and proof engineers, though it is incremental as it applies existing proof assistant techniques to a specific graphical language.
The authors tackled the challenge of formally verifying graphical quantum languages, which are difficult to reason about using traditional inductive methods, by developing VyZX, a verified library that proves the soundness of ZX-calculus rewrite rules and integrates visualization tools for proof engineers.
Graphical languages are a convenient shorthand to represent computation, with rewrite rules relating one graph to another. In contrast, proof assistants rely heavily on inductive datatypes, particularly when giving semantics to embedded languages. This creates obstacles to formally reasoning about graphical languages, since imposing an inductive structure obfuscates the diagrammatic nature of graphical languages, along with their corresponding equational theories. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category-theoretic definitions. We developed VyZX to Verify the ZX-calculus, a graphical langauge for reasoning about quantum computation. The ZX-calculus comes with a collection of diagrammatic rewrite rules that preserve the graph's semantic interpretation. We show how inductive graphs in VyZX are used to prove the soundness of the ZX-calculus rewrite rules and apply them in practice using standard proof assistant techniques. We also provide an IDE-integrated visualizer for proof engineers to directly reason about diagrams in graphical form.