VyZX: Formal Verification of a Graphical Quantum Language

Each language version is independently generated for its own context, not a direct translation.

这篇文章介绍了一个名为 VyZX 的新工具，它的核心任务是用计算机证明“图形化量子语言”是绝对正确的。

为了让你轻松理解，我们可以把这篇论文的内容想象成是在解决一个**“乐高积木与说明书”**的难题。

1. 背景：量子计算的“乐高”语言

想象一下，量子计算机的运作过程非常复杂。传统的量子编程就像是在写一段极其枯燥、充满数学公式的代码（就像用纯文字描述如何搭乐高）。

而 ZX-演算（ZX-calculus） 是一种更聪明的方法。它把量子计算变成了图形：

绿色和红色的圆点（像蜘蛛一样）代表不同的量子操作。
连线代表它们之间的连接。
这种图形语言非常直观，就像乐高积木的搭建图。只要连接方式对，怎么摆放这些积木（只要不改变连接关系）都不影响最终结果。

2. 问题：图形很美，但电脑“看不懂”

虽然图形对人类来说很直观，但对计算机（特别是像 Rocq/Coq 这样的“数学证明助手”）来说，图形太“自由”了。

人类的视角：只要线连着，把积木挪个位置没关系。
电脑的视角：电脑需要严格的顺序。它必须知道哪个积木在左，哪个在右，哪个先连，哪个后连。

这就好比你想让电脑证明“把乐高积木从左边移到右边，房子还是那个房子”。但在电脑眼里，积木的位置变了，结构就变了，它很难直接理解这种“图形上的变形”。以前的工具要么太死板（强迫电脑按顺序数积木，失去了图形的灵活性），要么太随意（只画图画，没法保证数学上的绝对正确）。

3. 解决方案：VyZX —— 给图形穿上“结构化”的铠甲

作者团队开发了 VyZX，这是一个经过严格数学验证的图书馆（代码库）。

核心创新：他们发明了一种方法，把那些自由的“图形积木”转化成了电脑能理解的**“结构化积木”**（归纳定义的数据类型）。
- 这就好比给每一块乐高积木都贴上了精确的标签和编号，告诉电脑：“虽然你在图里看起来是斜着放的，但在我的结构里，你就是第 3 层第 2 个积木。”
双重验证：
1. 数学地基：他们给这些图形赋予了严格的数学含义（就像给乐高积木赋予了物理重量和受力分析）。
2. 图形规则：他们证明了所有让图形变形的规则（比如把两个红点合并成一个）在数学上都是绝对安全的。

比喻：以前我们只能凭感觉说“这两个图形长得一样，所以它们一样”。现在，VyZX 就像一位超级严谨的质检员，它拿着放大镜，一边看着图形，一边对照着背后的数学公式，大声宣布：“是的，把这两个红点合并，数学上完全等价，我向你保证！”

4. 亮点功能：让证明过程“看得见”

写数学证明通常很枯燥，满屏都是代码和符号。VyZX 做了一个很酷的功能：ZXViz。

实时可视化：当你正在用电脑写证明时，VyZX 会像实时翻译器一样，把你屏幕上复杂的代码瞬间变成漂亮的图形。
就像看漫画：你不需要去读那些深奥的公式，直接看图形怎么变形、怎么合并，就能明白证明到了哪一步。这让复杂的量子证明变得像玩拼图游戏一样直观。

5. 他们证明了什么？

作者用 VyZX 做了几件大事：

验证了所有规则：他们证明了 ZX-演算里所有的“变形规则”（比如把线绕个弯、把两个点粘在一起）在数学上都是成立的。这就像给乐高说明书盖上了“官方认证”的印章。
万能性：他们证明了，用这种图形语言，可以表示任何可能的量子计算过程（就像用乐高可以搭出世界上任何东西）。
实际应用：他们展示了如何用这个工具来优化量子电路（就像帮乐高搭出更省材料、更稳固的房子），甚至验证了量子隐形传态（Teleportation）这种高深概念。

总结

VyZX 就像是一座桥梁：

一端连接着人类直观的图形思维（像画画一样思考量子计算）。
另一端连接着计算机严谨的数学逻辑（确保每一步都绝对正确）。

它让科学家和工程师可以放心大胆地用图形来设计量子计算机，因为背后有 VyZX 这个“数学保镖”在时刻盯着，确保没有任何逻辑漏洞。这对于未来开发安全、可靠的量子软件至关重要。

Each language version is independently generated for its own context, not a direct translation.

1. 研究背景与问题 (Problem)

核心挑战：图形化语言与归纳式证明助手之间的鸿沟

图形化语言的特性：图形化语言（如 ZX 演算）通过节点和连边表示计算过程，其核心原则是“仅连接性重要”（Only Connectivity Matters, OCM）。这意味着节点的空间位置不重要，重要的是拓扑连接。这种特性使得图形化语言在量子电路优化、纠错码设计等方面非常直观且强大。
形式化验证的困境：现有的证明助手（如 Rocq/Coq）主要依赖**归纳数据类型（Inductive Datatypes）**来定义语义。
- 为了在证明助手中进行语义定义，通常需要将图形强制转化为具有严格顺序的归纳结构（例如，规定节点的左右顺序）。
- 矛盾点：这种强制的顺序化破坏了图形化语言原本的“拓扑不变性”和“仅连接性重要”的直观特性。在归纳结构中，移动节点（例如交换两个相连节点的位置）需要繁琐的证明来确保语义不变，这使得基于图形的推理变得极其困难且难以维护。
现有工具的局限：现有的图形化证明工具（如 Quantomatic）缺乏基于底层线性代数语义的严格验证，无法与更广泛的验证库（如量子电路优化器）互操作。

2. 方法论 (Methodology)

作者提出了 VyZX，这是一个在 Rocq（Coq 的继任者）中构建的、经过形式化验证的 ZX 演算库。其核心方法论包括：

A. 归纳式块结构定义 (Inductive Block Structure)

定义方式：不同于直接定义图的邻接矩阵，VyZX 将 ZX 图定义为归纳数据类型。
基本构造子：
- Spider（蜘蛛）：Z 蜘蛛（绿色）和 X 蜘蛛（红色），带有输入/输出数量和旋转角度。
- 组合操作：串联（Compose, $\leftrightarrow$ ）和并行堆叠（Stack, $\updownarrow$ ）。
- 辅助构造：Hadamard 盒、杯（Cap）、盖（Cup）、交换（Swap）等。
语义映射：定义了一个求值函数 $\llbracket \cdot \rrbracket$ ，将归纳定义的 ZX 图映射到 QuantumLib 库中的复数矩阵（$2^m \times 2^n$）。这为图形操作提供了坚实的数学基础（Ground Truth）。

B. 处理“仅连接性重要” (Handling OCM)

比例关系 (Proportionality)：由于 ZX 演算中允许非零标量因子的差异，VyZX 定义了比例关系 $\propto$ （即 $M_1 = c \cdot M_2, c \neq 0$ ）。
类型转换 (Casting)：在归纳结构中，堆叠（Stack）和串联（Compose）对维度的要求非常严格。为了处理维度不匹配（例如结合律证明中 $(A \updownarrow B) \updownarrow C$ 与 $A \updownarrow (B \updownarrow C)$ 的类型差异），作者引入了 cast 函数。该函数利用自然数相等的证明来转换图的维度类型，从而在保持严格类型安全的同时，允许在归纳结构中进行灵活的重组。

C. 视觉化工具 ZXViz

痛点：归纳定义的文本表示（如 Z n m alpha <-> ...）对于人类来说极其难以阅读，尤其是嵌套结构。
解决方案：开发了 ZXViz，一个集成在 Rocq-LSP 中的可视化插件。
- 它解析证明状态中的归纳项，并将其渲染为图形。
- 关键创新：不仅显示连接，还通过虚线框明确显示结合律结构（堆叠、串联、转换），解决了纯图形化表示中丢失的结构性信息问题。

D. 自动化与对偶性

颜色交换与转置：利用 ZX 演算的性质，实现了自动化策略（Tactics），自动证明颜色交换（Color Swap）和转置（Transpose）后的对偶定理，大幅减少了重复证明工作。
归纳证明策略：设计了针对蜘蛛节点输入/输出数量的归纳策略（如 grow_Z），允许对参数化的图结构进行归纳推理。

3. 关键贡献 (Key Contributions)

VyZX 库的构建：
- 第一个在 Rocq 中完全形式化验证的 ZX 演算库。
- 定义了基于归纳结构的 ZX 图，并证明了其语义（矩阵）的正确性。
完备等式理论的验证：
- 验证了 Jeandel 等人提出的 ZX 演算完备等式理论（Complete Equational Theory）。
- 证明了所有标准重写规则（如 Spider Fusion, Bialgebra, Hopf 规则等）的保真性（Soundness）。这意味着用户可以在不依赖底层矩阵计算的情况下，仅通过图形重写规则证明两个 ZX 图等价。
通用性证明 (Universality)：
- 证明了任意复数标量都可以表示为 ZX 图（Scalar Universality）。
- 定义了图的加法操作，证明了任意线性映射（矩阵）都可以构造为 ZX 图。
互操作性与电路转换：
- 实现了从 sqir（基于电路的验证库）到 VyZX 的转换（Ingestion）。
- 证明了电路优化（如 Peephole Optimizations）可以通过转化为 ZX 图，利用图形规则进行验证，并转换回电路。
交互式可视化环境：
- 推出了 ZXViz，解决了图形化语言在文本证明助手中的可读性瓶颈，使证明工程师能够直观地观察和调试证明状态。

4. 实验结果与应用 (Results)

论文通过多个案例展示了 VyZX 的实际能力：

贝尔态制备 (Bell State Preparation)：将标准电路转换为 ZX 图，利用图形重写规则（重结合、颜色交换、融合）简化为“盖（Cap）”结构，证明了其正确性。
CNOT 与 SWAP 等价性：证明了三个 CNOT 门组成的电路等价于 SWAP 门。证明过程完全基于图形规则（Bialgebra 和 Hopf 规则），无需矩阵计算。
量子隐形传态 (Teleportation)：展示了如何处理测量和纠错。通过引入布尔变量捕获测量结果，并在图形中利用“盖”和“杯”结构进行抵消，证明了隐形传态协议的正确性。
电路优化验证：成功验证了 Nam 等人提出的电路优化规则（Peephole optimizations），证明了 VyZX 可以替代或辅助现有的基于电路的优化器（如 voqc）。

5. 意义与影响 (Significance)

填补了验证空白：VyZX 填补了“图形化直觉”与“严格形式化验证”之间的空白。它使得量子软件开发者可以像使用纸笔一样直观地操作图形，同时拥有机器验证的数学保证。
提升证明效率：通过图形重写规则（而非繁琐的矩阵代数），大大简化了量子电路等价性证明的复杂度。
通用框架：虽然目前专注于 ZX 演算，但其基于对称幺半范畴（Symmetric Monoidal Categories）的归纳块结构设计，可以推广到其他图形化语言（如 ZH 演算、ZW 演算）甚至非量子领域（如逻辑、拓扑）。
推动可信量子软件：为构建完全可信的量子编译器、优化器和纠错码验证工具提供了坚实的基础设施。

总结

VyZX 通过创新的归纳块结构和类型转换（Cast）机制，成功解决了在证明助手中形式化验证图形化语言的难题。结合完备的等式理论验证和交互式可视化工具，VyZX 不仅证明了 ZX 演算的数学完备性，更提供了一种实用的、可互操作的框架，用于构建和验证下一代可信量子软件。