Proof Engineering for Quantum Reasoning via E-Graphs

This dissertation is an exploration of quantum formal verification through the development of VyZX, a new formalization of the ZX-calculus. VyZX uses the categorical structure of the ZX-calculus to reason about ZX diagrams, providing a framework to establish completeness, encode common rules, and investigate applications like peephole optimization. However, working within a symmetric monoidal category introduces challenges, as the same ZX-diagram can have many equivalent representations in VyZX. This results in significant manual proof effort, as there is no single "best"; normal form, which is both tedious and difficult to fully automate. To address this, use E-Graphs, a data structure for managing equivalence classes, to streamline reasoning about equivalence. I build a system that can automatically use VyZX lemmas to prove the equivalence of two semantically equivalent diagrams if they are equal up to structure. The system performs well, solving complex associativity problems in less than a second. In benchmarks, the system is able to handle much larger problems than practical. In addition, I explore the solving of more complex equalities using custom rewrite databases. The system is able to replace and outperform Rocq’s autorewrite tactic for a common problem class in VyZX, showing its general applicability.