标题： 吉亚拉尔：Qiskit量子编译器的按键验证 显示英文标题

标题： Giallar: Push-Button Verification for the Qiskit Quantum Compiler

摘要： 本文介绍了一个名为 Giallar 的全自动量子编译器验证工具包。 Giallar 不需要手动指定规范、不变量或证明，可以自动验证编译器阶段是否保留量子电路的语义。 为了处理量子编译器中的无界循环，Giallar 抽象了三种循环模板，其循环不变量可以自动推断。 为了高效检查具有复杂矩阵语义表示的任意输入和输出电路的等价性， Giallar 引入了量子电路的符号表示以及一套用于证明符号量子电路等价性的重写规则。 使用 Giallar，我们验证了 Qiskit 编译器（开源量子编译器标准）13 个版本中的 44 个（共 56 个）编译器阶段，在此过程中，Qiskit 检测并确认了其中三个错误。 我们的评估表明，大多数 Qiskit 编译器阶段可以在几秒内自动验证，并且验证对编译性能仅施加了适度的开销。 显示英文摘要

摘要： This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically verify that a compiler pass preserves the semantics of quantum circuits. To deal with unbounded loops in quantum compilers, Giallar abstracts three loop templates, whose loop invariants can be automatically inferred. To efficiently check the equivalence of arbitrary input and output circuits that have complicated matrix semantics representation, Giallar introduces a symbolic representation for quantum circuits and a set of rewrite rules for showing the equivalence of symbolic quantum circuits. With Giallar, we implemented and verified 44 (out of 56) compiler passes in 13 versions of the Qiskit compiler, the open-source quantum compiler standard, during which three bugs were detected in and confirmed by Qiskit. Our evaluation shows that most of Qiskit compiler passes can be automatically verified in seconds and verification imposes only a modest overhead to compilation performance.