计算机科学 > 编程语言
[提交于 2022年5月2日
]
标题: 吉亚拉尔:Qiskit量子编译器的按键验证
标题: Giallar: Push-Button Verification for the Qiskit Quantum Compiler
摘要: 本文介绍了一个名为 Giallar 的全自动量子编译器验证工具包。 Giallar 不需要手动指定规范、不变量或证明,可以自动验证编译器阶段是否保留量子电路的语义。 为了处理量子编译器中的无界循环,Giallar 抽象了三种循环模板,其循环不变量可以自动推断。 为了高效检查具有复杂矩阵语义表示的任意输入和输出电路的等价性, Giallar 引入了量子电路的符号表示以及一套用于证明符号量子电路等价性的重写规则。 使用 Giallar,我们验证了 Qiskit 编译器(开源量子编译器标准)13 个版本中的 44 个(共 56 个)编译器阶段,在此过程中,Qiskit 检测并确认了其中三个错误。 我们的评估表明,大多数 Qiskit 编译器阶段可以在几秒内自动验证,并且验证对编译性能仅施加了适度的开销。
文献和引用工具
与本文相关的代码,数据和媒体
alphaXiv (什么是 alphaXiv?)
CatalyzeX 代码查找器 (什么是 CatalyzeX?)
DagsHub (什么是 DagsHub?)
Gotit.pub (什么是 GotitPub?)
Hugging Face (什么是 Huggingface?)
带有代码的论文 (什么是带有代码的论文?)
ScienceCast (什么是 ScienceCast?)
演示
推荐器和搜索工具
arXivLabs:与社区合作伙伴的实验项目
arXivLabs 是一个框架,允许合作伙伴直接在我们的网站上开发和分享新的 arXiv 特性。
与 arXivLabs 合作的个人和组织都接受了我们的价值观,即开放、社区、卓越和用户数据隐私。arXiv 承诺这些价值观,并且只与遵守这些价值观的合作伙伴合作。
有一个为 arXiv 社区增加价值的项目想法吗? 了解更多关于 arXivLabs 的信息.