VyZX : Formal Verification of a Graphical Language
Date:
Presented at Midwest Programming Languages Summit (MWPLS) 2023
Abstract
Mathematical representations of graphs often resemble adjacency matrices or lists, representations that facilitate whiteboard reasoning and algorithm design. In the realm of proof assistants, inductive representations effectively define semantics for formal reasoning. This highlights a gap where algorithm design and proof assistants require a fundamentally different structure of graphs. To address this gap, we present VyZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category theory definitions. A key goal for VyZX is to verify the ZX calculus, a graphical language for reasoning about categorical quantum mechanics. Used as a more general model than the standard quantum circuit model, the ZX calculus equips its construction “ZX-diagrams” with a collection of diagrammatic rewrite rules that preserve the graph’s semantic interpretation. The ZX calculus has been shown to be useful for building quantum error correction, quantum compilers, and for general graphical reasoning. In VyZX using an initial set of rules proven through their semantics, we proceed to prove facts about the ZX calculus by only appealing to statements about the ZX calculus using standard proof assistant techniques. VyZX integrates easily with the proof engineer’s workflow through visualization, automation and verified conversion of quantum circuits to ZX diagrams.