AI 中文总结
研究检查量子程序中多个断言的时空复杂度，揭示报告所有断言结果需线性复杂度，而检测断言失败及识别首个失败断言仅需对数复杂度，还建立了相关复杂度的格局并通过案例研究验证，为量子程序员提供设计空间。
AI 中文摘要
运行时断言是测试和调试量子程序的一种有前景的机制。与经典世界不同，检查包含多个断言的量子程序通常需要额外空间或多次运行程序。例如，在当前量子硬件上，中间电路测量受限或成本高，断言的通过/失败结果不能立即显示，而是在执行期间路由到辅助量子比特并通过终端测量读出。对于有n个断言的程序，一种朴素策略使用n个辅助量子比特来了解所有n个结果，另一种使用一个辅助量子比特但在n轮中重复程序执行，每轮检查一个断言。两者都满足S·T = O(n)。我们发现答案很大程度上取决于要学习的信息。报告所有断言的结果需要线性复杂度，但检测是否有断言失败以及识别第一个失败断言这两个部分信息任务仅需对数复杂度。此外，这些任务的检查策略可以以有用的方式进行时间和空间的权衡。在这项工作中，我们形式化了检查量子程序中多个断言的复杂度。利用这个定义，我们建立了其渐近下界和构造性上界的格局。通过对Grover算法的案例研究，我们确认了构造策略的资源成本与理论预测相符，说明了量子程序员的实际设计空间。
英文摘要
Runtime assertions are a promising mechanism for testing and debugging quantum programs. But unlike the classical world, checking a quantum program that contains multiple assertions often requires using additional space or running the program additional times. For example, on current quantum hardware where mid-circuit measurement is restricted or costly, an assertion's pass/fail outcome cannot be revealed immediately. Instead, it is routed into an ancilla qubit during execution and read out by a terminal measurement. For a program with $n$ assertions, a naive strategy uses $n$ ancillas to learn all $n$ outcomes, while an alternative uses one ancilla but repeats program execution over $n$ rounds, checking one assertion per round. Both satisfy $S \cdot T = O(n)$, where $S$ is the number of ancillas and $T$ the number of executions: a fundamental time-space trade-off. Can one do asymptotically better? We reveal that the answer depends sharply on the information to be learned. Reporting the outcomes of all assertions requires linear complexity, but two partial-information tasks of detecting whether any assertion fails, and of identifying the first failing assertion, require only logarithmic complexity -- an asymptotic improvement. Moreover, the checking strategies for these tasks can trade time for space in useful ways. In this work, we formalize the complexity of checking multiple assertions in a quantum program. Using this definition, we establish its landscape of asymptotic lower bounds and constructive upper bounds. We confirm via a case study on Grover's algorithm that the resource costs of constructed strategies match theoretical predictions, illustrating the practical design space for quantum programmers.
Comments28 pages
