Giallar: push-button verification for the qiskit Quantum compiler
Giallar: push-button verification for the qiskit Quantum compiler
复制标题
Giallar：qiskit Quantum 编译器的按钮验证
DOI：
10.1145/3519939.3523431
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Gu, Ronghui
中科院分区：
文献类型：
--
作者：
Tao, Runzhou;Shi, Yunong;Yao, Jianan;Li, Xupeng;Javadi-Abhari, Ali;Cross, Andrew W.;Chong, Frederic T.;Gu, Ronghui
本文介绍了Gialar，量子编译器的全自动验证工具包。Gialar不需要手动规范、不变量或证明，并且可以自动验证编译器是否保留了量子电路的语义。为了处理量子编译器中的无界循环，Gialar抽象了三个循环模板，其循环不变量可以自动推断。为了有效地检验具有复杂矩阵语义表示的任意输入和输出电路的等价性，Gialar引入了量子电路的符号表示和一组表示符号量子电路等价性的重写规则.使用Gialar，我们在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.
登录
查看更多内容
通过崩溃优化对文件系统进行一键式验证
DOI：
--
发表时间：
2016
期刊：
USENIX Annual Technical Conference
影响因子：
--
作者：
Helgi Sigurbjarnarson;James Bornholt;Nicolas Christin;L. Cranor
通讯作者：
L. Cranor
跨编译器优化的黑盒等效性检查
DOI：
10.1007/978-3-319-71237-6_7
发表时间：
2017
期刊：
2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)
影响因子：
--
作者：
Manjeet Dahiya;Sorav Bansal
通讯作者：
Sorav Bansal
中心简单代数和伽罗瓦上同调：目录
影响因子：
1.5
作者：
P. Gille;Tam'as Szamuely
通讯作者：
Tam'as Szamuely
Bugs4Q：量子程序真实错误的基准
DOI：
10.1109/ase51524.2021.9678908
发表时间：
2021
期刊：
2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)
影响因子：
--
作者：
Pengzhan Zhao;Jianjun Zhao;Zhongtao Miao;Shuhan Lan
通讯作者：
Shuhan Lan
DOI：
10.1145/3453483.3454029
发表时间：
2021-04
期刊：
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
影响因子：
--
作者：
Runzhou Tao;Yunong Shi;Jianan Yao;J. Hui;F. Chong;Ronghui Gu
通讯作者：
Runzhou Tao;Yunong Shi;Jianan Yao;J. Hui;F. Chong;Ronghui Gu