💻 computer science

A Practical Specification Language for Automatic Quantum Program Verification (Technical Report)

本文提出了一种扩展的基于集合的规范语言以及一种线性复杂度的翻译算法，该算法通过避免先前基于自动机方法中固有的指数级膨胀，实现了对量子程序完全自动且可扩展的霍风格验证。

原作者： Wei-Lun Tsai, Yu-Fang Chen, Ondřej Lengál

发布于 2026-05-08

📖 1 分钟阅读☕ 轻松阅读

原作者： Wei-Lun Tsai, Yu-Fang Chen, Ondřej Lengál

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你正在试图验证一个复杂的量子计算机程序是否正确运行。在经典计算的世界里，我们有检查清单和规则来确保软件不会崩溃。而在量子计算中，这要困难得多，因为计算机的“状态”更像是概率云，而不是简单的开/关开关。

本文介绍了一种新的、实用的方法来自动检查这些量子程序，无需人类专家为每一次检查编写数千行证明。

以下是他们解决方案的分解，使用简单的类比：

问题：《巴别图书馆》式的爆炸

将量子程序的可能状态想象成一座巨大的图书馆，里面堆满了书籍。

旧方法： 以前的方法试图通过将规则转换为特定格式（称为“自动机”）来验证这些程序。然而，这种转换就像试图将图书馆里的每一本书都复制到新书架上。如果你只增加了一页（或者给计算机增加了一个“量子比特”），需要复制的书籍数量就会翻倍。
结果： 对于小型程序，这还可以。但对于一个拥有 32 个量子比特的程序（这在量子世界中实际上相当小），图书馆变得如此巨大，以至于试图验证它的计算机要么内存耗尽，要么时间不够。这就像试图一粒一粒地捡起沙滩上的每一粒沙子来数数。

解决方案：聪明的“乐高”策略

作者们创造了一种新语言和一种新的转换方法，阻止了这种爆炸。他们将量子程序视为一组独立的乐高积木，而不是一个巨大而混乱的团块。

1. 新语言（蓝图）
他们设计了一种规范语言，让工程师可以使用简单的集合和约束来描述程序应该做什么。

你不必为每一种可能性编写复杂的数学公式，而是可以说：“输出应该是‘标记’项具有高概率的状态混合。”
这就像给承包商一张蓝图，上面写着“建造一扇红门和一蓝顶的房子”，而不是列出每一块砖的坐标。

2. 转换算法（智能分类器）
这是本文的核心魔法。当他们将蓝图转换为机器可读格式（自动机）时，他们使用了一个两步“重排序”技巧：

步骤 A：按依赖关系分组（变量层级）
想象你有一堆混在一起的袜子。有些袜子属于同一双（它们是相互依赖的），而其他袜子则是随机的。旧方法试图一次性整理整堆袜子。新方法首先观察袜子，并指出：“这两只是一双，这三只是另一双，这一只落单了。”它将整堆袜子分成几个小的、独立的组。
- 这为何有帮助： 它将一个巨大且不可能完成的整理工作，变成了几个微小且容易完成的工作。
步骤 B：拆解袜子（量子比特层级）
即使在一双袜子内部，旧方法也是整只袜子一起看。新方法意识到袜子只是线的集合。它将问题进一步分解，单独查看每一根“线”（量子比特）。
- 类比： 他们不是试图一次性验证整个三维拼图，而是一次验证一个切片，然后将切片重新堆叠起来。

3. 结果：线性增长
由于这种智能的排序和切片，随着你增加更多量子比特，验证任务的大小呈线性增长（1, 2, 3, 4...），而不是指数增长（1, 2, 4, 8, 16...）。

类比： 如果旧方法就像滚下山坡的雪球，越滚越大，直到压垮城镇，那么新方法就像一个无论滚多远都保持同样大小的雪球。

他们实际取得的成就

本文并未声称能解决所有量子问题或预测量子医学的未来。他们具体声称：

速度： 他们成功地在不到一秒的时间内，将一个32 量子比特的 Grover 搜索算法（一种著名的量子算法）的规范转换为机器可读格式。
对比： 之前的最佳方法（AutoQ）甚至无法在五分钟内完成同一 32 量子比特问题的转换（它超时了）。
可扩展性： 他们验证了多达 32 个量子比特的电路（其中一些为 25-29 个量子比特），而这些电路以前无法自动验证。
自动化： 该过程是“一键式”的。一旦你用他们的新语言编写了规范，计算机就会在无需人工干预的情况下完成其余工作。

局限性（他们不做的事情）

作者们诚实地说明了局限性。他们的方法非常适合检查程序是否产生了正确的状态集合。然而，他们有意避免支持以破坏其高效系统的方式进行的“否定”（即说“这种状态必须不发生”）。他们选择保持系统的快速和自动化，即使这意味着放弃一些会使系统再次变慢的非常复杂的逻辑技巧。

总之： 他们构建了一种更聪明的方法，将量子规则转换为计算机可以检查的格式。通过将大问题分解为小的、独立的片段，他们将一项曾经需要永恒时间（或导致计算机崩溃）的任务，变成了几秒钟内就能完成的事情，从而使量子软件的自动验证在实用规模上首次成为可能。

技术摘要：一种用于自动量子程序验证的实用规范语言

1. 问题陈述

尽管过去十年在量子程序逻辑和验证框架方面取得了显著的理论进展，但理论与实践应用之间仍存在关键差距。现有方法，特别是那些基于使用厄米算符或投影的量子霍尔逻辑（QHL）的方法，往往无法支持全自动（“一键式”）验证。虽然 QHL 提供了坚实的语义基础，但指定非平凡的正确性属性通常会导致复杂的证明义务，需要在交互式定理证明器（如 Isabelle/HOL 或 Coq）中进行大量的人工努力。

另一种由 AutoQ 提出的方法，利用表示为有限自动机的基于集合的断言来实现算法验证。然而，该方法存在严重的可扩展性瓶颈：将高层、基于集合的规范转换为自动机时，其规模相对于量子比特数量呈指数级膨胀。这一限制将实际验证局限于非常小的实例，使得该方法对于更大规模的现实世界量子电路不可行。

2. 方法论

作者提出了一种新颖的框架，通过引入扩展的基于集合的规范语言和新的规范到自动机的转换算法来弥合这一差距。核心创新在于一种分治策略，该策略在自动机构建之前重新组织规范，确保生成的复杂度与量子比特数量呈线性关系。

2.1 扩展规范语言

作者定义了一种规范语言，旨在将断言（量子态的集合）描述为前置条件和后置条件。该语言具有以下特性：

模块化构建： 支持标准的集合并集（ $\cup$ ）和张量积（ $\otimes$ ），以便从更简单的组件组合出复杂的集合。
符号表示： 允许在振幅（复变量）和基态（二进制字符串变量）中使用符号变量。这使得能够紧凑地描述无限状态的集合和叠加态，而无需显式枚举（例如，使用求和符号 $\sum$ ）。
基于约束的规范： 包含关于变量实部和虚部的无量化一阶公式，以约束有效状态空间（例如， $|\alpha|^2 > 0.8$ ）。

2.2 转换算法

转换过程将这些高层规范转换为层级同步树自动机（LSTAs），这是一种适合表示量子态集合的紧凑自动机模型。该算法经过四个关键阶段：

预处理（变量边界对齐）： 对输入进行规范化以消除语法糖（展开张量幂并拆分并集）。然后，算法验证变量边界在张量段之间是否对齐，并将常数二进制字符串抽象为由等式绑定的新变量。
变量级重排序： 算法基于共享变量或不等式约束，使用依赖图分析变量槽之间的依赖关系。它将槽划分为不相交的连通分量并重新排序。这使得规范可以转换为较小且独立组件的张量积（ $S_1 \otimes S_2 \otimes \dots$ ），从而将枚举复杂度从关于变量数量的指数级降低为线性级。
量子比特级重排序： 在变量级分解的基础上，算法进一步将多量子比特变量分解为单量子比特切片。它通过量子比特间的逻辑析取来处理不等式约束（例如， $i \neq j$ ）。此阶段引入“估值相关振幅”（布尔函数）来跟踪约束的部分满足情况，有效地将复杂度降低为关于量子比特数量的线性级。
紧凑 LSTA 构建： 对于每个分解后的组件，自底向上构建紧凑的 LSTA。构建过程合并同构子树，并使用“标记振幅”机制，确保在最终张量积组装期间，仅重组源自同一源项的投影项。在最终组装 LSTA 之前，通过过滤步骤移除无效的赋值。

3. 主要贡献

线性复杂度转换： 主要贡献是一种转换算法，其复杂度与量子比特数量呈线性关系（ $O(L)$ ），这是对以往基于集合的方法中指数级膨胀的重大改进。这是通过受控的自动机构建以及对变量和量子比特的战略性重排序实现的。
扩展规范语言： 一种更具表现力的语言，支持符号变量、张量积和定量约束，允许用户直接陈述非平凡的正确性属性（例如概率保证）。
全自动验证： 生成的紧凑自动机使得对固定量子比特量子程序的全自动霍尔风格验证成为可能，其规模对于自动化工具而言此前是不可行的。

4. 实验结果

作者实现了所提出的转换框架，并将其与最先进的 AutoQ 2.0 工具进行了比较。基准测试包括 Bernstein-Vazirani (BV)、GHZ 态制备、Grover 搜索（及其迭代）以及多控制 Toffoli 门。

性能： 所提出的方法始终优于 AutoQ 2.0。例如，使用新算法转换 32 量子比特 Grover 电路的功能正确性规范耗时不到一秒，而 AutoQ 2.0 在超时（5 分钟）后仍未完成转换。
可扩展性： 新方法成功验证了多达 32 个量子比特（Grover）和 24 个量子比特（MCToffoli）的电路，而先前的方法甚至无法完成 25 个量子比特（Grover）或 12 个量子比特（GHZ）电路的转换。
验证时间： 生成的 LSTA 规模较小也显著减少了验证时间，在许多先前方法耗时数分钟或超时的案例中，新方法通常在不到一秒内完成。

5. 意义与主张

本文声称成功弥合了富有表现力的高层规范与全自动量子程序验证之间的差距。通过解决先前基于自动机方法的指数级可扩展性瓶颈，作者使得验证大规模量子电路成为可能，而这些电路此前超出了自动化工具的触及范围。

作者将其工作定位为对传统 QHL 框架的补充。虽然 QHL 提供了通用性和强大的推理原则（通常需要人工证明），但这种方法通过采用规范的外延视图（状态集合）而非内涵的、基于公式的视图，优先考虑大规模电路的可处理性和自动化。作者承认了故意的限制，例如不支持任意否定（补集），以保持基于自动机方法的紧凑性和自动化。他们认为，这种权衡对于在实践领域实现“一键式”验证是合理的，为形式化验证成为量子软件开发工作流程中可用的组成部分铺平了道路。