💻 computer science

AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)

AutoQ 2.0 是一种先进的验证器，它通过解决与经典控制流相关的理论和工程挑战，将量子电路验证扩展至完整的量子程序，并在重复直至成功算法及基于弱测量的 Grover 搜索等复杂算法上成功证明了其高效性。

原作者： Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai

发布于 2026-05-08

📖 1 分钟阅读☕ 轻松阅读

原作者： Yu-Fang Chen, Kai-Min Chung, Min-Hsiu Hsieh, Wei-Jia Huang, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai

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

以下是论文《AutoQ 2.0：从量子电路验证到量子程序验证》的解释，已用通俗易懂的语言并辅以生动的类比进行翻译。

宏观图景：从静态蓝图到动态食谱

想象你正在建造一座房子。

AutoQ 1.0（旧版本） 就像一个只能检查静态蓝图的工具。它能验证一组固定不变的墙壁和横梁（即“量子电路”）是否建造正确。但它无法处理那种建筑师决定“如果风从北边吹来，我就加个门廊；否则，我就建个车库”的房子。
AutoQ 2.0（新版本） 是一个能检查动态食谱的工具。它理解量子程序不仅仅是静态电路；它们是可以根据过程中发生的情况做出决策（分支）和重复步骤（循环）的指令。

作者构建这个新工具，旨在验证这些复杂的、具备决策能力的量子程序是否完全按照程序员的意图运行，而无需人工逐一检查每一步。

核心挑战：“坍缩”问题

在量子世界中，有一条独特的规则：测量。
想象你有一枚正在旋转的硬币，它同时既是正面又是反面（叠加态）。一旦你观察它（测量它），它就会“坍缩”成正面或反面。

难点： 在旧工具中，一旦你测量了硬币，数学计算就会变得混乱。概率必须被“归一化”（重新计算以确保总和为 100%），这使得计算机数学变得极其缓慢且困难。
AutoQ 2.0 的妙招： 作者意识到他们不需要立即修正数学。他们决定让数字在过程中保持“混乱”（未归一化），仅检查结果的形式是否正确。他们构建了一种特殊的“蕴含测试”（一种比较工具），其逻辑是：“即使你的数字被放大或缩小，只要模式匹配，你就没问题。”这就像检查两张地图是否有相同的道路，即使一张地图是按 1:100 的比例绘制的，而另一张是按 1:1000 的比例绘制的。

引擎：“层级同步树自动机”（LSTAs）

为了处理这些复杂的程序，该工具使用了一种名为LSTAs的特殊数据结构。

类比： 将量子态想象成一棵巨大的、分叉的树。每个分支代表量子计算机可能采取的一条路径。
问题： 标准工具试图画出树上的每一片叶子。如果你有 100 个量子比特（qubits），树上的叶子数量比宇宙中的原子还多。根本不可能把它们都画出来。
解决方案（LSTAs）： LSTAs 不使用“画每一片叶子”的方法，而是使用“模板”或“模式”。它们会说：“这一层的所有分支看起来都是这样的。”
“同步”部分： 这是魔法所在。在量子程序中，如果你在树的一个部分做出决策，它会影响到该层级的整棵树。LSTAs 确保树同一“楼层”的所有分支对同一个选择达成一致。这就像一个合唱团，同一音高的人必须唱同一个音符；如果一个人唱了不同的音符，整个和声就会破裂。这使得该工具能够将巨大的量子态压缩成微小且易于管理的文件。

工作原理：三个步骤

当你想用 AutoQ 2.0 验证一个量子程序时，你就像一位正在批改学生作业的老师：

设置（前置条件）： 你告诉工具：“从一枚这样旋转的硬币开始。”（这是输入状态）。
循环（不变式）： 如果程序包含一个循环（即“重复直到”指令），你必须提供一个“循环不变式”。
- 类比： 想象一个跑步者在跑圈。你告诉工具：“无论他们跑多少圈，他们始终都在跑道上。”你不需要检查每一步；你只需要证明，如果他们在起跑时位于跑道上，那么他们跑完一圈后仍然会在跑道上。
目标（后置条件）： 你告诉工具：“程序必须以硬币显示正面结束。”

然后，该工具使用其“模式”（LSTA）在虚拟环境中运行程序以跟踪状态。它检查：

程序是否从正确的状态开始？
循环是否让跑步者保持在跑道上（不变式）？
程序结束时硬币是否显示正面？

现实世界测试：他们验证了什么？

作者在两种以前工具无法自动处理的极其困难的量子程序类型上测试了 AutoQ 2.0：

重复直到成功（RUS）：
- 场景： 想象你试图烤蛋糕，但你不知道烤箱温度是否足够。你把蛋糕放进去，检查温度，如果太冷，你就把它拿出来，等待，然后再试。你不断重复这个过程，直到蛋糕烤好。
- 结果： AutoQ 2.0 瞬间验证了这些“重试”算法。
弱测量 Grover 搜索：
- 场景： Grover 算法是一种著名的在干草堆中找针的方法。“弱测量”版本是一种棘手的新方法，你可以轻轻地窥视干草堆，而不会立即导致整个系统坍缩，从而允许你即使没有立刻找到针也能继续搜索。
- 结果： 这是一个庞大的程序。作者验证了一个包含100 个量子比特（对量子计算而言是巨大的数量）的版本，耗时约20 分钟。这是相对于以往可能性的巨大扩展。

总结

AutoQ 2.0 是一项突破，因为它是第一个能够自动验证使用循环和决策功能的复杂量子程序的工具。它通过利用智能的“模式匹配”（LSTAs）来避免陷入不可能的数学计算，并通过巧妙处理量子测量带来的混乱数学来实现这一目标。

它成功证明了这些高级量子食谱即使在非常大的系统中也能正确运行，而无需人类承担证明的重任。

技术摘要：AutoQ 2.0：从量子电路验证到量子程序验证

1. 问题陈述

量子程序通过引入分支和循环等经典控制流结构，扩展了量子电路。虽然量子电路（AutoQ 1.0 的领域）足以定义静态的门序列，但高级量子算法——例如“重复直到成功”（RUS）算法和基于弱测量的 Grover 搜索变体——需要根据从量子比特测量中获得的经典值进行动态控制。

验证这些程序带来了电路验证中不存在的重要挑战：

测量与归一化：测量会坍缩量子态并产生驱动控制流的经典值（0 或 1）。此过程通常需要对概率幅进行归一化，这使得形式化推理变得复杂。
控制流推理：验证循环和分支需要处理基于测量结果演化的状态空间，这是现有自动化工具难以完成的任务。
缺乏自动化工具：虽然存在用于经典程序的演绎验证工具（如 Dafny、KeY）以及一些量子工具（如 CoqQ、Qbricks），但它们要么缺乏完全自动化，要么需要大量人工努力（例如提供复杂的厄米算子或进行广泛的证明搜索）。现有的自动化工具通常专注于电路等价性或特定的参数化程序，缺乏对量子程序中控制流的通用支持。

2. 方法论

AutoQ 2.0 通过扩展先前的电路验证框架以支持完整的量子程序来解决这些挑战。其核心方法论依赖于层级同步树自动机（LSTAs）和一种新颖的蕴含测试方法。

2.1 形式模型：层级同步树自动机（LSTAs）

该工具使用 LSTAs 来表示量子态集合（前置条件、后置条件和循环不变式）。

结构：LSTAs 是符号树自动机，旨在将量子态编码为完美二叉树，其中分支代表计算基态，叶子代表复概率幅。
同步：LSTAs 的一个关键特征是“选择”机制。同一树层级上的转换必须共享一个共同的选择集。这使得 LSTAs 能够紧凑地表示标准树自动机无法处理的纠缠态和叠加态，通过确保仅生成有效的分支组合（即共享选择的分支）。
输入格式：用户将前置条件、后置条件和循环不变式指定为 .lsta 文件，这些文件定义了识别有效量子态集合的自动机。

2.2 验证框架

验证过程是自动化的，并遵循演绎风格：

程序执行：工具在代表前置条件的 LSTA 上执行量子门（例如 $H$ 、$CX $、$ T$）。
处理测量与分支：
- 当发生测量 $M_i = b$ 时，LSTA 被分裂为两个副本，分别对应结果 $b=0$ 和 $b=1$ 。
- 算法通过将不匹配分支的概率幅置零来更新树（例如，如果 $M_1=0$ ，则 $x_1$ 下 $1$-子树的幅值被设为 0）。
- 至关重要的是，工具在此步骤中不对幅值进行归一化。它保留原始幅值以避免执行期间的复杂算术运算，将归一化检查推迟到最终的蕴含测试中。
- 分支语句通过计算真路径和假路径的相应 LSTA 并取其并集来处理。
处理循环：
- 对于 while 循环，用户必须提供一个作为 LSTA 的循环不变式。
- 工具验证该不变式是否具有归纳性：它必须涵盖循环前可达的所有状态，并且在循环继续条件下对不变式执行循环体必须产生仍被该不变式涵盖的状态。
- 循环退出时的状态由基于循环终止条件的不变式进行超近似。
蕴含测试（至缩放）：
- 最后一步检查可达状态集合（由 LSTA $R$ 表示）是否包含在后置条件（LSTA $Q$ ）中。
- 由于在执行过程中忽略了归一化因子，工具使用一种专门的至缩放蕴含（ $|=_{uts}$ ）关系。
- 如果 $A$ 中的每棵树都是 $B$ 中某棵树的线性缩放版本（即 $T_A = r \cdot T_B$ ，其中 $r$ 为非零标量），则 $A |=_{uts} B$ 成立。
- 该检查使用图搜索算法执行，该算法逐层遍历 LSTAs，映射状态和项，并最终调用 SMT 求解器（Z3）来验证是否存在满足全局约束的缩放因子 $r$ 。

3. 主要贡献

扩展到量子程序：AutoQ 2.0 是首个为包含循环和分支的量子程序提供自动化演绎验证的工具，超越了 AutoQ 1.0 仅限于电路的范围。
自动处理测量：该工具引入了基于测量结果分裂 LSTAs 并管理由此产生的状态空间的算法，无需人工干预。
无归一化验证：通过设计一种适用于非归一化状态（至缩放）的蕴含测试，该工具避免了在执行阶段对幅值进行归一化的计算复杂性，显著提高了效率。
基于 LSTA 的不变式：该框架利用 LSTAs 来表示循环不变式，从而能够紧凑地表示迭代算法所需的复杂量子态。
可扩展性：该方法利用 LSTAs 的紧凑性和高效的 SMT 求解，支持验证具有大量量子比特的程序（在报告的基准测试中高达 100 个量子比特）。

4. 实验结果

作者在两类高级量子程序上评估了 AutoQ 2.0：

重复直到成功（RUS）算法：用于生成非标准量子门（例如特定的酉矩阵如 $(2X + \sqrt{2}Y + Z)/\sqrt{7}$ $(2 X + 2 Y + Z) / 7$ ）。
- 结果：所有 RUS 基准测试均被瞬间验证（0.0 秒）。
基于弱测量的 Grover 搜索：一种不需要预先知道解数量的 Grover 算法变体。
- 结果：该工具成功验证了多达100 个量子比特的实例（具体而言，表格中显示为 101 个量子比特），耗时约为11 秒（针对 101 量子比特情况）至20 分钟（如摘要所述针对 100 量子比特情况，尽管表格显示 101 量子比特为 11 秒；摘要可能指的是特定配置或包含了设置时间）。验证时间随量子比特和门数量的增加而合理扩展。

实验是在配备 AMD EPYC 7742 处理器和 1,152 GiB 内存的服务器上进行的。

5. 意义与主张

论文声称，AutoQ 2.0 是目前唯一能够以如此高度自动化程度验证量子程序的工具。与依赖证明助手（需要大量人力）或仅专注于电路等价性的现有工具不同，AutoQ 2.0 通过自动处理控制流和测量，弥合了形式化验证理论与实际量子编程之间的差距。

作者将该工具定位为迈向复杂量子算法形式化验证的重要一步，证明了自动化演绎验证对于无法表示为简单量子电路的程序是可行的。他们谦逊地指出，虽然当前的实现处理非嵌套控制流和纯态，但未来的工作旨在自动化不变式生成，并将支持扩展到由更复杂循环产生的混合态。