paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs

用于推理量子程序期望运行时间的量子最弱前置条件
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 1/10 · 该论文研究量子程序的最弱前置条件与期望运行时间，属于程序验证/概率程序分析方向，但用户关注的是 PL 与 AI/LLM/Agent 的交叉、浮点程序分析以及贝叶斯程序分析，量子程序验证不在这些核心方向内。引用 19 inbox
Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying
量子与概率编程程序验证
crossref: 2026-09-12dblp: 2026-09-12arxiv: 2026-09-12

AI 速览

一句话：将期望运行时间定义为量子最弱前置条件的推广，给出有限维量子程序期望运行时间计算方法并解决量子随机游走开放问题。

本文研究量子程序的期望运行时间。受概率程序期望运行时间工作的启发，作者首先把期望运行时间定义为量子最弱前置条件的一种推广，并证明量子程序的期望运行时间可表示为某个物理可观测量的期望。随后，针对有限维状态空间，提出计算量子程序期望运行时间的方法，并给出若干应用示例，包括量子伯努利工厂的期望运行时间计算。特别地，该方法解决了 Ambainis 等人 (STOC 2001) 提出的量子随机游走期望运行时间这一开放问题。

问题
如何为量子程序定义并计算期望运行时间，以便对其性能进行形式化推理，并解决量子随机游走等具体算法的期望运行时间开放问题。
方法
将期望运行时间刻画为量子最弱前置条件的推广，证明其等于某个可观测量的期望，并面向有限维状态空间开发计算方法。
评估
通过多个示例（含量子伯努利工厂）展示方法，并求解量子随机游走期望运行时间的公开问题。
原文摘要（Abstract）

We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory – a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. (STOC 2001) is solved.

链接与引用

DOI 原文 · arXiv · DBLP

BibTeX 
@inproceedings{LiuZBY22,
  title = {Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs},
  author = {Junyi Liu and Li Zhou and Gilles Barthe and Mingsheng Ying},
  booktitle = {LICS},
  year = {2022},
  doi = {10.1145/3531130.3533327}
}