一句话：提出 VyZX 库，用归纳图在证明助手中形式化验证 ZX 演算的图示重写规则及其可靠性。
图形语言以图及其重写规则简洁表示计算，但证明助手常依赖归纳数据类型，给图形语言赋予归纳结构会掩盖其图示本质与等式理论，阻碍形式化推理。为此，作者提出 VyZX，一个基于归纳定义图形语言的已验证库，其归纳构造源于范畴论定义。他们以量子计算的 ZX 演算为实例，利用 VyZX 中的归纳图证明 ZX 演算图示重写规则的可靠性，并用标准证明助手技术实际应用这些规则。此外，还提供集成于 IDE 的可视化器，使证明工程师能直接以图形形式推理。这项工作为图形量子语言的形式验证提供了可复用的基础。
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 Vy ZX, a verified library for reasoning about inductively defined graphical languages. These inductive constructs arise naturally from category-theoretic definitions. We developed Vy ZX to V erify the ZX -calculus, a graphical language 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 Vy ZX 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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2311-11571,
title = {<i>Vy</i>
ZX: Formal Verification of a Graphical Quantum Language},
author = {Adrian Lehmann and Ben Caldwell and Bhakti Shah and William Spencer and Robert Rand},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {48},
number = {3},
year = {2026},
doi = {10.1145/3807780}
}