ZX 演算与扩展 Wolfram 模型系统 II：快速图示推理及其在量子电路简化中的应用

本文提出了一种在组合结构上进行自动化图示演绎的新算法方法，该方法结合了改进的等式定理证明技术以及作者在前述工作中开发的扩展 Wolfram 模型超图重写形式体系。我们特别关注这一新算法在量子信息理论中自动化电路简化问题上的应用，利用 Wolfram 模型多路算子系统与 ZX 演算形式体系，对量子比特间线性变换实施快速图示推理。我们展示了如何构造 Knuth-Bendix 完备化演绎推理规则的一种推广，其中等式匹配是基于关联多路系统中的因果边密度来选择的，进而演示如何将 ZX 演算规则的高阶逻辑嵌入到这一阶等式框架中。在明确展示了 Wolfram 模型系统与 ZX 演算的（超）图重写均可在此形式体系中有效实现之后，我们进而给出了该新算法方法在将随机生成的 Clifford 电路简化至伪范式、以及减少随机生成的非 Clifford 电路中 T 门数量时的时复杂度与证明复杂度对比，电路规模最大达 3000 个门，表明该方法相较于现有电路简化框架表现优良，并且展示了采用因果边密度优化所获得的近似二次加速。最后，我们给出一个简单量子隐形传态协议正确性自动化证明的实例，以更清晰地展示定理证明过程的内部操作。