ZX演算和扩展Wolfram模型系统II：快速图解推理及其在量子电路简化中的应用
ZX-Calculus and Extended Wolfram Model Systems II: Fast Diagrammatic Reasoning with an Application to Quantum Circuit Simplification
摘要：
本文提出了一种新的算法方法进行自动化的图形演绎组合结构，使用修改后的方程定理证明技术和扩展的Wolfram模型超图重写形式主义的作者在以前的工作。我们特别关注这种新算法在量子信息论中的自动电路简化问题上的应用，使用Wolfram模型多路算子系统与ZX演算形式主义相结合，在量子比特之间的线性变换上进行快速图解推理。我们将展示如何构建一个推广的演绎推理规则的克努特-Benjunt完成方程匹配的基础上选择的因果边缘密度在相关的多路系统，然后再演示如何嵌入高阶逻辑的ZX演算规则在这个一阶方程框架。在明确展示了Wolfram模型系统和ZX演算的（超）图重写如何在这种形式主义中有效地实现之后，我们继续展示这种新算法方法的时间复杂度与证明复杂度的比较，当将随机生成的Clifford电路简化为伪范式时，以及当减少随机生成的非Clifford电路中的T门数量时，电路尺寸范围高达3000门，说明该方法与现有的电路简化框架相比表现良好，并且还表现出通过采用因果边密度优化获得的近似二次加速比。最后，我们提出了一个简单的量子隐形传态协议的正确性自动证明的工作实例，以更清楚地展示定理证明过程的内部操作。
英文摘要：
This article presents a novel algorithmic methodology for performing automated diagrammatic deductions over combinatorial structures, using a combination of modified equational theorem-proving techniques and the extended Wolfram model hypergraph rewriting formalism developed by the authors in previous work. We focus especially upon the application of this new algorithm to the problem of automated circuit simplification in quantum information theory, using Wolfram model multiway operator systems combined with the ZX-calculus formalism for enacting fast diagrammatic reasoning over linear transformations between qubits. We show how to construct a generalization of the deductive inference rules for Knuth-Bendix completion in which equation matches are selected on the basis of causal edge density in the associated multiway system, before proceeding to demonstrate how to embed the higher-order logic of the ZX-calculus rules within this first-order equational framework. After showing explicitly how the (hyper)graph rewritings of both Wolfram model systems and the ZX-calculus can be effectively realized within this formalism, we proceed to exhibit comparisons of time complexity vs. proof complexity for this new algorithmic approach when simplifying randomly-generated Clifford circuits down to pseudo-normal form, as well as when reducing the number of T-gates in randomly-generated non-Clifford circuits, with circuit sizes ranging up to 3000 gates, illustrating that the method performs favorably in comparison with existing circuit simplification frameworks, and also exhibiting the approximately quadratic speedup obtained by employing the causal edge density optimization. Finally, we present a worked example of an automated proof of correctness for a simple quantum teleportation protocol, in order to demonstrate more clearly the internal operations of the theorem-proving procedure.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
