综述：《量子电路验证中形式化方法的综述》 阿伦·戈文丹库蒂（Arun Govindankutty）

《Electronics》：A Review of Formal Methods in Quantum-Circuit Verification Arun Govindankutty

　　摘要：量子计算利用量子力学的原理来进行计算。信息存储在量子比特（qubits）中，并通过一系列按电路排列的量子门进行处理。随着硬件中量子比特数量和架构复杂性的增加，验证量子电路的正确性变得至关重要。传统的测试方法和简单的模拟方法无法扩展，并且由于状态空间的指数级增长，很快就变得计算上不可行。这迫切需要更强大且可扩展的验证技术。形式化方法通过提供数学上严谨且可扩展的验证技术来解决这些可扩展性挑战，这些技术利用抽象、符号推理和概率保证来解决问题。本研究探讨了形式化方法在量子电路验证中的应用。具体而言，研究了四类形式化技术：屏障证书（barrier certificates）、抽象解释（abstract interpretation）、模型检测（model checking）和定理证明（theorem proving），以及这些技术的理论基础和实际应用。最后，研究指出了未来的研究方向和存在的挑战。文中包含了一大批参考文献，以支持进一步的研究和探索。

1. 引言
量子计算通过利用叠加、干涉和纠缠等原理，在某些问题上展现出算法优势。近年来，这一领域发展迅速[1,2,3,4,5,6]。工业界和学术界的重大贡献推动了这一进展。量子处理器正变得越来越现实，纠错技术也在稳步改进[7,8,9,10,11]。谷歌、IBM和亚马逊等大型科技公司在此过程中发挥了关键作用，他们显著改进了他们的量子硬件平台，并通过实验验证了现代量子纠错代码的有效性[12,13,14]。微软采取了不同的方法，专注于拓扑量子计算，其工作展示了具有更强鲁棒性的量子比特和门操作[15]。这些进展共同帮助量子计算超越了“噪声中等规模量子”（Noisy Intermediate Scale Quantum, NISQ）时代，朝着能够实现可靠和容错计算的量子架构迈进。随着实验平台中量子比特数量和电路深度的增加，确保实现的有效电路保持预期的语义对于研究和部署变得越来越重要。量子算法的正确执行是一个关键问题，而量子电路是描述量子算法的主要抽象方式，因此对其正确性的验证至关重要且紧迫。

验证量子系统本质上非常困难。由于量子过程的复杂性和状态空间的爆炸性增长，大多数量子过程无法在经典计算机上高效模拟。因此，随着量子比特数量的增加，许多传统验证方法无法扩展。仅凭经验测试不足以验证量子行为，因为量子系统（如叠加、纠缠和测量）的行为与经典电路不同。因此，需要替代的验证方法。形式化验证提供了一种严谨的方式来验证复杂系统，它使用数学推理和证明来确保设计的正确性。与传统测试不同，形式化验证会探索整个设计空间，而不仅仅依赖于采样行为，这使得它可以检测到测试可能遗漏的微妙边缘情况错误。由于这些强大的保证，形式化验证广泛应用于安全和可靠性要求极高的领域，包括软件系统、硬件设计和VLSI设计验证[16,17,18]。

形式化方法也被应用于量子电路验证。它们不是测试或模拟的单一替代品，而是一组互补的工具，当其建模假设和抽象明确时，可以提供强有力的保证[19,20]。

为什么选择形式化方法进行量子电路验证？有两个实际原因促使了这一选择：首先，随着量子比特数量的增加，经典测试和采样方法无法穷尽n量子比特系统的2^n维状态空间；其次，量子门的代数结构（幺正性、可逆性和线性）以及它们在许多领域的应用（例如编译器转换、纠错）允许使用形式化工具进行符号和/或代数编码。综合来看，如果验证问题用适当的抽象提出，形式化方法既相关又易于处理。

表1比较了本文讨论的四种形式化方法，包括它们的计算复杂性、自动化程度和正确性保证。表2从可扩展性、常见用例和工具支持的角度比较了不同的技术。

本研究对用于量子电路验证的形式化方法进行了简要研究，具体涵盖了四种形式化技术：屏障证书、抽象解释、模型检测和定理证明，同时探讨了这些技术的理论基础和实际应用。它系统地分析了这些技术的优点和局限性，并指出了应对日益复杂的量子系统所带来的验证挑战的前沿研究方向。除非另有说明，本文讨论的所有保证都基于所选的模型、抽象和规范，并不消除最坏情况下的指数级复杂性。

如表1和表2所示，每种方法都有自己的优势。屏障证书利用凸优化进行安全检查效率高；抽象解释提供具有可靠近似的自动分析；模型检测为有限状态模型提供完整的验证；定理证明通过机器检查的证明提供最强的保证。最佳选择取决于任务、可用资源以及所需的保证程度。以下各节将详细解释每种方法。

2. 背景
本节介绍了理解量子比特和量子电路所需的背景知识，同时介绍了用于验证的一般形式化验证技术。

2.1. 量子比特与量子电路
量子电路与经典电路有本质的不同，这种差异源于量子信息的独特性质。经典比特只能取两个确定值之一，即0或1。相比之下，量子比特可以存在于基态的叠加状态中。量子比特的状态用复数值概率振幅来描述[21,22]。单量子比特的状态表示为 |???=???|0?+???|1?（1），其中 |??? 表示量子状态。向量 |0? 和 |1? 构成计算基础，系数 ?? 和 ?? 是复数。这些系数的平方幅度决定了测量结果，即 |??|2 和 |??|2 给出了测量 |0? 和 |1? 的概率，这些概率之和必须为一，即 |??|2+|??|2=1（2）。计算基础向量定义为 |0?=[1/√2, 1/√2]（3）。类似地，n量子比特系统的状态 |??? 用2^n个复概率振幅表示，可以写为 |???=∑??∈{0,1}^n ?????|???（4），每个基态 |??? 都有一个对应的振幅 ????，测量处于状态 x 的概率为 |????|2（5），所有测量概率之和必须为一，即 ∑??∈{0,1}^n |????|2=1（6）。量子比特还可以处于纠缠状态，纠缠产生了任何经典系统都无法复制的非经典相关性。这些特性使得量子算法在某些任务上优于经典算法，但同时也给量子电路的验证带来了显著挑战。

量子电路由作用在一组量子比特上的量子门序列表示[21]，每个门对量子比特施加一个幺正变换。常见的单量子比特门包括泡利算子（X, Y, Z）、哈达玛德门（Hadamard gate）和各种相位门。多量子比特门（如CNOT门）可以在量子比特之间创建纠缠。

由于状态空间随着量子比特数量的增加而呈指数级增长，验证量子电路变得具有挑战性。一个n量子比特系统占据一个维度为2^n的希尔伯特空间（Hilbert space），这使得经典模拟对于大型电路不可行。

2.2. 形式化验证原理
如第1节所述，形式化验证涉及数学证明或反驳一个系统是否符合形式化规范。与仅检查有限输入集或执行路径的测试不同，形式化方法考虑了整个状态空间和系统的所有可能演化。这使它们能够保证每个可能的输入、时间或量子状态的正确性、安全性或合规性，而不仅仅是测试的案例。换句话说，形式化方法提供了数学上的确定性，而测试只能证明在实际检查的情景中没有错误。

形式化验证方法可以分为三大类：
1. 演绎验证：使用数学证明系统证明正确性属性。
2. 模型检测：针对时态逻辑规范验证有限状态系统。
3. 抽象解释：使用合理的语义近似分析系统行为。

在量子系统中，形式化验证面临独特的挑战，这些挑战来自叠加、纠缠、测量和退相干。经典方法必须经过仔细调整才能用于量子电路验证，并且需要在计算上保持可行性。

3. 屏障证书
本节介绍了用于验证量子电路的重要方法——屏障证书（barrier certificates）。它们源自经典动态系统理论，在那里它们用于区分安全区域和不安全区域[23]。最近的研究还发现了量子纠缠与非线性动力学之间的联系，这激发了在量子验证中使用屏障证书的兴趣[24]。

屏障证书是验证动态系统安全属性的有效方法[23]，它们保证系统轨迹永远不会达到不安全或不可取的状态。最近，屏障证书也被扩展用于量子电路的验证[23,24,26]。屏障证书使用单个实值函数捕获系统的所有可能执行路径，该函数将状态空间的安全区域与不安全区域分开。形式上，量子系统的屏障证书定义为定义在希尔伯特空间 ? 上的函数 ?? :? →?，它必须满足三个主要条件：
- 初始状态条件：?|????∈?, ??(|????)≤0（7）
- 不安全状态条件：?|????∈??, ??(|????)>0（8）
- 递减条件：?|???∈?,???∈??, ??(|???)???(|???)≤0（9）

其中 ? 是初始状态的集合，?? 是不安全状态的集合，?? 是对应于量子门的幺正变换的集合。递减条件确保 B 在电路演化过程中是非增加的，保证从 ? 开始的轨迹永远不会进入 ??。这意味着从任何初始状态开始的轨迹在任何给定时间步长内都不会进入不安全区域。这种屏障证书的存在保证了无限时间范围内的安全性。这种方法避免了显式的状态或时间枚举，从而在一定程度上缓解了状态空间爆炸问题。

量子电路可以被视为动态系统，这使得屏障证书非常适合对其进行验证。n量子比特的状态 |??? 位于 ?2^n 中，并满足归一化条件 ∑??|???|2 = 1/√(2^n)???|??? = 1。每个量子门作为幺正线性变换，在状态空间中产生一条轨迹[26]。安全性和正确性属性可以表示为振幅的多项式或半代数约束，这些包括测量概率的界限和逻辑子空间的保持。这种代数结构自然与多项式屏障证书和平方和推理相一致。

3.3. 与非线性动力学和纠缠的联系
通过将量子纠缠与非线性动力学进行比较，可以更好地理解量子系统的屏障证书[27]。混沌系统对微小变化非常敏感，高度纠缠的量子状态也显示出复杂的相关性，这使得验证更加困难。最近的研究表明，量子电路中的纠缠可以被视为一种动态不稳定性[28]。这种联系对屏障证书的合成具有重要意义：当纠缠迅速增长时，屏障函数通常需要更复杂；而低纠缠度的电路（保持稳定器结构的电路）可以使用更简单的多项式屏障。在这种视角下，屏障条件（方程（7）–（9）作用类似于量子状态空间中稳定区域和不稳定区域之间的边界，屏障函数 B 的作用类似于李雅普诺夫函数（Lyapunov function），有助于确保系统保持在安全区域内。这种联系将经典动态系统的思想引入量子验证中，并有助于根据预期的纠缠结构选择屏障函数。

3.4. 基于场景的方法
基于场景的方法是量子电路屏障证书合成的一个关键进展[24,29,30]。基于场景的合成使用有限和无限时间范围内的采样轨迹来构建屏障证书，明确考虑了初始状态和系统动态的不确定性。这些特点使其非常适合噪声量子系统，在这些系统中，通常无法准确知道所有参数。这种方法将验证问题转化为一个使用采样约束的凸优化问题，因此得到的保证是概率性的而不是绝对的。这意味着它能够保证在未见过的案例中保持用户所选择的故障级别。设计者选择一个目标违规概率??和一个置信度1 ???。然后选择场景数量N，以便合成的证书违反属性的概率最多为??，置信度至少为??。较大的N值可以降低故障概率，但会增加计算成本。具体来说，只要使用足够的独立样本，该方法可以保证至少1 ???（例如，?? =10?6）的置信度来确保正确性[29]。然而，这一保证取决于采样假设，并且可能无法检测到罕见的违规情况。该方法为量子电路验证提供了几个实际的好处：1. 支持量子系统固有的连续状态空间；2. 处理由量子噪声和设备缺陷引起的不确定性动态；3. 提供正确性的概率保证；4. 适用于有限和无限的时间范围。

3.4 应用
屏障证书已被用于验证量子系统的行为。例如，在[26]中，屏障证书的概念被扩展到复数变量，并阐明了Hadamard、相位和控制非操作等的验证。在[24]中演示了最多30个量子位的Grover搜索算法的验证。研究人员测试了各种类型的屏障证书，如多项式、指数和有理函数。这有助于确定每种应用最有效的类型。表3总结了这些屏障证书类型，突出了它们的优点、局限性和典型用例。

3.4.2 抽象解释
本节概述了如何将抽象解释应用于量子电路的形式验证。抽象解释是一种静态分析技术，它通过在抽象域中计算程序语义的合理上近似来验证程序属性[31]。在量子电路验证中，抽象解释非常有用，因为它避免了显式枚举指数级的希尔伯特空间。它不是跟踪精确的量子状态，而是对抽象表示（如投影子空间、稳定器或振幅的区间界限）进行推理[32]。量子电路由结构化的、顺序的幺正变换组成，这使它们非常适合抽象解释。这允许为每个量子门定义组合性的抽象转换器。使用抽象解释进行验证涉及定义一个抽象域和到原始状态空间的映射，实现保守地近似幺正演化的抽象门语义，并检查抽象状态上的属性。这种方法保证了正确性，并且对于特定的抽象域（例如，可达性的区间域）和属性类型（例如，鲁棒性），可以实现多项式时间可扩展性。然而，这种行为仅适用于在所选抽象域中可表达的属性。抽象压缩了量子状态，不表示完整的希尔伯特空间。因此，多项式复杂性适用于抽象操作，而不是具体状态模拟。例如，已经使用投影元组抽象来验证具有数百个量子位的基准电路上的断言，这些电路直接模拟是不可行的[32]。然而，这种可扩展性伴随着精度 trade-offs。分析可能会产生导致误报的上近似，其适用性取决于电路结构和所选的抽象。

4.1. 语义框架
抽象解释为近似计算系统语义提供了一个理论框架。它使得程序属性的静态分析成为可能[32,33,34,35,36,37]。最近的工作将这种方法扩展到了变分量子电路（VQCs）[38,39]。VQCs是许多量子机器学习算法的基础。与经典深度神经网络类似，VQCs容易受到对抗性输入的影响。输入中的微小偏差或扰动可能导致错误的输出或预测。Assolini等人[38]提出了一种基于抽象解释的语义框架来验证VQCs。他们的方法明确处理了量子特有的属性，如状态归一化。归一化在变量之间引入了依赖性，这使得传统的验证方法变得复杂。该框架提供了一种正式的方式来定义VQCs的验证问题。它还提供了分析验证过程计算复杂性的工具。

4.2. 基于区间的可达性
基于区间的可达性分析是量子电路抽象解释中的关键技术。它计算量子电路每一层的可达状态的上近似[38,40,41,42]。这种方法通过电路的各层传播区间界限，从而提供了关于电路行为的形式保证。然而，量子效应（如叠加和纠缠）会在变量之间创建依赖性。这些依赖性使得区间分析更具挑战性。为了解决这些挑战，研究人员开发了增强型的抽象技术。这些技术明确跟踪变量之间的依赖性。然而，这种额外的精度伴随着更高的计算成本[43]。在精度和效率之间找到正确的平衡仍然是量子抽象解释中的一个活跃研究问题。

4.3. 鲁棒性属性的验证
抽象解释在验证VQCs的鲁棒性属性方面非常有效。它可以用来研究不利扰动如何影响电路行为。这些技术分析输入状态中的微小变化如何影响最终测量概率。通过这种方式，它们提供了形式上的鲁棒性证书。这些证书类似于用于经典神经网络的证书[44,45,46,47,48]。验证过程通常包括四个主要步骤：1. 为输入状态定义一个扰动模型；2. 使用抽象域将这些扰动传播通过量子电路；3. 计算输出测量概率的界限；4. 检查分类决策在允许的扰动范围内是否保持稳定。这种方法已经在标准验证基准上进行了测试。结果表明它在证明量子机器学习模型的可靠性方面具有潜力[49]。这使得它对于安全关键应用尤为重要[50,51,52,53]。

5. 模型检查
模型检查是一种形式验证技术，系统地探索系统的所有可能状态。在量子电路验证中，它检查电路是否满足指定的时序逻辑属性。模型检查很有价值，因为它为有限或符号可表示的量子系统提供了完整的、基于反例的验证[54,55]。量子电路可以被建模为有限状态转换系统或量子马尔可夫链。这是通过离散化它们的演化或关注基态和测量结果来完成的。这种结构允许使用时序逻辑（包括概率扩展）来指定正确性、安全性或终止属性。这种方法已经得到了广泛的研究[56,57,58,59,60,61,62,63,64]。对于量子电路，模型检查通常包括三个主要步骤：1. 将量子电路编码为有限状态模型；2. 使用适当的时间逻辑表达所需的属性；3. 根据编码的模型检查这些属性。早期的工作通过将量子电路映射到量子马尔可夫链来验证它们。然后使用模型检查分析这些模型[55]。其他方法扩展了概率模型检查，考虑了量子测量的固有随机性和退相干[65]。

5.1. 符号技术和SMT集成
尽管模型检查在理论上具有强大的能力，但由于状态空间的指数级增长，它在量子系统中面临着严重的可扩展性问题。随着量子位数的增加，状态空间呈指数级增长。这使得穷尽状态空间的探索变得不切实际。为了解决这个状态爆炸问题，人们开发了符号模型检查技术。这些方法使用二进制决策图（BDDs）和相关的压缩策略[66,67,68,69,70,71,72]。它们在提高可扩展性方面取得了不同程度的成功。例如，基于BDD的方法已经在受控环境中验证了最多30个量子位的电路的等价性，但运行时间和内存使用量可能会迅速超出这个范围[68]。基于张量决策图的图像计算展示了针对Grover（20）等电路的可扩展性，在有利的分区策略下运行时间在几秒钟之内[73]。一个重要的最新进展是将可满足性模理论（SMT）求解器集成到量子模型检查工作流程中。现代验证框架利用SMT求解器高效地处理来自量子程序的约束。AutoQ工具[63]使用基于自动机的表示与SMT推理相结合来验证量子电路。这种混合方法实现了：1. 高效处理量子振幅的算术约束；2. 测量结果和概率的符号表示；3. 在混合量子-经典电路中与经典控制逻辑的集成；4. 为属性违规生成反例。基于SMT的模型检查在验证具有显著经典组件的量子程序（如量子纠错和混合算法中的程序）方面特别有效[35,63,74]。符号状态表示和SMT求解的结合在保持有限状态模型完整性的同时推动了可扩展性的边界。

5.2. 经典可模拟性阈值
模型检查只有在电路低于经典可模拟性阈值时才能很好地工作[75]。对于Clifford-heavy电路，稳定器方法可以使用表格方法有效地压缩状态[76]，并且模型检查的计算成本随量子位数的增加而仅呈多项式增长。对于具有许多非Clifford门的电路（高T计数或T深度），成本通常会呈指数级增长。稳定器项的数量迅速增加，压缩变得不那么有用。这一结果基于已知的经典模拟限制，应指导验证方法的选择。在某些情况下，电路被分成Clifford部分和Non-Clifford部分，分别进行符号验证和有界技术验证。即使最坏情况下的成本仍然是指数级的，这种方法在实践中也有帮助。

5.3. 工具支持和应用
已经开发了几种用于量子验证的模型检查工具。QMC（Quantum Model Checker）为量子协议提供了早期的支持[54]。AutoQ[63]实现了基于自动机的验证与SMT的集成。qMC框架[58]针对超导量子逻辑。这些工具已被用于验证量子纠错协议、通信协议和中小规模的量子算法。尽管取得了这些进展，模型检查工具仍处于原型阶段（表2）。与量子软件开发工具包的集成程度有限，工具的成熟度也各不相同。需要标准化的基准和输入格式来加速工具开发和比较。

6. 定理证明
定理证明是一种用于验证量子电路的演绎方法。在这种方法中，通过证明助手检查的形式逻辑证明来建立正确性属性[77]。由于定理证明产生机器检查的逻辑证明，因此它为所表达的属性提供了最高级别的保证。然而，这种保证是有条件的。它仅适用于开发者编码的形式模型和规范。量子电路具有丰富的代数和数学结构，如幺正算子、线性和可逆性。这些属性使它们非常适合在高阶逻辑或依赖类型理论中进行形式推理。定理证明方法通常在证明助手中形式化量子门和电路的语义。然后它们证明与规范相关的等价性、不变量或正确性定理。这种方法已在Coq、Isabelle/HOL和Lean等证明助手中实现。这些工具通常还配备了专门的量子计算库[78,79,80,81,82]。

6.1. 与SMT求解器的集成
SMT求解器已被集成到量子电路的定理证明中，以自动化证明义务。现代验证工作流程结合了交互式定理证明的表现力与SMT求解器的自动化推理能力。这种混合方法解决了纯交互式证明的可扩展性限制，同时保持了高保真度。Giallar工具[83]示例了这种方法在量子编译器验证中的应用。Giallar使用SMT求解器来验证编译器传递是否保持量子语义。验证过程包括：1. 将量子电路转换为捕获门语义的逻辑公式；2. 将编译器转换编码为输入和输出电路之间的逻辑关系；3. 使用SMT求解器检查等价性或语义保持条件；4. 当验证条件失败时生成反例。旋转抽象用于量子傅里叶变换电路的验证[74]，以及基于叠加的抽象用于量子数据编码验证[84]，阐明了使用SMT求解器的量子电路验证的符号演绎抽象方法。这些例子表明，定理证明可以为非平凡的量子算法生成经过认证的、端到端的结果。同时，交互式证明的开发往往劳动密集，并且需要仔细建模假设和界限。这使得它不太适合在量子电路设计工作流程中快速迭代。6.2. 局限性 尽管取得了这些进展，与完全自动的方法相比，定理证明仍然劳动密集。交互式证明开发需要相当的专业知识和对假设的仔细建模。SMT求解器的集成自动化了许多证明任务，但用户仍必须提供高层次的规范和证明策略。在交互式定理证明和基于SMT的自动化之间做出选择涉及保证水平、自动化和可扩展性之间的权衡。交互式证明提供了最高的保证，但随着电路规模的增加而扩展性较差。基于SMT的方法提供更大的自动化程度，但可能会忽略需要归纳推理或复杂不变量的微妙错误。结合这两种方法的混合工作流程正成为高保证量子验证的首选方法。6.3. 运行时验证 运行时验证监控量子电路的执行情况，以检查其是否满足指定的属性。虽然它不提供完整的正式保证，但可以在测试或实际操作过程中检测到属性违反。这使得运行时验证对于近期的量子应用非常实用[63,83,85,86,87,88,89,90,91]。运行时验证过程通常包括三个主要步骤：1. 为量子电路添加额外的测量操作。2. 为特定电路状态定义断言（如属性）。3. 在执行过程中对这些属性进行统计测试。运行时验证特别适用于验证量子硬件上的具体执行情况。它是分析整个量子电路设计的形式化方法的补充。7. 应用 本节介绍了量子电路验证的实际应用案例研究。7.1. 量子纠错 量子纠错（QEC）是采用形式化验证方法的关键领域。容错量子计算依赖于QEC电路的正确操作[92,93,94]。形式化方法已被用于验证QEC实现的不同方面[95,96,97,98,99]，包括：1. 稳定器测量的正确性。2. 容错阈值。3. 逻辑操作的实现。例如，屏障证书有效地确保错误保持在状态空间的可纠正区域内。模型检查用于验证QEC协议在各种故障模型下的序列行为。7.2. 编译器验证 量子电路通常用高级编程语言编写，然后编译成特定硬件的指令。这使得验证编译过程的正确性变得至关重要[37,85,87,89,100,101,102,103]。Giallar工具[83]使用SMT求解器来检查每个编译步骤是否保持了量子电路的语义完整性。这个验证过程通常包括三个主要步骤：1. 将量子电路转换为逻辑公式。2. 检查原始电路和编译后电路之间的等价性。3. 验证编译过程中应用的优化规则是否正确。对于正确性至关重要的量子应用来说，编译器验证至关重要。小的编译错误可能导致错误的结果，在安全关键的环境中（例如，量子纠错或算法电路），可能会导致算法正确性失效并引发操作故障。7.3. 量子算法 形式化方法已用于验证各种量子算法的正确性[104,105]。这些包括Grover搜索算法[106]、量子相位估计[107,108]和量子近似优化算法（QAOAs）[109]等。每种算法都有其自身的验证挑战：1. Grover算法：验证需要证明收敛性并确定成功概率的界限。2. 量子相位估计：验证涉及在不同噪声模型下确保精度保证。3. QAOA：验证侧重于近似比率和收敛属性。这些验证通常结合使用形式化技术。例如，屏障证书可用于建立安全性属性，而定理证明则确保功能正确性。因此，可以根据应用程序的不同选择每种方法的好处。最近的研究展示了在量子网络中使用结合技术的隐私保护双向数据传输[110]和半量子私有比较协议[111]。验证方法的选择通常取决于问题的类型。屏障证书或抽象解释适用于具有大规模或连续状态空间的系统。当离散状态的穷尽探索可行时，模型检查效果很好。当必须保证转换过程中的语义正确性或等价性时，可以使用定理证明或基于SMT的方法。运行时验证有助于在实际硬件执行过程中检测错误。混合方法可以结合这些技术来平衡可扩展性、自动化和形式化保证。这使得验证方法能够适应量子系统的结构和要求。如表4所示，根据每个量子计算领域的特点和挑战选择验证方法。对于量子纠错，屏障证书和模型检查特别适合。它们严格保证了所有可能错误轨迹下反馈控制稳定器电路的稳定性和正确性。屏障证书处理连续状态空间动态，而模型检查系统地探索离散综合征转换。这种组合使它们非常适合纠错的安全关键性质。表4. 形式化验证在量子计算中的应用。在量子编译器中，定理证明和SMT求解器专注于跨多个编译层的语义保持。量子门的代数和逻辑结构允许进行形式化推导。这有助于验证转换和优化是否保持了程序的语义。经常在指数级大状态空间上操作的量子算法从抽象解释和屏障证书中受益。抽象解释可以高效地检查不变量，而无需枚举所有状态。这两种方法都能实现可扩展的验证。对于量子硬件，模型检查和运行时验证效果显著。它们能够捕捉物理缺陷的离散和连续方面。模型检查系统地探索控制序列和配置。运行时验证监控实时信号以检测与预期行为的偏差。8. 挑战和局限性 本节对当前量子电路验证方法中的挑战和局限性进行了批判性评估。抽象降低了状态复杂性，但丢弃了一些具体信息。典型的损失包括振幅、相位细节以及远距离量子比特之间的相关性。如果模块之间的相互作用较弱，模块化验证效果很好，但当纠缠跨越模块边界时可能会失败。当电路具有规则结构或有限的纠缠时，符号压缩（BDDs、张量决策图）效果显著。对于高度纠缠或随机的电路，其压缩因子会降低。基于场景的方法通过抽样减少验证成本，但所需样本大小随优化变量的数量和期望的置信度而增加。因此，需要平衡??（允许的违反概率）、??（置信度）和N（样本数量）。更强的保证总是在计算、建模工作或样本数量方面带来可衡量的成本。下面列出了三个关键挑战：可扩展性、量子特定能力和工具支持。8.1. 可扩展性 量子电路验证的一个主要挑战是随着量子比特数量的线性增加，状态空间呈指数级增长。图1阐明了每种方法如何解决验证问题和管理状态爆炸的概念性比较。如图所示，模型检查使用符号压缩和决策图，而定理证明利用归纳不变量和机器检查的证明来解决指数级的状态空间增长。屏障证书不进行状态枚举，而是使用连续的分离函数，并在抽象域中使用合理的近似技术来保持可扩展性。图1. 每种形式化方法解决状态爆炸问题的概念性比较。屏障证书使用连续函数来分隔安全/不安全区域，而不进行状态枚举（蓝色曲线）。抽象解释在抽象域中使用合理的过度近似（红色框内的灰色点）。模型检查通过决策图利用符号压缩。定理证明依赖于组合推理和归纳不变量。可扩展性仍然受到经典模拟阈值的主导。1. 由Clifford门主导的电路：精确的符号压缩（稳定器形式主义、表格方法）和符号模型检查通常成功。对于由Clifford门主导的电路，验证随量子比特数量多项式级扩展。2. 高非Clifford内容：验证成本通常随着非Clifford生成器的数量（T-count、T-depth）或电路纠缠宽度的增加而呈指数级增长。实用方法采用近似方法，包括稳定器秩分解、张量网络收缩启发式和有界误差统计证书。这种区分有实证基础，并与经典模拟结果在理论上相关联。它有助于指导实践中的方法选择。当前的方法尝试使用以下方法来解决这一挑战：1. 用可扩展性交换完整性的抽象和近似技术。2. 将大型电路分解为较小组件的模块化验证。3. 用紧凑的方式表示量子状态集的符号方法。尽管采取了这些策略，验证具有许多量子比特的电路仍然很困难。这突显了进一步研究可扩展验证技术和方法的必要性。8.2. 量子特定能力 量子现象（如纠缠、叠加和测量）创造了没有经典对应物的验证挑战。这些效应在量子比特之间产生了复杂的相关性，难以在不丢失重要信息的情况下进行抽象或近似。测量和非幺正语义 一个主要的建模和验证挑战是正确处理测量和其他非幺正操作。最近开发了以下方法：1. 密度矩阵/超算子语义：将模型门和噪声通道表示为完全正迹保持（CPTP）映射??(??)[112]。这捕获了混合状态和部分迹，但增加了维度和计算成本。2. Kraus分解抽象：使用参数化Kraus集合来表示测量噪声和非幺正步骤。在抽象（合理的）域中验证属性，跟踪概率和测量后的子空间[113]。3. 关系/概率程序逻辑：采用断言是密度算子上分布或线性函数的逻辑。合理性证明关于预期的测量结果，将经典Hoare逻辑推广到量子CPTP映射[114]。每种方法都涉及表达力和易处理性之间的权衡。用于解决这些挑战的方法包括：1. 创建专门的抽象域来捕获量子相关性。2. 设计了解测量的验证技术。3. 使用关系逻辑来表示和推理纠缠。8.3. 工具支持 已经开发了许多用于量子电路验证的工具。该生态系统仍然不如经典软件验证的生态系统成熟。大多数工具需要相当的专业知识才能使用。它们通常针对特定的验证方法或量子编程语言进行定制。虽然表2根据验证方法捕捉了工具的成熟度状态，但表5捕捉了现有工具的当前状态。表5. 工具成熟度的说明性表示。评估工具的检查清单1. 输入语言兼容性：该工具是否接受主流的量子中间表示（OpenQASM、Quil、Q#等）？2. 自动化水平：每个验证目标需要多少手动工作？3. 可扩展性：已经证明了哪些量子比特数量和门深度，以及适用于哪些电路家族？4. 正理性保证：该工具是否提供机器检查的合理性（形式化证明）还是高置信度的数字证书？5. 互操作性：它能否将证明和反例导出到定理证明器或SMT求解器？这个实用的检查清单有助于读者选择合适的实现。改进工具支持需要：1. 标准化验证工具和量子编程框架之间的接口。2. 创建用户友好的接口来指定验证属性。3. 建立复杂的基准套件来评估和比较验证工具。4. 自动化为给定电路选择最合适的验证方法。9. 未来方向 本节提出了量子电路验证的关键挑战和未来研究方向。它关注实际可行性、当前限制和开放的理论问题。9.1. 混合验证方法 未来的验证框架可能会将多种技术结合成混合方法。这些方法可以利用每种方法的优势。例如，抽象解释可以快速识别潜在的问题区域。然后可以使用更精确的方法（如定理证明或模型检查）详细检查这些区域。有前景的混合组合包括：1. 将屏障证书与抽象解释一起用于安全性验证。2. 将定理证明与模型检查结合，以验证功能和时间属性。3. 用形式化方法增强运行时验证以提供实际保证。实际的混合管道应解决以下问题：1. 分解策略：一种将电路明确划分为易于处理的部分（主要是稳定器门）和包含少量非Clifford门的较难部分的方法。主要问题是这种划分是否可以自动完成，并具有已证明的大小限制。当前方法是启发式的，在困难情况下可能会失败。2. 接口语义：符号部分和数值部分必须以清晰和经过验证的方式连接。这需要一个将符号结果映射到数值工具假设的小型翻译器。在表格、稳定器形式和张量网络之间建立经过验证的链接仍然是一个未解决的问题。3. 错误累积：数值方法会累积小错误。我们需要结果来根据局部错误来限制总错误，类似于数值分析中的想法。此类保证在当前的工作中仍然有限。下面给出了针对稳定器量子纠错码（例如，表面码）的混合验证工作流程：

1. 将模型综合征提取为离散转换系统（综合征状态+综合征更新规则）。
2. 使用模型检测来验证离散综合征协议，并为可修复区域内连续错误生成屏障证书。
3. 综合结果以表明，在假设的噪声模型下，错误仍保持在逻辑可修复集合内，并且逻辑操作保持了代码的不变性。

下面提供了一种编译器验证的混合策略：

1. 用符号形式（SMT公式或中间代数形式）编码源代码和目标代码。
2. 对每次编译器遍历使用SMT/定理证明或针对受限门集（例如，Clifford+T）的自动等价性检查来证明语义保持性。
3. 当完整证明成本过高时，使用抽象解释来捕获语义违规类别，并对剩余的关键遍历采用交互式证明。

对于算法验证的混合方法包括：

1. Grover算法：使用屏障证书证明收敛性和成功率界限（以捕获迭代幅度放大），并对预言机行为进行符号推理。
2. 量子相位估计（QPE）：通过对相位反馈结构进行定理证明来建立精度界限，并通过模型检测来处理时间受限的噪声模型。
3. QAOA：使用抽象解释来限定参数扰动下的期望值，并结合特定参数选择的数值认证。

这些方法展示了如何结合多种验证方法来利用每种方法的优势，以解决不同类别的问题。

9.2. 机器学习辅助验证
机器学习（ML）为量子电路的形式化验证提供了有前景的方法。虽然ML可以加速启发式选择（包括变量排序、分组和模板度）并预测验证失败模式，但它不能替代正确性保证。因此，一个现实的研究方法可以是仅使用ML辅助来提出候选抽象；验证决策仍由所采用的可靠引擎（SMT/交互式证明）来做出。技术可行性问题包括：
1. 如何认证ML建议的不变量（例如，通过运行简短的验证检查）？
2. 如何限定ML引起的误导概率（通过统计验证和对基准集的交叉验证）？
3. 学习到的启发式是否适用于不同电路家族，或者每个新架构都需要重新训练？

潜在的应用包括：
1. 直接从模拟数据中学习屏障证书。
2. 预测哪些电路组件难以验证，以便集中验证资源。
3. 使用学习到的启发式来指导抽象解释。
4. 通过学习到的状态空间表示来加速模型检测。

初步结果表明，ML可以减少特定电路类的验证时间，但泛化能力仍然有限。未来的挑战包括开发尊重量子力学约束的ML架构，并提供启发式正确性的统计保证。

9.3. 测量和非幺正语义
量子特性如测量和非幺正操作尚未得到充分发展。重要的研究任务包括：
1. 设计适用于密度矩阵和CPTP映射的程序逻辑，并证明良好的完备性结果。目前已有相关想法，但缺乏自动化和工具支持。
2. 创建包含大量测量操作的标准化基准集，例如交互式协议、基于传输的编译器和动态电路，以便能够公平比较不同的方法。
3. 为某些噪声和测量模型证明验证复杂性的下界。这有助于设定现实的期望并指导方法选择。通过解决这些具体技术问题将取得进展，因为每个问题都可以通过形式分析和实验进行研究。

9.4. 验证容错量子计算
随着量子计算向容错操作发展，新的验证挑战和机会也随之出现。未来的研究方向包括：
1. 在现实的噪声模型下验证量子纠错协议，能够处理连续错误参数和随机行为。
2. 开发用于分布式量子系统的验证技术，涉及关于通信和纠缠分布的推理。
3. 建立量子硬件组件的认证框架，需要将物理建模与形式化验证相结合。
4. 制定量子软件验证的标准，需要社区在规范语言和保证水平上达成共识。在这些领域的进展对于构建可靠的量子计算系统至关重要。

9.5. 近期研究议程
我们强调了近期研究的关键技术问题：
1. 自动分解：将电路拆分为Clifford部分和非Clifford部分的算法，并对非Clifford部分的大小进行证明。
2. 经过验证的转换：在稳定器表格、张量网络和密度矩阵表示之间进行形式化验证的转换器。
3. 错误组合：证明验证错误在混合管线中传播的界限。
4. ML认证：为机器学习建议的验证结果提供统计保证的方法。
5. 程序逻辑自动化：为量子程序逻辑自动进行定理证明，结合SMT求解器和量子推理。

这些专注的问题为可扩展和可靠的量子电路验证提供了清晰的路径。

10. 结论
近年来，量子电路验证的形式化方法取得了显著进展。它们已经从理论框架发展成为可以应用于实际量子电路的实用工具。本研究考察了当前各种方法的现状，包括屏障证书、抽象解释、模型检测和定理证明。每种方法都提供了独特的优势，并适用于不同的验证场景。屏障证书为安全性验证提供了一种强大的方法。当与基于场景的方法结合使用时，它们可以处理初始状态和系统动态的不确定性。抽象解释为分析变分量子电路及其鲁棒性提供了语义框架。模型检测允许对时间属性进行彻底的验证。定理证明通过严谨的数学证明提供了最高级别的保证。尽管取得了这些进展，但主要挑战仍然存在。将验证扩展到更大的量子系统以及处理量子特有的特性（如纠缠、叠加和测量）仍然很困难。未来的研究应侧重于开发结合多种验证技术的混合方法，并探索使用机器学习来提高可扩展性并满足容错量子计算的验证需求。随着量子计算日益接近实际应用，形式化验证方法对于确保量子软件和硬件的可靠性和正确性将变得越来越重要。开发强大的验证工具和方法将是构建可靠和值得信赖的量子计算系统、释放其解决复杂计算问题潜力的关键。