Skip to main content
CenXiv.org
此网站处于试运行阶段,支持我们!
我们衷心感谢所有贡献者的支持。
贡献
赞助
cenxiv logo > cs > arXiv:2205.00661

帮助 | 高级搜索

计算机科学 > 编程语言

arXiv:2205.00661 (cs)
[提交于 2022年5月2日 ]

标题: 吉亚拉尔:Qiskit量子编译器的按键验证

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

Authors:Runzhou Tao, Yunong Shi, Jianan Yao, Xupeng Li, Ali Javadi-Abhari, Andrew W. Cross, Frederic T. Chong, Ronghui Gu
摘要: 本文介绍了一个名为 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.
评论: PLDI 2022; 改进了 arXiv:1908.08963
主题: 编程语言 (cs.PL) ; 量子物理 (quant-ph)
引用方式: arXiv:2205.00661 [cs.PL]
  (或者 arXiv:2205.00661v1 [cs.PL] 对于此版本)
  https://doi.org/10.48550/arXiv.2205.00661
通过 DataCite 发表的 arXiv DOI

提交历史

来自: Runzhou Tao [查看电子邮件]
[v1] 星期一, 2022 年 5 月 2 日 05:37:18 UTC (442 KB)
全文链接:

获取论文:

    查看标题为《》的 PDF
  • 查看中文 PDF
  • 查看 PDF
  • TeX 源代码
  • 其他格式
查看许可
当前浏览上下文:
quant-ph
< 上一篇   |   下一篇 >
新的 | 最近的 | 2022-05
切换浏览方式为:
cs
cs.PL

参考文献与引用

  • NASA ADS
  • 谷歌学术搜索
  • 语义学者
a 导出 BibTeX 引用 加载中...

BibTeX 格式的引用

×
数据由提供:

收藏

BibSonomy logo Reddit logo

文献和引用工具

文献资源探索 (什么是资源探索?)
连接的论文 (什么是连接的论文?)
Litmaps (什么是 Litmaps?)
scite 智能引用 (什么是智能引用?)

与本文相关的代码,数据和媒体

alphaXiv (什么是 alphaXiv?)
CatalyzeX 代码查找器 (什么是 CatalyzeX?)
DagsHub (什么是 DagsHub?)
Gotit.pub (什么是 GotitPub?)
Hugging Face (什么是 Huggingface?)
带有代码的论文 (什么是带有代码的论文?)
ScienceCast (什么是 ScienceCast?)

演示

复制 (什么是复制?)
Hugging Face Spaces (什么是 Spaces?)
TXYZ.AI (什么是 TXYZ.AI?)

推荐器和搜索工具

影响之花 (什么是影响之花?)
核心推荐器 (什么是核心?)
IArxiv 推荐器 (什么是 IArxiv?)
  • 作者
  • 地点
  • 机构
  • 主题

arXivLabs:与社区合作伙伴的实验项目

arXivLabs 是一个框架,允许合作伙伴直接在我们的网站上开发和分享新的 arXiv 特性。

与 arXivLabs 合作的个人和组织都接受了我们的价值观,即开放、社区、卓越和用户数据隐私。arXiv 承诺这些价值观,并且只与遵守这些价值观的合作伙伴合作。

有一个为 arXiv 社区增加价值的项目想法吗? 了解更多关于 arXivLabs 的信息.

这篇论文的哪些作者是支持者? | 禁用 MathJax (什么是 MathJax?)
  • 关于
  • 帮助
  • contact arXivClick here to contact arXiv 联系
  • 订阅 arXiv 邮件列表点击这里订阅 订阅
  • 版权
  • 隐私政策
  • 网络无障碍帮助
  • arXiv 运营状态
    通过...获取状态通知 email 或者 slack

京ICP备2025123034号