Quantum technology is advancing at an exceptional pace and holds the potential to transform numerous sectors on both national and global scales. As quantum systems become more sophisticated and widespread, ensuring their correctness becomes critically important. This highlights the pressing need for rigorous tools capable of analyzing and verifying their behavior. However, developing such verification tools poses significant challenges. Fundamental quantum phenomena—most notably superposition and entanglement—lead to program behaviors that differ radically from those in classical computing. These characteristics give rise to inherently probabilistic models and result in exponentially large state spaces, even for systems of modest complexity. In this paper, we outline initial steps toward addressing these challenges by drawing on insights gained from the verification of classical systems within our community. We then present a roadmap for designing novel verification frameworks that adapt the strengths of classical methods—such as succinct property specification, precise fault detection, automation, and scalability—to the quantum setting.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

On the Verification of Quantum Circuits (Research Challenges and Opportunities)

  • Parosh Aziz Abdulla,
  • Yo-Ga Chen,
  • Yu-Fang Chen,
  • Kai-Min Chung,
  • Lukáš Holík,
  • Ondřej Lengál,
  • Jyun-Ao Lin,
  • Fang-Yi Lo,
  • Wei-Lun Tsai

摘要

Quantum technology is advancing at an exceptional pace and holds the potential to transform numerous sectors on both national and global scales. As quantum systems become more sophisticated and widespread, ensuring their correctness becomes critically important. This highlights the pressing need for rigorous tools capable of analyzing and verifying their behavior. However, developing such verification tools poses significant challenges. Fundamental quantum phenomena—most notably superposition and entanglement—lead to program behaviors that differ radically from those in classical computing. These characteristics give rise to inherently probabilistic models and result in exponentially large state spaces, even for systems of modest complexity. In this paper, we outline initial steps toward addressing these challenges by drawing on insights gained from the verification of classical systems within our community. We then present a roadmap for designing novel verification frameworks that adapt the strengths of classical methods—such as succinct property specification, precise fault detection, automation, and scalability—to the quantum setting.