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.

翻译：本文展示了量子汇编者完全自动化的核查工具Giallar。 Giallar 不需要人工规格、变量或证明,并且可以自动核实一个编译者通行证保存量子电路的语义。要处理量子汇编者中无限制的循环,Giallar 摘要的三个环状模板可以自动推断。为了有效地检查任意输入和输出电路的等同性,这些输入和输出电路具有复杂的矩阵语义代表,Giallar 引入了量子电路的象征性表示和一组重写规则以显示象征性量子电路的等同性。与Giallar 一起,我们执行并核查了13个版本的 Qiskit 编译者的44个(在56个版本中), 开源量汇编者标准, 在此期间, 3个错误在Qiskit 中被检测和确认。我们的评估表明, 大部分 Qiskit 编译者通行证可以在数数数秒数数数数数秒数数秒内自动核查, 核查只给编篡。