论文标题
Giallar：Qiskit量子编译器的按钮验证
Giallar: Push-Button Verification for the Qiskit Quantum Compiler
论文作者
论文摘要
本文介绍了Giallar，这是一种用于量子编译器的完全自动验证工具包。 Giallar不需要手动规格，不变性或证明，并且可以自动验证编译器通行证可以保留量子电路的语义。为了处理量子编译器中的无界循环，Giallar摘要三个循环模板，它们的循环不变性可以自动推断。为了有效地检查具有复杂矩阵语义表示的任意输入和输出电路的等效性，Giallar引入了量子电路的符号表示，以及一组重写规则，用于显示符号量子电路的等效性。使用Giallar，我们在13个版本的Qiskit编译器（开源量子编译器标准）中实施并验证了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.
