论文标题
vyzx：验证ZX演算的愿景
VyZX : A Vision for Verifying the ZX Calculus
论文作者
论文摘要
优化量子电路是量子计算的关键挑战。 PYZX编译器通过通过ZX微积分优化电路，这是量子电路模型的强大图形替代方案。尽管如此，它仍然无法保证其正确性。为了解决这个问题，我们开发了Vyzx，这是COQ证明助手中经过验证的ZX-Calculus。 Vyzx提供了ZX图的两个不同表示形式，以易于编程和证明：基于图形的表示图表上的高级函数和基于块的基于块的表示，用于证明ZX图等效。通过这两个不同的视图，Vyzx提供了验证ZX图的属性和转换所需的工具。本文探讨了Vyzx及其应用程序的证明和设计选择以及验证图形编程语言的挑战。
Optimizing quantum circuits is a key challenge for quantum computing. The PyZX compiler broke new ground by optimizing circuits via the ZX calculus, a powerful graphical alternative to the quantum circuit model. Still, it carries no guarantee of its correctness. To address this, we developed VyZX, a verified ZX-calculus in the Coq proof assistant. VyZX provides two distinct representations of ZX diagrams for ease of programming and proof: A graph-based representation for writing high-level functions on diagrams and a block-based representation for proving ZX diagrams equivalent. Through these two different views, VyZX provides the tools necessary to verify properties and transformations of ZX diagrams. This paper explores the proofs and design choices underlying VyZX and its application and the challenges of verifying a graphical programming language.
