论文状态:已完成

Approximate Relational Reasoning for Quantum Programs

发表:2024/01/01
原文链接
价格:0.100000
已有 2 人读过
本分析由 AI 生成,可能不完全准确,请以原文为准。

TL;DR 精炼摘要

本文提出了一种证明系统,以验证量子程序的近似关系属性,解决了量子计算中的实施不完善问题。研究首次形式化验证了量子傅里叶变换的低深度近似,并验证了重复直到成功算法的近似正确性。同时开发了近似量子耦合工具,拓展了近似概率耦合的应用,回应了对投影谓词的开放问题。

摘要

Quantum computation is inevitably subject to imperfections in its implementation. These imperfections arise from various sources, including environmental noise at the hardware level and the introduction of approximate implementations by quantum algorithm designers, such as lower-depth computations. Given the significant advantage of relational logic in program reasoning and the importance of assessing the robustness of quantum programs between their ideal specifications and imperfect implementations, we design a proof system to verify the approximate relational properties of quantum programs. We demonstrate the effectiveness of our approach by providing the first formal verification of the renowned low-depth approximation of the quantum Fourier transform. Furthermore, we validate the approximate correctness of the repeat-until-success algorithm. From the technical point of view, we develop approximate quantum coupling as a fundamental tool to study approximate relational reasoning for quantum programs, a novel generalization of the widely used approximate probabilistic coupling in probabilistic programs, answering a previously posed open question for projective predicates.

思维导图

论文精读

中文精读

1. 论文基本信息

1.1. 标题

近似关系推理用于量子程序 (Approximate Relational Reasoning for Quantum Programs)

1.2. 作者

  • 彭燕 (Peng Yan)
    • 隶属机构:悉尼科技大学 (University of Technology Sydney, Sydney, Australia)
    • 联系方式:pengyan.edu@gmail.com
  • 姜涵如 (Hanru Jiang)
    • 隶属机构:北京应用数学研究院 (Beijing Institute of Mathematical Sciences and Applications, Beijing, China)
    • 联系方式:hanru@bimsa.cn
  • 于能可 (Nengkun Yu)
    • 隶属机构:石溪大学 (Stony Brook University: Stony Brook, New York, USA)
    • 联系方式:nengkunyu@gmail.com

1.3. 发表期刊/会议

未明确提及,但从“Published at (UTC)”和“Keywords”推断,通常为计算机科学领域的顶级会议或期刊,特别是编程语言或形式化方法相关。

1.4. 发表年份

2024年

1.5. 摘要

量子计算在实现过程中不可避免地会受到不完美性的影响。这些不完美性来源于多个方面,包括硬件层面的环境噪声以及量子算法设计者引入的近似实现(如低深度计算)。鉴于关系逻辑在程序推理中的显著优势,以及评估量子程序在其理想规范和不完美实现之间鲁棒性的重要性,本文设计了一个证明系统来验证量子程序的近似关系属性。通过对著名的量子傅里叶变换 (Quantum Fourier Transform, QFT) 的低深度近似进行首次形式化验证,以及对重复直到成功算法 (repeat-until-success algorithm) 的近似正确性进行验证,证明了该方法的有效性。从技术角度来看,本文开发了近似量子耦合 (approximate quantum coupling) 作为研究量子程序近似关系推理的基础工具,这是对概率程序中广泛使用的近似概率耦合 (approximate probabilistic coupling) 的一种新颖泛化,回答了之前针对投影谓词 (projective predicates) 提出的一个开放问题。

1.6. 原文链接

/files/papers/693815b632a6edc179c2e94e/paper.pdf 发布状态:已正式发表 (Published at 2024-01-01T00:00:00.000Z)

2. 整体概括

2.1. 研究背景与动机

2.1.1. 论文试图解决的核心问题

量子计算的实际实现面临着固有缺陷,包括硬件层面的环境噪声和算法设计层面的近似实现(例如,为了效率而采用的低深度电路)。这些不完美性使得“理想”的量子程序与其“实际”实现之间存在偏差。传统的程序验证方法通常关注精确的等价性或属性,但在量子领域,这种精确性往往难以达到且不切实际。因此,论文旨在解决的核心问题是:如何设计一个逻辑框架和证明系统,以形式化地推理和验证量子程序在不完美实现下的近似关系属性? 具体来说,是如何量化并证明两个量子程序(一个理想程序和一个近似实现)之间的近似等价性或更一般的近似关系。

2.1.2. 问题的重要性与现有研究空白

这个问题在当前量子计算领域至关重要,主要体现在以下几点:

  • 硬件局限性 (Hardware Limitations): 约翰·普雷斯基尔 (John Preskill) 指出,量子门中的噪声会限制可靠量子电路的规模。在噪声中等规模量子 (Noisy Intermediate-Scale Quantum, NISQ) 时代,考虑近似是必然的。精确的量子门物理实现几乎不可能。
  • 软件效率与错误 (Software Efficiency and Errors): 为了提高效率和减少错误,量子算法设计者经常采用近似计算,例如近似量子傅里叶变换 (Approximate Quantum Fourier Transform, AQFT),它通过降低电路深度来简化计算。这使得“理想”算法与“近似”算法之间存在固有差异。
  • 现有验证方法的不足 (Deficiencies in Existing Verification Methods):
    • 精确关系逻辑的局限性 (Limitations of Exact Relational Logic): 尽管现有的量子关系逻辑 (Relational Quantum Hoare Logic, RHL) 能够捕获程序间的精确关系,但在噪声或近似存在的实际场景中,精确关系往往不成立。例如,在有噪声或近似的情况下,两个量子程序的分支概率可能不同,导致精确量子耦合 (exact quantum coupling) 不存在。
    • 近似推理的空白 (Gap in Approximate Reasoning): 尽管有研究讨论了量子程序的鲁棒性 (robustness) 和近似谓词的满足性,但缺乏一个统一的、健壮的逻辑框架来有效地进行量子程序之间的近似关系推理。特别是,在现有工作中,缺乏一个关于量子版近似耦合 (approximate couplings) 的数学理论,这曾是 [8] 中提出的一个开放问题。

2.1.3. 论文的切入点或创新思路

论文的创新点在于:

  • 引入近似量子耦合 (Approximate Quantum Coupling): 针对精确量子耦合在存在噪声或近似时无法处理不同分支概率的问题,论文提出了近似量子耦合的概念。它通过参数化偏差 δ\delta 来量化两个(部分)密度算子之间的迹距离 (trace distance),从而允许处理边缘概率分布不完全匹配的情况。
  • 基于投影谓词的近似量子提升 (Approximate Quantum Lifting with Projective Predicates): 结合近似量子耦合和投影谓词 (projective predicates),定义了近似量子提升 (approximate quantum lifting)。这种方法使得近似推理变得简单而强大,并且不再要求两个量子态具有相同的迹 (trace)。
  • 设计近似量子关系霍尔逻辑 (aqRHL) (Approximate Quantum Relational Hoare Logic): 在近似量子耦合和提升的基础上,设计并构建了一个新的证明系统 aqRHL。这个系统能够推理和量化量子程序之间的近似关系,其中偏差 δ\delta 反映了近似的程度。这回答了 [8] 中提出的一个开放问题。
  • 将经典 apRHL 推广到量子领域 (Generalizing Classical apRHL to Quantum Domain): aqRHL 可以被看作是经典近似概率关系霍尔逻辑 (approximate probabilistic relational Hoare logic, apRHL) 的量子对应物,利用投影谓词作为量子版二元关系。

2.2. 核心贡献/主要发现

2.2.1. 论文最主要的贡献

  • 提出了近似量子提升 (Approximate quantum liftings) 的新概念: 这一概念基于投影谓词,使得近似推理既简单又强大。它不要求两个量子态具有相同的迹,解决了精确量子耦合可能不存在的问题。通过迹距离 (trace distance) 和金刚石范数 (diamond norm) 定义了“类 Hausdorff”距离 (Hausdorff-like distance) 作为耦合近似的度量。
  • 构建了健全的 aqRHL 提出了一种形式化的关系判断,将经典 apRHL 的思想与基于近似量子提升的新量子解释相结合。建立了一个健全的近似量子关系霍尔逻辑 (aqRHL),能够跟踪具有不同经典分支概率的两个程序的关系属性,并计算量子等价关系近似提升的适当上限。
  • 成功应用于形式化验证 (Applications in Formal Verification):
    • 首次对低深度近似量子傅里叶变换 (AQFT) 进行了形式化验证,其误差界限与 [16] 中的结果渐近等价。
    • 验证了重复直到成功算法 (repeat-until-success algorithm) 的近似正确性。
    • 在论文的完整版中还包括了酉门分解 (unitary gates decomposition) 的验证和比特翻转码 (bit flip code) 对抗单量子位错误的正确性验证。

2.2.2. 关键结论或发现

  • 通过引入近似量子耦合和提升,为量子程序的近似关系推理提供了一个坚实的理论基础。
  • aqRHL 框架能够有效地量化和推理量子程序在存在实现不完美性(如噪声或效率优化导致的近似)时的行为偏差。
  • 该方法在实际应用中具有可行性,成功解决了复杂量子算法(如 AQFT)的形式化验证问题,这在以前是难以通过精确关系逻辑实现的。
  • aqRHL 能够处理两个程序具有不同经典分支概率的场景,极大地扩展了关系逻辑在量子程序分析中的适用范围。

3. 预备知识与相关工作

3.1. 基础概念

为了理解本文提出的 aqRHL,需要对量子计算的基础、程序语义以及关系逻辑有一定了解。

3.1.1. 量子计算基础

  • 量子态空间 (State Space of a Quantum System): 量子系统的状态空间是希尔伯特空间 (Hilbert space) H\mathcal{H}
  • 纯态 (Pure State): 狄拉克符号 ψ| \psi \rangle 表示一个单位复向量,称为纯态或向量态。
  • 计算基 (Computational Basis): 单量子位系统最重要的正交基是计算基,即 {0,1}\{|0\rangle, |1\rangle\}
  • 叠加态 (Superposition): 量子程序不同于经典程序的关键特性,例如一个量子位可以处于叠加态 (0±1)/2(|0\rangle \pm |1\rangle)/\sqrt{2}
  • 算子 (Operator): 作用在 dd 维希尔伯特空间 H\mathcal{H} 上的算子表示为 d×dd \times d 矩阵。
  • 部分密度算子 (Partial Density Operator): 一个作用在 H\mathcal{H} 上的半正定 (positive semi-definite)、厄米 (Hermitian) 算子 ρ\rho,如果其迹 (trace) 满足 Tr(ρ)1\operatorname{Tr}(\rho) \leq 1,则称为部分密度算子。
  • 密度算子 (Density Operator): 如果 Tr(ρ)=1\operatorname{Tr}(\rho) = 1,则 ρ\rho 称为密度算子。部分密度算子可以表示纯态和混合量子态。
    • 纯态的密度算子: 对于纯态 ψ| \psi \rangle,其部分密度算子为 ψψ| \psi \rangle \langle \psi |,其中 ψ\langle \psi |ψ| \psi \rangle 的共轭转置 (conjugate transpose)。
    • 混合态的密度算子: 混合态是纯态 {ψi}\{ | \psi_i \rangle \} 上的经典概率分布 {pi}\{ p_i \},其部分密度算子为 ipiψiψi\sum_i p_i | \psi_i \rangle \langle \psi_i |
    • D(H)\mathcal{D}(\mathcal{H}) 表示作用在希尔伯特空间 H\mathcal{H} 上的所有部分密度算子的集合。
  • 复合系统 (Composite System): 如果 q1q_1q2q_2 是两个独立的寄存器,状态分别为 ρ1D(Hqˉ1)\rho_1 \in \mathcal{D}(\mathcal{H}_{\bar{q}_1})ρ2D(Hqˉ2)\rho_2 \in \mathcal{D}(\mathcal{H}_{\bar{q}_2}),那么复合寄存器 qˉ={qˉ1,qˉ2}\bar{q} = \{\bar{q}_1, \bar{q}_2\} 的状态是 ρ1ρ2Hqˉ=Hqˉ1Hqˉ2\rho_1 \otimes \rho_2 \in \mathcal{H}_{\bar{q}} = \mathcal{H}_{\bar{q}_1} \otimes \mathcal{H}_{\bar{q}_2}
  • 部分迹 (Partial Trace): 用于描述复合量子系统子系统的重要工具。例如,对 Hqˉ1\mathcal{H}_{\bar{q}_1} 的部分迹 Tr1()\operatorname{Tr}_1(\cdot) 是从 Hqˉ1Hqˉ2\mathcal{H}_{\bar{q}_1} \otimes \mathcal{H}_{\bar{q}_2} 中的算子到 Hqˉ2\mathcal{H}_{\bar{q}_2} 中的算子的映射。如果复合系统 qˉ\bar{q} 处于状态 ρ\rho,那么子系统 q1q_1q2q_2 分别处于状态 Tr2(ρ)\operatorname{Tr}_2(\rho)Tr1(ρ)\operatorname{Tr}_1(\rho)
  • 酉算子/酉门 (Unitary Operator/Gate): 孤立量子系统的演化由酉算子 UU 表征,满足 UU=UU=IU^\dagger U = U U^\dagger = I。例如 Pauli X, Y, Z 门、Hadamard HH 门、相位门 P(θ)P(\theta)、受控非 (Controlled-NOT, CNOT) 门、受控相位门 c.P(θ)c.P(\theta) 等。
  • 量子测量 (Quantum Measurement): 从量子系统提取信息的操作。测量 M={Mm}\mathcal{M} = \{M_m\} 由一组线性算子描述,满足 mMmMm=I\sum_m M_m^\dagger M_m = I,其中 mm 是测量结果。对纯态 ψ| \psi \rangle 进行测量 M\mathcal{M},观察到结果 mm 的概率是 pm=ψMmMmψp_m = \langle \psi | M_m M_m^\dagger | \psi \rangle,测量后状态坍缩为 Mmψ/pmM_m | \psi \rangle / \sqrt{p_m}
  • 投影 (Projection): 希尔伯特空间 H\mathcal{H} 上的线性算子 PP,满足 P2=P=PP^2 = P = P^\dagger。本文采用 [12] 和 [51, 66] 的约定,将量子谓词 (quantum predicates) 限制为希尔伯特空间或投影。
  • 支持 (Support): 对于 A=iλiψiψiA = \sum_i \lambda_i |\psi_i\rangle\langle\psi_i|,其中 ψi|\psi_i\rangleH\mathcal{H} 中的单位向量且 λi>0\lambda_i > 0,则 AA 的支持 (support) 是由 {ψi}\{|\psi_i\rangle\} 张成的空间。即 supp(A)=span{ψi}\operatorname{supp}(A) = \operatorname{span}\{|\psi_i\rangle\}
  • 满足 (Satisfaction): 一个部分密度算子 ρ\rho 满足谓词 PP (记作 ρP\rho \models P),如果 supp(ρ)P\operatorname{supp}(\rho) \subseteq P
  • 超算子 (Superoperator): 一般的量子操作,可以由引入辅助系统并丢弃测量后状态的酉变换和量子测量组合实现。超算子总是将密度矩阵映射到部分密度矩阵,并具有 Kraus 表示 (Kraus representation)。

3.1.2. 量子编程语言基础

本文使用的量子 while 语言语法和语义与 [59] 类似:

  • 语法 (Syntax): S::=skipq:=0qˉ:=U[qˉ]S1;S2if(ΩmM[qˉ]=m Sm)fiwhileM[qˉ]=1doSodS ::= \textbf{skip} | \boldsymbol{q} := |0\rangle | \bar{\boldsymbol{q}} := U[\bar{\boldsymbol{q}}] | S_1; S_2 | \textbf{if} (\boxed{\Omega m} \cdot \mathcal{M}[\bar{\boldsymbol{q}}] = m \ S_m) \textbf{fi} | \textbf{while} \mathcal{M}[\bar{\boldsymbol{q}}] = 1 \textbf{do} S \textbf{od} 其中 var(S) 表示程序 SS 中的所有变量集合,\mathcal{H}_S = \otimes_{q \in var(S)} \mathcal{H}_q 表示程序 SS 中所有量子变量的希尔伯特空间。
  • 语义 (Semantics):
    • skip: IskipI(ρ)=ρ\mathbb{I}\textbf{skip}\mathbb{I}(\rho) = \rho
    • q:=0>q := |0>: 初始化量子位 qq00|0\rangle\langle0|,其他不变。
    • q:=U[q]q := U[q]: 执行酉变换 ρUρU\rho \mapsto U\rho U^\dagger
    • S1; S2: 顺序执行。IS1;S2I(ρ)=IS2I(IS1I(ρ))\mathbb{I}S_1; S_2\mathbb{I}(\rho) = \mathbb{I}S_2\mathbb{I}(\mathbb{I}S_1\mathbb{I}(\rho))
    • if: Iif(mM[qˉ]=m Sm)fiI(ρ)=mISmI(MmρMm)\mathbb{I}\textbf{if}(\sum m \cdot \mathcal{M}[\bar{q}] = m \ S_m)\textbf{fi}\mathbb{I}(\rho) = \sum_m \mathbb{I}S_m\mathbb{I}(M_m\rho M_m^\dagger)。 如果测量结果是 mm,输入状态 ρ\rho 将以概率 pm=Tr(MmρMm)p_m = \operatorname{Tr}(M_m\rho M_m^\dagger) 坍缩为 MmρMm/pmM_m\rho M_m^\dagger / p_m,然后执行子程序 SmS_m。这里 MmρMmM_m\rho M_m^\dagger 代表对应的测量输出,概率 pmp_m 被吸收到坍缩状态中。最终输出是所有分支输出的总和。
    • while: \mathbb{I}\textbf{while} \mathcal{M}[\bar{q}] = 1 \textbf{do} S \textbf{od}\mathbb{I}(\rho) = \sum_{k=0}^\infty \mathcal{M}_0 \circ (\mathbb{I}S\mathbb{I} \circ \mathcal{M}_1)^k(\rho)。 其中 M0\mathcal{M}_0 是循环终止时的测量操作,M1\mathcal{M}_1 是循环体开始前的测量操作。kk 次展开表示循环的第 kk 次迭代。
  • 超算子性质 (Superoperator Property): 任何量子 while 程序 SS 的指称语义函数 ISI:D(H)D(H)\mathbb{I}S\mathbb{I}: \mathcal{D}(\mathcal{H}) \mapsto \mathcal{D}(\mathcal{H}) 都是一个超算子 (superoperator)。

3.1.3. 关系逻辑基础

  • 程序等价性 (Program Equivalence): 计算机科学许多领域的核心概念。
  • 关系验证 (Relational Verification): 旨在证明两个程序之间的关系属性。
  • 霍尔逻辑 (Hoare Logic): 一种形式逻辑,用于推理程序正确性。
    • 经典关系霍尔逻辑 (Relational Hoare Logic, RHL): 形式为 c1c2:ψϕ\vdash c_1 \sim c_2 : \psi \Rightarrow \phi,其中 c1,c2c_1, c_2 是程序,ψ,ϕ\psi, \phi 是关系断言 (relational assertions)。它断言对于满足前置条件 ψ\psi 的任何初始内存对 (m1,m2)(m_1, m_2),执行程序后得到的内存对 (m1,m2)(m_1', m_2') 将满足后置条件 ϕ\phi。谓词是内存上的二元关系。
    • 概率关系霍尔逻辑 (Probabilistic Relational Hoare Logic, pRHL): 将谓词提升为内存上概率分布的关系。
    • 近似概率关系霍尔逻辑 (Approximate Probabilistic Relational Hoare Logic, apRHL): 引入额外参数 α,δ\alpha, \delta 来允许对分布关系进行近似提升,形式为 c1α,δc2:ψϕc_1 \sim_{\alpha, \delta} c_2 : \psi \Rightarrow \phi,用于差分隐私 (differential privacy) 等推理。

3.2. 前人工作

3.2.1. 量子程序形式化验证 (Formal Verification of Quantum Programs)

自量子编程语言出现以来,已经有大量关于量子程序形式化验证的工作 [25, 27, 32, 44, 57, 59-62]。这些工作涵盖了从语义定义到具体验证工具的开发。

3.2.2. 精确关系逻辑用于量子程序 (Exact Relational Logic for Quantum Programs)

精确关系逻辑在量子程序分析中受到了广泛关注 [8, 33, 51]。它提供了一种更富有表现力的方法来刻画两个程序之间的关系。例如,直接验证量子程序 S1S_1S2S_2 在寄存器 qq 上的等价性,需要检查对于希尔伯特空间 Hqˉ\mathcal{H}_{\bar{q}} 中所有 ρ\rhoIS1I(ρ)\mathbb{I}S_1\mathbb{I}(\rho)IS2I(ρ)\mathbb{I}S_2\mathbb{I}(\rho) 的等价性,这涉及到对无限集合的枚举。量子关系判断能够简洁地解释这种直接枚举。

3.2.3. 量子近似推理 (Quantum Approximate Reasoning)

  • [66] 通过引入谓词的近似满足 (approximate satisfaction of predicates) 概念,讨论了量子程序的鲁棒性 (robustness)。
  • [26] 提出了一个参数化的金刚石范数 (parameterized diamond norm) 来刻画理想程序和噪声程序之间的距离。 这些工作侧重于单个程序执行的鲁棒性分析,而不是两个程序之间的关系推理。

3.3. 技术演进

3.3.1. 从经典到量子关系逻辑

关系霍尔逻辑最初为经典确定性程序而设计,随后扩展到概率程序(pRHL 和 apRHL)。在量子计算兴起后,关系逻辑也被引入到量子领域(量子 RHL)。

3.3.2. 从精确到近似推理

早期和大部分关系逻辑工作都关注程序的精确关系属性。然而,在实际的量子计算中,由于噪声、近似优化等因素,精确关系通常难以维持。这就促使研究转向近似推理。

3.3.3. 耦合理论的演变

  • 经典耦合 (Classical Coupling): 用于概率程序,将两个概率分布耦合到一个联合分布上,其边缘分布恰好是这两个分布。
  • 精确量子耦合 (Exact Quantum Coupling): [8] 将经典耦合的概念推广到密度矩阵,要求耦合的边缘分布与原始密度矩阵精确匹配。然而,这限制了其在处理具有不同分支概率的近似程序时的适用性。
  • 本文的近似量子耦合 (Approximate Quantum Coupling): 本文提出,这是对精确量子耦合的泛化,允许边缘分布之间存在一个小的偏差 δ\delta,从而能处理更广泛的近似场景,尤其是那些由于噪声或优化导致分支概率不一致的情况。这直接解决了 [8] 中提出的一个开放问题。

3.4. 差异化分析

3.4.1. 与精确量子关系霍尔逻辑的区别

  • 核心能力: 现有精确量子 RHL [8, 33, 51] 只能验证程序之间的精确关系。aqRHL 能够验证程序之间的近似关系,并量化近似的偏差 δ\delta
  • 耦合机制: 精确量子 RHL 依赖于精确量子耦合,这要求两个被比较程序的分支概率完全相同,才能找到有效的耦合。aqRHL 引入了近似量子耦合,允许两个程序在存在噪声或近似时具有不同的分支概率,从而显著扩展了适用范围。
  • 谓词的鲁棒性: aqRHL 的近似提升概念使得谓词的满足性不再是严格的布尔值,而是带有偏差 δ\delta 的。

3.4.2. 与量子鲁棒性推理工作的区别 ([26, 66])

  • 逻辑公式形式: [26, 66] 中的逻辑公式的谓词存在于单个主程序的空间中,主要关注单个程序执行的鲁棒性。本文的 aqRHL 的谓词存在于两个程序的联合空间中,能够捕获两个程序之间的关系。
  • 应用范围: [26, 66] 专注于研究量子程序的鲁棒性,即理想程序和噪声程序之间的等价性或接近程度。aqRHL 的关系霍尔逻辑选择可以推理超越等价性或接近性的更一般关系,甚至可以推理不同量子位数量的程序之间的关系。
  • 证明规则: [26, 66] 的证明规则讨论具有相同语法语句的程序。本文的单侧规则 (-L 规则) 能够跟踪不同语句的关系属性,这在结构不匹配的程序比较中非常有用。

3.4.3. 与经典 apRHL 的异同

  • 相似之处: aqRHL 在概念上是 apRHL 的量子对应物,两者都引入了参数来量化近似偏差。
  • 关键区别: aqRHLapRHL 中用于经典概率分布的二元关系推广到量子领域的投影谓词,使其适用于量子态的希尔伯特空间结构,并处理量子特有的叠加和纠缠现象。同时,量子耦合比经典概率耦合复杂得多,例如,即使是精确量子耦合,概率耦合的基本性质也不再成立 [67]。

4. 方法论

本文的核心是设计一个证明系统,用于验证量子程序的近似关系属性。这主要通过引入近似量子耦合和近似量子提升的概念,并在此基础上构建近似量子关系霍尔逻辑 (aqRHL) 来实现。

4.1. 近似量子耦合与提升

4.1.1. 迹距离 (Trace Distance)

在经典设置中,两个离散分布 μ1\mu_1μ2\mu_2 在集合 A1A_1A2A_2 上耦合当且仅当联合分布 μ\muA1×A2A_1 \times A_2 上的第一个和第二个边缘分布 (marginals) 分别精确地是 μ1\mu_1μ2\mu_2。这一概念推广到密度矩阵的精确量子耦合 [8]。 但在量子程序中,由于噪声或近似,两个量子程序的测量通常会产生不同的概率分布,导致精确量子耦合不存在。因此,论文引入了迹距离 (trace distance) 作为衡量两个(部分)量子态差异的常用度量。

定义 4 (迹距离) 两个部分密度算子 ρ\rhoσ\sigma 的迹距离 D(ρ,σ)D(\rho, \sigma) 定义为: D(ρ,σ)12Trρσ D(\rho, \sigma) \equiv \frac{1}{2} \operatorname{Tr} |\rho - \sigma| 其中,对于任何算子 AAA=AA|A| = \sqrt{A^\dagger A},即 AAA^\dagger A 的正平方根。

4.1.2. 近似量子耦合 (Approximate Quantum Coupling)

由于精确量子耦合在面对不同概率分布时会失效,本文提出了参数化偏差 δ\delta 的近似量子耦合。

定义 5 (近似量子耦合)ρ1D(H1)\rho_1 \in \mathcal{D}(\mathcal{H}_1)ρ2D(H2)\rho_2 \in \mathcal{D}(\mathcal{H}_2),则 ρD(H1H2)\rho \in \mathcal{D}(\mathcal{H}_1 \otimes \mathcal{H}_2)ρ1,ρ2\langle \rho_1, \rho_2 \rangleδ\delta-耦合 ( δ\delta-coupling ) 如果: D(ρ1,Tr2(ρ))δD(ρ2,Tr1(ρ))δ D(\rho_1, \operatorname{Tr}_2(\rho)) \leq \delta \qquad D(\rho_2, \operatorname{Tr}_1(\rho)) \leq \delta 其中:

  • ρ1,ρ2\rho_1, \rho_2 分别是两个希尔伯特空间 H1,H2\mathcal{H}_1, \mathcal{H}_2 中的部分密度算子。

  • ρ\rho 是定义在复合希尔伯特空间 H1H2\mathcal{H}_1 \otimes \mathcal{H}_2 上的部分密度算子,充当“耦合”状态。

  • Tr2(ρ)\operatorname{Tr}_2(\rho)ρ\rho 对第二个子系统(对应 H2\mathcal{H}_2)求部分迹后得到的算子,其结果是定义在 H1\mathcal{H}_1 上的算子,可以近似看作是 ρ1\rho_1 的“边缘分布”。

  • Tr1(ρ)\operatorname{Tr}_1(\rho)ρ\rho 对第一个子系统(对应 H1\mathcal{H}_1)求部分迹后得到的算子,其结果是定义在 H2\mathcal{H}_2 上的算子,可以近似看作是 ρ2\rho_2 的“边缘分布”。

  • δ\delta 是一个非负实数,表示近似的偏差上限。

    如果 δ=0\delta = 0,近似量子耦合退化为精确量子耦合。

4.1.3. 近似量子提升 (Approximate Quantum Lifting)

近似量子耦合引出了通过近似提升来表示投影谓词的近似语义。

定义 6 (近似量子提升)ρ1D(H1)\rho_1 \in \mathcal{D}(\mathcal{H}_1)ρ2D(H2)\rho_2 \in \mathcal{D}(\mathcal{H}_2),设 PP 是一个投影到 H1H2\mathcal{H}_1 \otimes \mathcal{H}_2 的闭子空间上的投影算子。那么 ρD(H1H2)\rho \in \mathcal{D}(\mathcal{H}_1 \otimes \mathcal{H}_2) 被称为 ρ1Pδρ2\rho_1 \sim_P^\delta \rho_2 的一个见证 (witness),如果:

  1. ρ\rhoρ1,ρ2\langle \rho_1, \rho_2 \rangle 的一个 δ\delta-耦合;

  2. supp(ρ)P\operatorname{supp}(\rho) \subseteq P (即 Pρ=ρP\rho = \rho)。

    其中 δ\delta 是与精确量子提升的偏差。 一个有效的近似量子提升意味着存在一个满足量子谓词的近似量子耦合。当 δ=0\delta = 0 时,近似提升 ρ1Pδρ2\rho_1 \sim_P^\delta \rho_2 退化为精确提升 ρ1Pρ2\rho_1 \sim_P \rho_2

4.1.4. 量子等价性 (Quantum Equivalence)

最重要的量子谓词之一是两个寄存器之间的等价关系。

定义 7 (等价性) 设寄存器 pˉ\bar{p}qˉ\bar{q} 是两个大小相同的、不相交的寄存器。在 (pˉ,qˉ)(\bar{p}, \bar{q}) 上的量子等价谓词 (quantum equivalence predicate),记作 (pˉ,qˉ)\equiv_{(\bar{p}, \bar{q})},是投影算子: (IpˉIqˉ+SWAP)/2 (I_{\bar{p}} \otimes I_{\bar{q}} + \mathrm{SWAP}) / 2 作用在子空间 HpˉHqˉ\mathcal{H}_{\bar{p}} \otimes \mathcal{H}_{\bar{q}} 上。其中 SWAP\mathrm{SWAP} 是定义在 (pˉ,qˉ)(\bar{p}, \bar{q}) 上的交换算子,使得对于任何 ψHpˉ| \psi \rangle \in \mathcal{H}_{\bar{p}}φHqˉ| \varphi \rangle \in \mathcal{H}_{\bar{q}}SWAPψφ=φψ\mathrm{SWAP} | \psi \rangle | \varphi \rangle = | \varphi \rangle | \psi \rangle

这一投影算子代表了对应的对称空间。例如,对于 +=(0+1)/2|+\rangle = (|0\rangle + |1\rangle)/\sqrt{2},有 (I+SWAP)(++)/2=++(I+\mathrm{SWAP}) (|+\rangle \otimes |+\rangle)/2 = |+\rangle \otimes |+\rangle。 以下引理说明了关于 \equiv 的近似提升有效地编码了两个部分密度矩阵的迹距离。

引理 2 对于任何 ρ1,ρ2\rho_1, \rho_2,我们有 ρ1δρ2D(ρ1,ρ2)2δ\rho_1 \sim_\equiv^\delta \rho_2 \Leftrightarrow D(\rho_1, \rho_2) \leq 2\delta。特别地,如果 δ=0\delta=0,我们有 ρ1ρ2ρ1=ρ2\rho_1 \sim_\equiv \rho_2 \Leftrightarrow \rho_1 = \rho_2

4.1.5. 近似上限的衡量 (Upper Bound of Approximation)

近似通常出现在我们使用一个理想的后置条件来近似一个精确的后置条件时。形式上,设 (A, B) 是希尔伯特空间 H1H2\mathcal{H}_1 \otimes \mathcal{H}_2 上的两个投影算子。 ρ1,ρ2,ρ1Aρ2ρ1Bδρ2 \forall \rho_1, \rho_2, \rho_1 \sim_A \rho_2 \Rightarrow \rho_1 \sim_B^\delta \rho_2 这个推断展示了引入近似推理的一般方式。即,给定精确提升 ρ1Aρ2\rho_1 \sim_A \rho_2 的见证,是否存在近似提升 ρ1Bδρ2\rho_1 \sim_B^\delta \rho_2 的见证 σ\sigma? 方程 (1) 中的最优偏差 δ\delta 等价于以下量: δ=d(A,B)=supρAinfσBmax{D(Tr1(ρ),Tr1(σ)),D(Tr2(ρ),Tr2(σ))} \delta = d(A, B) = \operatorname{sup}_{\rho \models A} \operatorname{inf}_{\sigma \models B} \operatorname{max} \{ D(\operatorname{Tr}_1(\rho), \operatorname{Tr}_1(\sigma)), D(\operatorname{Tr}_2(\rho), \operatorname{Tr}_2(\sigma)) \} 其中 d(A, B) 可以通过 [66] 中引入的 supρAinfσBD(ρ,σ)\operatorname{sup}_{\rho \in A} \operatorname{inf}_{\sigma \in B} D(\rho, \sigma) 进行上界限制。

本文讨论了一个重要情况:A = (U_1 \otimes U_2) B (U_1 \otimes U_2)^\daggerBB 是量子等价谓词 \equiv。那么方程 (1) 可以表示为: ρ1,ρ2,ρ1ρ2U1ρ1U1AU2ρ2U2U1ρ1U1δU2ρ2U2 \forall \rho_1, \rho_2, \rho_1 \sim_\equiv \rho_2 \Rightarrow U_1 \rho_1 U_1^\dagger \sim_A U_2 \rho_2 U_2^\dagger \Rightarrow U_1 \rho_1 U_1^\dagger \sim_\equiv^\delta U_2 \rho_2 U_2^\dagger 其中 δ\delta 可以通过金刚石范数 (diamond norm) U1U1U2U2\lVert U_1 \cdot U_1^\dagger - U_2 \cdot U_2^\dagger \rVert_\diamond 进行上界限制。金刚石范数由 Kitaev [2] 提出,通过引入辅助量子位,利用量子纠缠的力量,能更好地区分两个超算子。

定义 8 (金刚石范数)A:L(H)L(H)\mathcal{A}: \mathcal{L}(\mathcal{H}) \mapsto \mathcal{L}(\mathcal{H}),其中 L(H)\mathcal{L}(\mathcal{H}) 表示 H\mathcal{H} 的矩阵空间: AmaxρD(HH)12Tr(AIH)(ρ) \|\mathcal{A}\|_\diamond \equiv \operatorname{max}_{\rho \in \mathcal{D}(\mathcal{H} \otimes \mathcal{H}')} \frac{1}{2} \operatorname{Tr} |(\mathcal{A} \otimes I_{\mathcal{H}'})(\rho)| 其中 H\mathcal{H}' 表示 H\mathcal{H} 的一个副本。因子 1/21/2 是为了与迹距离保持一致。

对于任何 σD(H)\sigma \in \mathcal{D}(\mathcal{H}) 的超算子 E1,E2\mathcal{E}_1, \mathcal{E}_2,有 D(E1(σ),E2(σ))E1E2D(\mathcal{E}_1(\sigma), \mathcal{E}_2(\sigma)) \leq \|\mathcal{E}_1 - \mathcal{E}_2\|_\diamond。 两个酉算子 U1U_1U2U_2 之间的距离为: U1U1U2U2={sinα/2α<π1απ \|U_1 \cdot U_1^\dagger - U_2 \cdot U_2^\dagger\|_\diamond = \begin{cases} \sin \alpha / 2 & \alpha < \pi \\ 1 & \alpha \geq \pi \end{cases} 其中 α\alpha 是包含 U1U2U_1^\dagger U_2 谱的最小弧长 [37]。

4.2. 近似关系逻辑 (Approximate Relational Logic, aqRHL)

4.2.1. 判断和有效性 (Judgment and Validity)

aqRHL 的判断形式为 S1δS2:ABS_1 \sim_\delta S_2 : A \Rightarrow B,其中 S1S_1S2S_2 是量子程序,AABB 是定义在 Hqˉ1Hqˉ2\mathcal{H}_{\bar{q}_1} \otimes \mathcal{H}_{\bar{q}_2} 子空间上的投影算子(谓词),qˉi\bar{q}_i 包含 SiS_i 的所有自由变量。δ[0,1/2]\delta \in [0, 1/2] 是与精确量子提升的偏差。

定义 9 (有效性) 近似关系判断 S1δS2:ABS_1 \sim_\delta S_2 : A \Rightarrow B 是有效的,记作 S1δS2:AB\vdash S_1 \sim_\delta S_2 : A \Rightarrow B,当且仅当: ρ1,ρ2.ρ1Aρ2IS1I(ρ1)BδIS2I(ρ2) \forall \rho_1, \rho_2. \rho_1 \sim_A \rho_2 \Rightarrow \mathbb{I}S_1\mathbb{I}(\rho_1) \sim_B^\delta \mathbb{I}S_2\mathbb{I}(\rho_2) 其中 AABB 是投影算子。如果偏差 δ\delta 等于零,为简洁起见可以省略。

该定义选择了在两个程序的联合系统上使用投影谓词,因为它们是二元关系(apRHL 中使用)的量子对应物。当 δ=0\delta = 0 时,该定义退化为 [8] 中的判断。

引理 3 (程序等价性) 程序 S1S_1 等价于程序 S2S_2 当且仅当 S1S2:\models S_1 \sim S_2 : \equiv \Rightarrow \equiv

4.2.2. 证明规则 (Proof Rules)

4.2.2.1. 简单规则 (Simple Rules)

图 2 展示了基本语句和顺序结构的双边/单边证明规则。

Fig. 2. Simple aqRHL rules.

规则解释:

  • [SKIP]: skip 语句不改变状态,因此偏差为 0。如果输入满足 AA,输出也满足 AAskip0skip:AA[SKIP] \frac{}{ \vdash \textbf{skip} \sim_0 \textbf{skip} : A \Rightarrow A } \quad \textbf{[SKIP]}
  • [INIT]: 初始化操作 q:=0q := |0\rangle 将量子位 qq 置于 00|0\rangle\langle0| 状态,并保持其他量子位不变。 q1:=00q2:=0:Aproj(A0(q1,q2))[INIT] \frac{}{ \vdash q_1 := |0\rangle \sim_0 q_2 := |0\rangle : A \Rightarrow \operatorname{proj}(A_0 \otimes \equiv_{(q_1, q_2)}) } \quad \textbf{[INIT]} 其中 A0A_0 是将 AAq1,q2q_1, q_2 部分替换为 00|0\rangle\langle0| 后的谓词。
  • [UT] (Unitary Transformation): 酉变换 U[qˉ]U[\bar{q}] 将状态 ρ\rho 变为 UρUU\rho U^\dagger。如果输入满足 AA,输出将满足 (U1U2)A(U1U2)(U_1 \otimes U_2) A (U_1^\dagger \otimes U_2^\dagger)qˉ1:=U1[qˉ1]0qˉ2:=U2[qˉ2]:A(U1U2)A(U1U2)[UT] \frac{}{ \vdash \bar{q}_1 := U_1[\bar{q}_1] \sim_0 \bar{q}_2 := U_2[\bar{q}_2] : A \Rightarrow (U_1 \otimes U_2) A (U_1^\dagger \otimes U_2^\dagger) } \quad \textbf{[UT]} 规则 [UT] 提供了最强的后置条件。
  • [SEQ] (Sequence): 顺序执行的偏差是各个步骤偏差的总和,这直接来源于迹距离的三角不等式 (triangle inequality)。 S1δ1S2:ABS1δ2S2:BCS1;S1δ1+δ2S2;S2:AC[SEQ] \frac{ \vdash S_1 \sim_{\delta_1} S_2 : A \Rightarrow B \quad \vdash S'_1 \sim_{\delta_2} S'_2 : B \Rightarrow C }{ \vdash S_1; S'_1 \sim_{\delta_1 + \delta_2} S_2; S'_2 : A \Rightarrow C } \quad \textbf{[SEQ]}
  • [UT-L] (Unitary Transformation - Left): 单边规则,仅左侧程序执行酉变换,右侧为 skipqˉ1:=U1[qˉ1]0skip:A(U1I)A(U1I)[UT-L] \frac{}{ \vdash \bar{q}_1 := U_1[\bar{q}_1] \sim_0 \textbf{skip} : A \Rightarrow (U_1 \otimes I) A (U_1^\dagger \otimes I) } \quad \textbf{[UT-L]}
  • [SkIP-L] (Skip - Left): 左侧 skip,右侧任意程序。 skipδS2:ABS1δS2:AB[SKIP-L] \frac{ \vdash \textbf{skip} \sim_{\delta} S_2 : A \Rightarrow B }{ \vdash S_1 \sim_{\delta} S_2 : A \Rightarrow B } \quad \textbf{[SKIP-L]} 这里有一个排版错误,原图中的 [SkIP-L] 规则应该是: skip0S2:AA[SKIP-L] \frac{}{ \vdash \textbf{skip} \sim_0 S_2 : A \Rightarrow A } \quad \textbf{[SKIP-L]} 或者更通用的形式: skip0S2:Aproj(A)[SKIP-L] \frac{}{ \vdash \textbf{skip} \sim_0 S_2 : A \Rightarrow \operatorname{proj}(A) } \quad \textbf{[SKIP-L]} 在图2中,[SKIP-L] 规则似乎是表达 S1S_1skipS2S_2 任意程序,但其结论是 AAA \Rightarrow Aδ=0\delta=0,这与右侧 S2S_2 任意程序且可能有偏差不符。考虑到上下文和 aqRHL 的设计,如果左侧是 skip 而右侧是任意 S2S_2,那么需要一个更复杂的规则来处理 S2S_2 可能带来的偏差。更合理的解释是,图中的 [SKIP-L] 可能指“如果 S1S_1skip,则其对 AA 的影响是 0 偏差地保持 AA”。

4.2.2.2. 等价关系规则 (Rules for Equivalence Relation)

图 3 关注前置条件和后置条件都是定义在等价谓词 \equiv 上的情况。

Fig. 3. Rules for Equivalence Relation

规则解释:

  • [UT-ID] (Unitary Transformation with Identity): 这是 [UT] 规则的一个特例,用于比较两个酉算子 U1U_1U2U_2 对输入状态的近似等价性。偏差由金刚石范数来界定。 qˉ1:=U1[qˉ1]δqˉ2:=U2[qˉ2]:[UT-ID] \frac{}{ \vdash \bar{q}_1 := U_1[\bar{q}_1] \sim_\delta \bar{q}_2 := U_2[\bar{q}_2] : \equiv \Rightarrow \equiv } \quad \textbf{[UT-ID]} 其中 δ=12U1U1U2U2\delta = \frac{1}{2} \|U_1 U_1^\dagger - U_2 U_2^\dagger\|_\diamond
  • [COMP] (Composition): 允许通过引入中间程序来推理程序间的等价关系。 S1δ1S2:ABS2δ2S3:BCS1δ1+δ2S3:AC[COMP] \frac{ \vdash S_1 \sim_{\delta_1} S_2 : A \Rightarrow B \quad \vdash S_2 \sim_{\delta_2} S_3 : B \Rightarrow C }{ \vdash S_1 \sim_{\delta_1 + \delta_2} S_3 : A \Rightarrow C } \quad \textbf{[COMP]}

4.2.3. 健全性定理 (Soundness Theorem)

定理 1 (健全性) 对于任何程序 S1,S2S_1, S_2,投影 AABB,偏差 δ\delta,我们有: S1δS2:ABS1δS2:AB \vdash S_1 \sim_\delta S_2 : A \Rightarrow B \quad \Rightarrow \quad \models S_1 \sim_\delta S_2 : A \Rightarrow B 这个定理说明了证明系统 aqRHL 的健全性 (soundness),即如果一个判断可以在 aqRHL 中被证明,那么它在语义上是有效的。 本文的证明系统是健全的,但完整性 (completeness) 仍然是一个开放问题。对于经典确定性程序,关系霍尔逻辑在辅助补充单边规则的情况下被证明是相对完整的。然而,相对完整性不适用于概率程序。量子概率耦合的扩展以及引入近似使得这个问题更加复杂。

4.3. 测量条件和额外证明规则 (Measurements Conditions and Additional Proof Rules)

4.3.1. 测量条件 (Measurement Conditions)

对于 ifwhile 等复杂结构的语句,需要对程序施加额外的约束以建立可行的关系证明规则。经典 pRHL 中要求 ifwhile 语句中的守卫 (guards) 必须相等。但量子程序本质上是概率性的,通常不可能要求两个 if 语句给出相同的测量结果或相同的概率分布。

定义 10 (近似测量条件)M1={M1m}\mathcal{M}_1 = \{M_1^m\}M2={M2m}\mathcal{M}_2 = \{M_2^m\}H1\mathcal{H}_1H2\mathcal{H}_2 中具有相同测量结果集 {m}\{m\} 的两个测量。测量条件 M1{δm}M2:A{(pm,Bm)}\mathcal{M}_1 \approx_{\{\delta_m\}} \mathcal{M}_2 : A \Rightarrow \{(p_m, B_m)\} 意味着对于每个测量结果 mm,我们有: ρ1,ρ2.ρ1Aρ2{M1mρ1M1mBmδmM2mρ2M2mmax{Tr(M1mρ1M1m),Tr(M2mρ2M2m)}pm \forall \rho_1, \rho_2. \rho_1 \sim_A \rho_2 \Rightarrow \begin{cases} M_1^m \rho_1 M_1^{m\dagger} \sim_{B_m}^{\delta_m} M_2^m \rho_2 M_2^{m\dagger} \\ \max\{\operatorname{Tr}(M_1^m \rho_1 M_1^{m\dagger}), \operatorname{Tr}(M_2^m \rho_2 M_2^{m\dagger})\} \leq p_m \end{cases} 其中 pm[0,1]p_m \in [0, 1]。如果偏差 δm\delta_m 为零,可以省略。如果所有 pm=1p_m = 1,则将谓词 {(pm,Bm)}\{ (p_m, B_m) \} 简写为 {Bm}\{B_m\}

4.3.2. 额外证明规则 (Additional Proof Rules)

图 8 展示了 ifloop 语句的规则。

VLM 描述: 该图像是公式插图,展示了量子程序中分支和循环语句的证明规则。图中包括了针对 if 语句和 while 循环语句的规则,并给出了处理测量条件和偏差的数学表达式。

注意: 图像中公式的文本识别结果质量较低,部分字符难以辨认,因此在解释时会依赖其结构和典型含义进行推断。

  • [IF] (If-Then-Else): M1{δm}M2:A{(pm,Bm)}m.S1,mδmS2,m:BmCif(mM1=mS1,m)fim(pmδm+δm)if(mM2=mS2,m)fi:AC[IF] \frac{ \mathcal{M}_1 \approx_{\{\delta'_m\}} \mathcal{M}_2 : A \Rightarrow \{(p_m, B_m)\} \quad \forall m. \vdash S_{1,m} \sim_{\delta_m} S_{2,m} : B_m \Rightarrow C }{ \vdash \textbf{if}(\sum m \cdot \mathcal{M}_1 = m S_{1,m}) \textbf{fi} \sim_{\sum_m (p_m \delta_m + \delta'_m)} \textbf{if}(\sum m \cdot \mathcal{M}_2 = m S_{2,m}) \textbf{fi} : A \Rightarrow C } \quad \textbf{[IF]} 该规则要求前提中的测量条件提供整个近似的边界,其中分支体 S1,m,S2,mS_{1,m}, S_{2,m} 的偏差 δm\delta_m 会按 pmp_m 进行缩放。
  • [LP] (Loop): 循环规则不要求循环守卫的同步执行 [8, 9],也不要求循环收敛的速度边界 [26]。相反,测量条件只对第一次迭代进入循环体的概率 p1p_1 施加上限。 M1{δ0,δ1}M2:A{(p0,B0),(p1,B1)}S1δS2:B1Awhile M1=1 do S1 od δ0+p1δ/(1p1)while M2=1 do S2 od :AB0[LP] \frac{ \mathcal{M}_1 \approx_{\{\delta'_0, \delta'_1\}} \mathcal{M}_2 : A \Rightarrow \{(p_0, B_0), (p_1, B_1)\} \quad \vdash S_1 \sim_\delta S_2 : B_1 \Rightarrow A }{ \vdash \textbf{while } \mathcal{M}_1 = 1 \textbf{ do } S_1 \textbf{ od } \sim_{\delta'_0 + p_1 \delta / (1-p_1)} \textbf{while } \mathcal{M}_2 = 1 \textbf{ do } S_2 \textbf{ od } : A \Rightarrow B_0 } \quad \textbf{[LP]} 规则 [LP] 要求 p1[0,1)p_1 \in [0, 1),并且 p1p_1 越小,偏差越小。如果 p1p_1 最初等于 1,可以通过多次展开循环语句使其小于 1。
  • [LP] (Loop Iteration):* 作为 [LP] 的替代,当无法为 [LP] 找到好的 AA 时,此规则为循环迭代引入了更具体的测量条件。通常,在对循环进行近似推理时,会设置迭代次数的上限 NNM1{δm}M2:A0{(pm,Am+1)}m[0,N1].S1δmS2:AmAm+1max(pN,p~N)ϵwhile M1=1 do S1 od m=0N1(j=0m1pj)(δm+δm)+ϵwhile M2=1 do S2 od :A0AN[LP*] \frac{ \mathcal{M}_1 \approx_{\{\delta'_m\}} \mathcal{M}_2 : A_0 \Rightarrow \{(p_m, A_{m+1})\} \quad \forall m \in [0, N-1]. \vdash S_1 \sim_{\delta_m} S_2 : A_m \Rightarrow A_{m+1} \quad \max(p_N, \tilde{p}_N) \leq \epsilon }{ \vdash \textbf{while } \mathcal{M}_1 = 1 \textbf{ do } S_1 \textbf{ od } \sim_{\sum_{m=0}^{N-1} (\prod_{j=0}^{m-1} p_j) (\delta_m + \delta'_m) + \epsilon} \textbf{while } \mathcal{M}_2 = 1 \textbf{ do } S_2 \textbf{ od } : A_0 \Rightarrow A_N } \quad \textbf{[LP*]} [LP*] 是 [SEQ] 规则在有限次迭代上的直接应用,其中测量条件用于调整偏差。
  • 单边规则 (One-sided Rules): 例如 [IF-L], [LP-L], [LP*-L],它们在左右程序结构不同时很有用。例如,左侧程序是 if 语句,右侧程序是 skip

4.3.2.1. 结构规则 (Structural Rules)

图 9 展示了结构规则。

VLM 描述: 该图像是公式插图,展示了量子程序的关系逻辑中的结构规则。图中包含了三个规则:框架规则(FRAME)、顺序规则(ORDER)和近似规则(APPROX),并给出了它们的形式化表达。
  • [FRAME] (Frame Rule): 针对量子程序,由于子系统之间潜在的量子纠缠,构建通用框架规则具有挑战性。此规则适用于额外独立系统 (rˉ1,rˉ2)(\bar{r}_1, \bar{r}_2) 上的谓词 CC 是一维的情况。 (qˉ1,qˉ2)S1δS2:AB(rˉ1,rˉ2)var(S1,S2)=Dim(C(rˉ1,rˉ2))=1(qˉ1,rˉ1),(qˉ2,rˉ2)S1δS2:AC(rˉ1,rˉ2)BC(rˉ1,rˉ2)[FRAME] \frac{ \vdash_{(\bar{q}_1, \bar{q}_2)} S_1 \sim_\delta S_2 : A \Rightarrow B \quad (\bar{r}_1, \bar{r}_2) \cap \operatorname{var}(S_1, S_2) = \emptyset \quad \operatorname{Dim}(C_{(\bar{r}_1, \bar{r}_2)}) = 1 }{ \vdash_{(\bar{q}_1, \bar{r}_1), (\bar{q}_2, \bar{r}_2)} S_1 \sim_\delta S_2 : A \otimes C_{(\bar{r}_1, \bar{r}_2)} \Rightarrow B \otimes C_{(\bar{r}_1, \bar{r}_2)} } \quad \textbf{[FRAME]} 其中 var(S1,S2)\operatorname{var}(S_1, S_2) 是程序 S1,S2S_1, S_2 中所有变量的集合,C(rˉ1,rˉ2)C_{(\bar{r}_1, \bar{r}_2)} 是在独立系统 (rˉ1,rˉ2)(\bar{r}_1, \bar{r}_2) 上的谓词。
  • [ORDER] (Order Rule): 允许在偏差上添加序关系 \leqS1δS2:ABAABBδδS1δS2:AB[ORDER] \frac{ \vdash S_1 \sim_{\delta'} S_2 : A' \Rightarrow B' \quad A \subseteq A' \quad B' \subseteq B \quad \delta' \leq \delta }{ \vdash S_1 \sim_\delta S_2 : A \Rightarrow B } \quad \textbf{[ORDER]} 这表示如果一个判断以更小的偏差和更强的条件成立,那么它也以更大的偏差和更弱的条件成立。
  • [APPROX] (Approximation Rule): 引入一个额外条件,允许切换后置条件,但会引入近似。 S1S2:ABρ1,ρ2.ρ1Bρ2ρ1Cδρ2S1δS2:AC[APPROX] \frac{ \vdash S_1 \sim S_2 : A \Rightarrow B \qquad \forall \rho_1, \rho_2. \rho_1 \sim_B \rho_2 \Rightarrow \rho_1 \sim_C^\delta \rho_2 }{ \vdash S_1 \sim_\delta S_2 : A \Rightarrow C } \quad \textbf{[APPROX]} 这表示如果两个程序精确地满足后置条件 BB,而 BB 又可以通过偏差 δ\delta 近似于 CC,那么这两个程序可以近似地满足 CC

5. 实验设置

本文通过对两个著名的量子算法进行形式化验证来展示 aqRHL 的有效性:低深度近似量子傅里叶变换 (AQFT) 和重复直到成功算法 (Repeat-Until-Success, RUS)。这里我们主要关注 AQFT 的验证。

5.1. 目标 (Objective)

量子傅里叶变换 (QFT) 是经典离散傅里叶变换的量子模拟,它对量子态进行线性变换,并提取量子态振幅的周期性。由于量子门的非完美性,提出了近似量子傅里叶变换 (AQFT) 以降低 QFT 的电路深度,提高效率。

  • [17] 提出了一种直接的 AQFT,通过忽略与高阶项相关的门。

  • Cleve 和 Watrous [16] 通过并行化相位估计过程实现了低电路深度的 AQFT。

    本文的目标是使用 aqRHL 来推导形式为 SQFTδSAQFT:S_{\mathrm{QFT}} \sim_\delta S_{\mathrm{AQFT}} : \equiv \Rightarrow \equiv 的判断,以评估 AQFT 近似 QFT 的程度。

5.2. 规格 (Specification)

对于一个 nn 量子位系统,QFT 在计算基态 x=x1x2xn|x\rangle = |x_1 x_2 \dots x_n\rangle 上的线性操作 UU 定义为: Ux=ψx=12ny=0N1(e2πi/N)xyy U |x\rangle = |\psi_x\rangle = \frac{1}{\sqrt{2^n}} \sum_{y=0}^{N-1} (e^{2\pi i / N})^{x \cdot y} |y\rangle 其中 N:=2nN := 2^nψx|\psi_x\rangle 被称为相对于状态 x|x\rangle 的傅里叶基态,xyx \cdot y 表示 xxyy 的二进制表示之间的乘积。

ψx|\psi_x\rangle 也可以描述为: ψx=μ0.xnμ0.xn1xnμ0.x1xn |\psi_x\rangle = |\mu_{0.x_n}\rangle |\mu_{0.x_{n-1}x_n}\rangle \cdots |\mu_{0.x_1\dots x_n}\rangle 其中 μθ=(0+e2πiθ1)/2|\mu_\theta\rangle = (|0\rangle + e^{2\pi i \theta} |1\rangle)/\sqrt{2}0.xixj0.x_i\dots x_j 表示二进制小数 xi/2+xi+1/4++xj/2ji+1x_i/2 + x_{i+1}/4 + \cdots + x_j/2^{j-i+1}。 状态 μθ|\mu_\theta\rangle 可以通过对 +=(0+1)/2|+\rangle = (|0\rangle + |1\rangle)/\sqrt{2} 应用相位移门 P(2πθ)P(2\pi\theta)(见第 2 节)获得。相位移门 P(2πθ)P(2\pi\theta) 可以分解为一系列 R_m = P(2\pi/2^m) 门,因为 P(θ1)P(θ2)=P(θ1+θ2)P(\theta_1)P(\theta_2) = P(\theta_1+\theta_2)。受控 RmR_m 门表示为 CRm[(q1,q2)]CR_m[(q_1, q_2)],它是 c.P(θ)c.P(\theta) 门(见第 2 节)的特例,其中 θ=2π/2m\theta = 2\pi/2^m

QFT 可以并行实现 [16],如下图 (原文 Figure 4) 所示。

Fig. 4. QFT circuit in \[16\]. Given a computational basis state \(| x \\rangle\) and corresponding Fourier basis state \(| \\psi _ { x } \\rangle\) , unitary \(V\) performs mapping \(| x \\rangle | 0 \\rangle ^ { \\otimes n } \\mapsto | x \\rangle | \\psi _ { x } \\rangle\) , unitary `A d d` performs mapping \(| \\psi _ { x } \\rangle | 0 \\rangle ^ { \\otimes n } \\cdots | 0 \\rangle ^ { \\otimes n } \\mapsto | \\psi _ { x } \\rangle | \\psi _ { x } \\rangle \\cdots | \\psi _ { x } \\rangle\) , and unitary \(T\) performs mapping \(| \\psi _ { x } \\rangle \\cdots | \\psi _ { x } \\rangle | 0 \\rangle ^ { \\otimes n } \\mapsto | \\psi _ { x } \\rangle \\cdots | \\psi _ { x } \\rangle | x \\rangle\) . Fig. 5. Proof sketch for programs \(S _ { \\mathrm { Q F T } }\) and \(S _ { \\mathrm { A Q F T } }\) . To easily refer to predicates, we label each assertion a name `/ / P _ { i }` on its right. 该图像是 QFT 电路示意图,展示了如何将计算基态 x| x \rangle 映射为对应的傅里叶基态 ψx| \psi _ { x } \rangle。单位算子 VVAddTT 分别执行特定的映射操作,构成整个量子傅里叶变换过程。

原文 Figure 4 描述: QFT 电路在 [16] 中。给定计算基态 x| x \rangle 和对应的傅里叶基态 ψx| \psi _ { x } \rangle ,酉算子 VV 执行映射 x0nxψx| x \rangle | 0 \rangle ^ { \otimes n } \mapsto | x \rangle | \psi _ { x } \rangle ,酉算子 Add 执行映射 ψx0n0nψxψxψx| \psi _ { x } \rangle | 0 \rangle ^ { \otimes n } \cdots | 0 \rangle ^ { \otimes n } \mapsto | \psi _ { x } \rangle | \psi _ { x } \rangle \cdots | \psi _ { x } \rangle ,酉算子 TT 执行映射 ψxψx0nψxψxx| \psi _ { x } \rangle \cdots | \psi _ { x } \rangle | 0 \rangle ^ { \otimes n } \mapsto | \psi _ { x } \rangle \cdots | \psi _ { x } \rangle | x \rangle

可以通过忽略较高阶的 CRmCR_m 门来近似酉算子 VVTT,以实现更低的电路深度。酉算子 VV'TT'VVTT 的近似。程序 SAQFTS_{\mathrm{AQFT}}SQFTS_{\mathrm{QFT}} 几乎相同,只是用 VV'TT' 替换了 VVTT

本文使用 aqRHL 推理程序 SQFTS_{\mathrm{QFT}}SAQFTS_{\mathrm{AQFT}} 之间的近似等价性,即: SQFTδ1+2δ2SAQFT:(qˉ0,qˉ0)00aux(qˉ0,qˉ0)00aux S_{\mathrm{QFT}} \sim_{\delta_1 + 2\delta_2} S_{\mathrm{AQFT}} : \equiv_{(\bar{q}_0, \bar{q}_0')} \otimes |0\rangle\langle0|_{\mathrm{aux}} \Rightarrow \equiv_{(\bar{q}_0, \bar{q}_0')} \otimes |0\rangle\langle0|_{\mathrm{aux}} 其中 δ=nπ2k1+2nek/8\delta = n\pi 2^{-k-1} + 2ne^{-k/8}00aux|0\rangle\langle0|_{\mathrm{aux}} 表示除了 q0q_0qˉ0\bar{q}_0' 之外所有寄存器中量子位上的常数投影 00|0\rangle\langle0| 的张量积。

5.3. 主要证明步骤

5.3.1. 创建傅里叶基态 (Create the Fourier Basis State)

方程 (6) 中酉算子 UU 的计算可以通过以下酉算子 Qt,iQ_{t,i} 并行化 [16],该算子在不擦除 x|x\rangle 的情况下生成傅里叶基态 ψx|\psi_x\rangleQt,i:0tx1xnμ0.xixi+t10t1x1xn Q_{t,i} : |0\rangle^{\otimes t} |x_1 \dots x_n\rangle \mapsto |\mu_{0.x_i \dots x_{i+t-1}}\rangle |0\rangle^{\otimes t-1} |x_1 \dots x_n\rangle 其中 i+t1ni+t-1 \le n,量子位 x1xi1x_1 \dots x_{i-1}xi+txnx_{i+t} \dots x_n 未被使用。 酉算子 Qt,iQ_{t,i} 作用在寄存器 (qˉ,pˉ)(\bar{q}, \bar{p}) 上,可以表示为: UGHZ[qˉ];CR1[(pˉ[i],qˉ[1])];;CRt[(pˉ[i+t1],qˉ[t])];UGHZ[qˉ];H[qˉ[1]] U_{\mathrm{GHZ}}[\bar{q}]; CR_1[(\bar{p}[i], \bar{q}[1])]; \dots; CR_t[(\bar{p}[i+t-1], \bar{q}[t])]; U_{\mathrm{GHZ}}^\dagger[\bar{q}]; H[\bar{q}[1]] 其中 UGHZU_{\mathrm{GHZ}} 生成 GHZ 态,UGHZ0t=(0t+1t)/2U_{\mathrm{GHZ}}|0\rangle^{\otimes t} = (|0\rangle^{\otimes t} + |1\rangle^{\otimes t})/\sqrt{2}。寄存器 qqpp 的大小分别为 ttnnqˉ[i]\bar{q}[i] 表示寄存器 qq 中的第 ii 个量子位。

如下图 (原文 Figure 6) 所示的酉算子 Q4,iQ_{4,i} 的电路。

Fig. 6. Circuit for oracle `Q _ { 4 , i }` on state \(\\left| x _ { 1 } \\ldots x _ { n } \\right.\) . Qubits \(x _ { 1 } \\ldots x _ { i - 1 }\) and \(x _ { i + 4 } \\ldots x _ { n }\) are not used and ignored. 该图像是示意图,展示了用于量子算法的电路,特别是包含多个门控操作 HHRiR_i 的配置。电路的输入状态为 0angle|0 angle,并且最后一个量子态为 u0,xiext...xi+3angle| u_0, x_i ext{ ... } x_{i+3} angle,其中部分量子位未被使用。

原文 Figure 6 描述: 在状态 x1xn\left| x _ { 1 } \ldots x _ { n } \right. 上的酉算子 Q _ { 4 , i } 电路。量子位 x1xi1x _ { 1 } \ldots x _ { i - 1 }xi+4xnx _ { i + 4 } \ldots x _ { n } 未被使用并被忽略。

类似于 [17] 中的近似,酉算子 Qt,iQ_{t,i} 可以通过忽略较大的 CRmCR_m 门来近似。即,如果 1k<tn1 \leq k < t \leq n,我们可以用 Qk,iQ_{k,i} 来近似 Qt,iQ_{t,i}。这种近似可以通过以下判断建模: (qˉ,pˉ):=Qt,i[(qˉ,pˉ)]δ(t,t)(qˉ,pˉ):=Qt,i[(qˉ,pˉ)]:00(qˉ,qˉ)(pˉ,pˉ)(qˉ[1],qˉ[1])00(qˉ[2,n],qˉ[2,n])(pˉ,pˉ) \vdash (\bar{q}, \bar{p}) := Q_{t,i}[(\bar{q}, \bar{p})] \sim_{\delta(t,t')} (\bar{q}', \bar{p}') := Q_{t',i}[(\bar{q}', \bar{p}')] : |0\rangle\langle0|_{(\bar{q}, \bar{q}')} \otimes \equiv_{(\bar{p}, \bar{p}')} \Rightarrow \equiv_{(\bar{q}[1], \bar{q}'[1])} \otimes |0\rangle\langle0|_{(\bar{q}[2,n], \bar{q}'[2,n])} \otimes \equiv_{(\bar{p}, \bar{p}')} 其中 δ(t,t)=12sinπ(2t2t)\delta(t, t') = \frac{1}{2} \sin \pi (2^{-t} - 2^{-t'})

如下图 (原文 Figure 7) 所示的酉算子 VV 的电路。

Fig. 7. Circuit for oracle \(V\) . Given a computational basis state \(\\left| x \\right. = \\left| x _ { 1 } \\ldots x _ { n } \\right.\) , unitary \(C\) performs the mapping \(| x \\rangle | 0 \\rangle ^ { \\otimes ^ { n } } \\cdot \\cdot \\cdot | 0 \\rangle ^ { \\otimes ^ { n } } \\mapsto | x \\rangle ^ { \\otimes ^ { n } }\) , and unitary `Q _ { t , i }` performs the mapping \(| 0 \\rangle | x \\rangle \\mapsto | \\mu _ { 0 . x _ { i } . . . x _ { i + t - 1 } } \\rangle | x \\rangle\) . 该图像是示意图 7,展示了量子算子 VV 的电路结构。给定计算基态 xangle=x1angleimesext...imesxnangle| x angle = | x_{1} angle imes ext{...} imes | x_{n} angle,单位算子 CC 实现了映射 xangle0angleimesnoxangleimesn| x angle | 0 angle^{ imes n} o | x angle^{ imes n},而单位算子 Qt,iQ_{t,i} 完成了 0anglexangleou0.xi...extxi+t1anglexangle| 0 angle | x angle o | u_{0.x_{i}... ext{x}_{i+t-1}} angle | x angle 的映射。

原文 Figure 7 描述: 酉算子 VV 的电路。给定计算基态 x=x1xn\left| x \right. = \left| x _ { 1 } \ldots x _ { n } \right. ,酉算子 CC 执行映射 x0n0nxn| x \rangle | 0 \rangle ^ { \otimes n } \cdots | 0 \rangle ^ { \otimes n } \mapsto | x \rangle ^ { \otimes n } ,酉算子 Q _ { t , i } 执行映射 0xμ0.xi...xi+t1x| 0 \rangle | x \rangle \mapsto | \mu _ { 0 . x _ { i } . . . x _ { i + t - 1 } } \rangle | x \rangle

酉算子 VV 可以表示为: V=C[(qˉ0,rˉ)];Q1,n[(qˉ1[1],qˉ0)];Q2,n1[(qˉ1[2],rˉ1)];;Qn,1[(qˉ1[n],rˉn1)];C[(qˉ0,rˉ)] V = C[(\bar{q}_0, \bar{r})]; Q_{1,n}[(\bar{q}_1[1], \bar{q}_0)]; Q_{2,n-1}[(\bar{q}_1[2], \bar{r}_1)]; \dots; Q_{n,1}[(\bar{q}_1[n], \bar{r}_{n-1})]; C^\dagger[(\bar{q}_0, \bar{r})] 酉算子 VV'SAQFTS_{\mathrm{AQFT}} 中的近似)与 VV 几乎相同,只是用 Qk,iQ_{k,i} 近似了 Qt,iQ_{t,i},其中 0<k<tn0 < k < t \leq nkk 表示显著相位移门的数量。 基于判断 (8),得到以下判断: (qˉ0,qˉ1):=V[(qˉ0,qˉ1)]δ1(qˉ0,qˉ1):=V[(qˉ0,qˉ1)]:P0P1 \vdash (\bar{q}_0, \bar{q}_1) := V[(\bar{q}_0, \bar{q}_1)] \sim_{\delta_1} (\bar{q}_0', \bar{q}_1') := V'[(\bar{q}_0', \bar{q}_1')] : P_0 \Rightarrow P_1 其中 \delta_1 = \sum_{i=k+1}^n \delta(k, i) = \frac{1}{2} \sum_{i=k+1}^n \sin \pi (2^{-k} - 2^{-i}) \leq n\pi 2^{-k-1}

5.3.2. 复制与擦除傅里叶基态 (Replicate & Erase Fourier Basis State)

在 [16] 中,酉算子 Add 的功能是通过哈达玛门和望远镜式减法 (telescoping subtraction) 复制傅里叶基态,而 AddAdd^\dagger 则通过前缀加法 (prefix addition) 消除复制。由于 SAQFTS_{\mathrm{AQFT}}SQFTS_{\mathrm{QFT}} 在复制和擦除傅里叶基态的程序上相同,因此将它们简化为量子酉算子 AddAddAdd^\dagger。 然后使用 [UT] 规则得到以下判断: (qˉ1,qˉ2):=Add[(qˉ1,qˉ2)](qˉ1,qˉ2):=Add[(qˉ1,qˉ2)]:P1P2 \vdash (\bar{q}_1, \bar{q}_2) := \mathrm{Add}[(\bar{q}_1, \bar{q}_2)] \sim (\bar{q}_1', \bar{q}_2') := \mathrm{Add}[(\bar{q}_1', \bar{q}_2')] : P_1 \Rightarrow P_2 (qˉ1,qˉ2):=Add[(qˉ1,qˉ2)](qˉ1,qˉ2):=Add[(qˉ1,qˉ2)]:P5P6 \vdash (\bar{q}_1, \bar{q}_2) := \mathrm{Add}^\dagger[(\bar{q}_1, \bar{q}_2)] \sim (\bar{q}_1', \bar{q}_2') := \mathrm{Add}^\dagger[(\bar{q}_1', \bar{q}_2')] : P_5 \Rightarrow P_6

5.3.3. 估计傅里叶态的相位 (Estimate the Phase of a Fourier State)

这一步的关键在于量子测量可以通过辅助量子位和酉算子来模拟。 酉算子 TT 生成傅里叶态 ψx|\psi_x\rangle 中寄存器 q3q_3 的相位 x|x\rangle,然后通过 CNOT 门擦除寄存器 q0q_0 中的傅里叶基态 x|x\rangle (即 CNOTxx=x0CNOT|x\rangle|x\rangle = |x\rangle|0\rangle)。接着应用 TT^\dagger 来恢复状态。 为了降低酉算子 TT 的电路深度,[16] 并行化了 [29] 提出的相位估计过程。给定 kkμx2i|\mu_{x2^{-i}}\rangle 的副本,独立地对其中 k/2k/2 个副本执行两个单量子位测量: M1={M10=μ0μ0,M11=μ12μ12}M2={M20=μ14μ14,M21=μ34μ34} \mathcal{M}_1 = \{M_1^0 = |\mu_0\rangle\langle\mu_0|, M_1^1 = |\mu_{\frac{1}{2}}\rangle\langle\mu_{\frac{1}{2}}|\} \quad \mathcal{M}_2 = \{M_2^0 = |\mu_{\frac{1}{4}}\rangle\langle\mu_{\frac{1}{4}}|, M_2^1 = |\mu_{\frac{3}{4}}\rangle\langle\mu_{\frac{3}{4}}|\} 这些测量会在测量结果的 nk 比特字符串上生成一个分布 {p(x,i)}\{p_{(x,i)}\}。然后应用可逆经典处理函数 ff 来从 m(x,i)|m_{(x,i)}\rangle 推断出 xix_i'引理 4 [16] 给定任何计算基 x|x\rangle,随机测量可观测值 XXYY 会生成一个分布 {p(x,i)}\{p_{(x,i)}\},接着通过经典处理生成相位 xi|x_i'\rangle。我们有 Pr(xi=x)=p(x,i)>14nek/8\operatorname{Pr}(|x_i'\rangle = |x\rangle) = p_{(x,i)} > 1 - 4ne^{-k/8}

可以将上述整个过程转换为一个在叠加态上操作的酉算子 TT',而无需实际测量。 首先,应用酉算子 UM([qˉ1,qˉ2,rˉ])U_M([\bar{q}_1, \bar{q}_2, \bar{r}]) 模拟测量: UM([qˉ1,qˉ2,rˉ]):=i=1n(j=1k/2UX[(r[ik+j],p[ik+j])])(j=1+k/2kUY[(r[ik+j],p[ik+j])])) U_M([\bar{q}_1, \bar{q}_2, \bar{r}]) := \otimes_{i=1}^n (\otimes_{j=1}^{k/2} U_X[(r[ik+j], p[ik+j])]) \otimes (\otimes_{j=1+k/2}^k U_Y[(r[ik+j], p[ik+j])])) 其中寄存器 pˉ={qˉ1,qˉ2}\bar{p} = \{\bar{q}_1, \bar{q}_2\},辅助寄存器 rr 初始化为 0|0\rangle。酉门 UXU_XUYU_Y 引入辅助量子位 q1q_1 来模拟单量子位测量 M1\mathcal{M}_1M2\mathcal{M}_2。 接下来,将 UMU_M 的辅助寄存器 rr 的输出设置为酉算子 O[(rˉ,qˉ3)]O[(\bar{r}, \bar{q}_3)] 的输入,使得: UMμx2i0Oip(x,i)φxi U_M |\mu_{x2^{-i}}\rangle \otimes |0\rangle \stackrel{O}{\longrightarrow} \sum_i \sqrt{p_{(x,i)}} |\varphi\rangle \otimes |x_i'\rangle 因此,酉算子 TT' 可以通过顺序应用 UM([qˉ1,qˉ2,rˉ])U_M([\bar{q}_1, \bar{q}_2, \bar{r}])O[(rˉ,qˉ3)]O[(\bar{r}, \bar{q}_3)] 来实现。根据引理 4,得到: (qˉ1,qˉ2,qˉ3):=T[(qˉ1,qˉ2,qˉ3)]δ2(qˉ1,qˉ2,qˉ3,rˉ):=T[(qˉ1,qˉ2,qˉ3,rˉ)]:P2P3 \vdash (\bar{q}_1, \bar{q}_2, \bar{q}_3) := T[(\bar{q}_1, \bar{q}_2, \bar{q}_3)] \sim_{\delta_2} (\bar{q}_1', \bar{q}_2', \bar{q}_3', \bar{r}) := T'[(\bar{q}_1', \bar{q}_2', \bar{q}_3', \bar{r})] : P_2 \Rightarrow P_3 (qˉ1,qˉ2,qˉ3):=T[(qˉ1,qˉ2,qˉ3)]δ2(qˉ1,qˉ2,qˉ3,rˉ):=T[(qˉ1,qˉ2,qˉ3,rˉ)]:P4P5 \vdash (\bar{q}_1, \bar{q}_2, \bar{q}_3) := T^\dagger[(\bar{q}_1, \bar{q}_2, \bar{q}_3)] \sim_{\delta_2} (\bar{q}_1', \bar{q}_2', \bar{q}_3', \bar{r}) := T'^\dagger[(\bar{q}_1', \bar{q}_2', \bar{q}_3', \bar{r})] : P_4 \Rightarrow P_5 其中 δ2=2nek/8\delta_2 = 2ne^{-k/8}

5.4. 评估指标 (Evaluation Metrics)

本文的评估指标是近似偏差 δ\delta。它量化了两个量子程序(一个理想程序和一个近似实现程序)之间的差异。

  • 概念定义: 近似偏差 δ\delta 是衡量近似量子耦合和近似量子提升中,两个状态的边缘分布与原始状态之间的迹距离的最大值。它直接反映了近似实现的“不完美”程度。
  • 数学公式: 在近似量子耦合的定义中: D(ρ1,Tr2(ρ))δD(ρ2,Tr1(ρ))δ D(\rho_1, \operatorname{Tr}_2(\rho)) \leq \delta \qquad D(\rho_2, \operatorname{Tr}_1(\rho)) \leq \delta aqRHL 的判断中: S1δS2:AB S_1 \sim_\delta S_2 : A \Rightarrow B 在特定的酉变换近似中,偏差 δ\delta 可以通过金刚石范数来上界: δ=12U1U1U2U2 \delta = \frac{1}{2} \|U_1 \cdot U_1^\dagger - U_2 \cdot U_2^\dagger\|_\diamond
  • 符号解释:
    • ρ1,ρ2\rho_1, \rho_2: 待比较的两个量子态(部分密度算子)。
    • ρ\rho: 两个量子态的耦合状态。
    • D(,)D(\cdot, \cdot): 迹距离。
    • Tri()\operatorname{Tr}_i(\cdot): 对第 ii 个子系统求部分迹。
    • δ\delta: 近似偏差,通常是一个非负实数,表示近似程度。
    • S1,S2S_1, S_2: 待比较的两个量子程序。
    • A, B: 分别是前置条件和后置条件,表示为投影算子。
    • U1,U2U_1, U_2: 两个酉算子。
    • \|\cdot\|_\diamond: 金刚石范数。

5.5. 对比基线 (Comparative Baselines)

本文的工作是提出一种新的形式化验证框架,因此没有直接与其他“方法”进行性能比较,而是通过解决现有框架难以处理的问题来展示其优势。

  • 与精确关系霍尔逻辑对比: 本文的工作解决了现有精确量子关系霍尔逻辑在处理具有不同分支概率的近似程序时遇到的局限性,即精确耦合不存在的问题。通过引入近似偏差,aqRHL 能够对这些实际场景进行形式化验证。
  • 与单程序鲁棒性分析对比: 现有关于量子程序鲁棒性的工作 [26, 66] 主要关注单个程序的误差界限,而非两个程序之间的关系。本文的 aqRHL 提供了更通用的关系推理能力。
  • 验证标准: 本文通过验证两个知名量子算法——低深度近似量子傅里叶变换 (AQFT) 和重复直到成功算法 (Repeat-Until-Success, RUS) 来验证其框架的有效性。AQFT 的误差界限与 [16] 中的结果渐近等价,表明 aqRHL 能够得到与现有理论结果一致的量化近似。

6. 实验结果与分析

本文通过对低深度近似量子傅里叶变换 (AQFT) 进行形式化验证来展示其 aqRHL 框架的有效性。主要目标是推导 QFT 和 AQFT 之间的近似关系判断 SQFTδSAQFT:S_{\mathrm{QFT}} \sim_\delta S_{\mathrm{AQFT}} : \equiv \Rightarrow \equiv,并量化偏差 δ\delta

6.1. 核心结果分析

6.1.1. AQFT 近似 QFT 的偏差量化

通过应用 aqRHL 中的规则,论文得出了 SQFTS_{\mathrm{QFT}}SAQFTS_{\mathrm{AQFT}} 之间的最终近似关系判断: SQFTδ1+2δ2SAQFT:(qˉ0,qˉ0)00aux(qˉ0,qˉ0)00aux S_{\mathrm{QFT}} \sim_{\delta_1 + 2\delta_2} S_{\mathrm{AQFT}} : \equiv_{(\bar{q}_0, \bar{q}_0')} \otimes |0\rangle\langle0|_{\mathrm{aux}} \Rightarrow \equiv_{(\bar{q}_0, \bar{q}_0')} \otimes |0\rangle\langle0|_{\mathrm{aux}} 其中总偏差 δ=nπ2k1+2nek/8\delta = n\pi 2^{-k-1} + 2ne^{-k/8}

  • 偏差构成: 总偏差 δ\delta 由两部分组成:

    • \delta_1 = \sum_{i=k+1}^n \delta(k, i) = \frac{1}{2} \sum_{i=k+1}^n \sin \pi (2^{-k} - 2^{-i}) \leq n\pi 2^{-k-1}。这部分偏差主要来源于酉算子 VV 被其近似 VV' 替代时,即在生成傅里叶基态时忽略了 CRmCR_m 门中的高阶项(对应于 mm 较大的项)。kk 是保留的显著相位移门的数量。当 kk 增加时(即更少的项被忽略),δ1\delta_1 会减小,表示近似更精确。
    • δ2=2nek/8\delta_2 = 2ne^{-k/8}。这部分偏差主要来源于酉算子 TT 被其近似 TT' 替代时,即在相位估计过程中引入的近似。它是通过测量可观测值 XXYY 后进行经典后处理来估计相位时产生的误差。这里 kk 指的是用于相位估计的副本数量。当 kk 增加时,δ2\delta_2 会指数级减小,表示相位估计的准确度提高。
  • 渐近等价性: 论文指出,这个误差界限与 [16] 中的结果渐近等价。这表明 aqRHL 能够提供与现有领域专家分析结果相符的、有意义的量化误差估计。这种一致性增强了 aqRHL 作为形式化验证工具的可信度。

6.1.2. 证明流程的有效性

论文通过图 5 (原文 Figure 5) 展示了 QFT 和 AQFT 程序验证的证明草图。这个草图展示了如何通过 aqRHL 规则逐步推导最终的近似关系。

原文 Figure 5 描述: 程序 SmathrmQFTS _ { \\mathrm { Q F T } }SmathrmAQFTS _ { \\mathrm { A Q F T } } 的证明草图。为了便于引用谓词,我们在其右侧用 / / P _ { i } 标记每个断言。

VLM 描述: 该图像是公式插图,展示了量子傅里叶变换 (QFT) 及其近似版本 (AQFT) 的验证证明草图。图中包含了一系列量子操作的序列,如初始化、酉变换、加法和受控非门,并为每个步骤定义了前置条件和后置条件,以及相应的近似偏差。每个断言都通过 //Pi 进行了标记,例如 //P0、//P1 等。
  • 逐步推导: 证明过程将复杂的 QFT/AQFT 程序分解为一系列基本操作(如 VV, Add, TT, CNOT 及其逆操作)。每一步都应用了 aqRHL 中的相应规则(如 [UT], [SEQ])来计算或累积偏差。
  • 谓词演化: 谓词从初始的 P0P_0 (表示输入寄存器的等价性) 逐步演化到 P6P_6,最终通过 [SEQ] 规则将所有偏差累加起来,得到总偏差。
  • 精确操作的零偏差: 对于 AddCNOT 等被假定为精确执行的操作,其偏差为 0,这简化了证明。
  • 近似操作的偏差计算: 对于 VVTT 及其逆操作,由于使用了近似版本 VV'TT',需要使用金刚石范数等工具计算其引入的偏差 δ1\delta_1δ2\delta_2

6.1.3. 重复直到成功算法 (Repeat-Until-Success, RUS) 的近似正确性验证

除了 AQFT,论文还验证了 RUS 算法的近似正确性。RUS 算法是量子计算中一种重要的循环程序,它通过重复尝试直到达到特定条件来执行非确定性操作。

  • 适用性: aqRHL 中的循环规则 (如 [LP] 和 [LP*]) 能够处理 RUS 算法的概率性和潜在无限次迭代特性。通过设定迭代上限 NN,可以量化 RUS 算法在有限迭代次数下的近似性能。
  • 偏差来源: RUS 算法的近似偏差主要来自循环的有限次迭代。如果循环是无限次迭代,它可以精确地实现目标酉操作;但在实践中,迭代次数通常是有限的,因此会产生一个与未完成迭代概率相关的偏差。 例如,在论文中提到,如果 RUS 算法的迭代次数有上限 NN,则会产生一个近似等价性 E(ρ)δUρU\mathcal{E}'(\rho) \sim_\equiv^\delta U\rho U^\dagger,其中 E\mathcal{E}' 是有限循环的函数,偏差 δ=(1p)N/2\delta = (1-p)^N/2pp 是每次迭代成功达到目标状态的概率。

6.2. 实验结果的启示

  • 框架的实用性: aqRHL 框架不仅在理论上解决了量子程序近似关系推理的开放问题,而且通过具体的案例(QFT、RUS)证明了其在实际复杂量子算法形式化验证中的实用性。
  • 量化近似: aqRHL 提供了量化近似程度的机制(通过 δ\delta),这对于在 NISQ 时代设计和分析容错量子算法至关重要。开发者可以根据可接受的误差范围来选择近似策略。
  • 对未来发展的支持: 这种形式化方法为量子编译器优化、错误缓解技术和量子加密协议的验证提供了坚实的基础。

7. 总结与思考

7.1. 结论总结

本文成功解决了量子程序形式化验证领域的一个长期开放问题,即如何对量子程序的近似关系属性进行鲁棒的推理。通过以下关键创新,论文构建了一个名为 aqRHL 的近似量子关系霍尔逻辑:

  • 引入近似量子耦合和近似量子提升: 解决了在存在噪声或近似时,精确量子耦合失效的问题,使得即使在两个程序产生不同分支概率的情况下也能进行关系推理。

  • 构建了健全的 aqRHL 证明系统: 这是一个形式化的逻辑框架,能够量化和跟踪量子程序之间的近似偏差。

  • 成功应用于复杂量子算法的验证: 首次形式化验证了低深度近似量子傅里叶变换 (AQFT) 的误差界限,并验证了重复直到成功算法 (RUS) 的近似正确性。这些应用证明了 aqRHL 在实际问题中的有效性和实用性。

    aqRHL 弥补了现有量子关系逻辑在处理实际量子计算中不可避免的近似和不完美性方面的空白,为 NISQ 时代量子程序的可靠性分析提供了强有力的工具。

7.2. 局限性与未来工作

7.2.1. 论文作者指出的局限性与未来工作

  • 逻辑的完整性: 论文指出 aqRHL 的健全性已得到证明,但完整性仍是一个开放问题。对于概率程序,即使是经典的 pRHL 也难以证明相对完整性,量子版的 aqRHL 复杂度更高。
  • 扩展到混合系统:aqRHL 理论扩展到混合系统(即包含量子变量和经典变量的程序)是一个有前景的方向。统一的语言和分析框架对于利用量子优势同时利用现有经典计算基础设施至关重要。
  • 新应用: 探索 aqRHL量子密码学证明的构建和验证、以及专门为 NISQ 设备设计的优化量子编译器的正确性验证中的潜在应用。
  • 结合现有工具: 结合最近发展的工具,如量子抽象解释 (quantum abstract interpretation) [62] 和量子分离逻辑 (quantum separation logic) [64],来设计过近似 (over-approximation) 技术 [58]。
  • 后端表示与操作: 探索使用上下文无关语言有序二叉决策图 (Context-Free-Language Ordered Binary Decision Diagrams, CFLOBDDs) [46] 作为研究量子霍尔逻辑的后端表示和操作技术。

7.2.2. 个人启发与批判

  • 启发:

    • 应对现实世界挑战: 本文最显著的启发是,形式化方法不应止步于理想化模型,而应积极拥抱并形式化地处理现实世界系统固有的“不完美性”。在量子计算领域,近似是常态而非异常,因此能够量化和推理近似的逻辑框架显得尤为重要。
    • 理论与实践的桥梁: aqRHL 为连接量子算法的理论设计和实际物理实现之间的差距提供了桥梁。它允许算法设计者在保证一定误差范围内对程序的行为进行推理,这对于构建可信赖的量子软件生态系统至关重要。
    • 耦合理论的强大: 近似耦合的概念是一个优雅且强大的工具,它在量子领域找到了新的生命力,扩展了其在概率程序中的应用。这表明跨领域理论的迁移和泛化可以带来突破性的进展。
  • 潜在问题与可以改进的地方:

    • 偏差的精细化控制: 虽然论文提出了量化偏差 δ\delta 的方法,但在实际应用中,如何精确地为各种量子操作和测量计算最优的 δ\delta 值可能仍然具有挑战性。尤其是在程序结构变得非常复杂时,δ\delta 的累积方式可能导致边界过于宽松。未来可以研究更紧凑的偏差估计方法。
    • 自动化支持: 形式化验证方法通常需要专家手工构造证明。为了提高 aqRHL 的可用性和可扩展性,开发自动化或半自动化的证明工具和技术是关键。这可能涉及到与量子编程语言工具链的集成,以实现对程序属性的自动推理。
    • 对纠缠和非局域性的处理: 虽然 aqRHL 使用投影谓词在联合系统上定义关系,从而间接处理了纠缠,但在更复杂的纠缠态或非局域操作场景下,这种谓词的表达能力和证明复杂性可能需要进一步深入研究。特别是在框架规则中,对独立系统上的谓词 CC 限制为一维可能是一个简化,未来可以探索更通用的框架规则。
    • 完整性问题: 完整性是一个核心的理论问题。虽然很难,但探索 aqRHL 的相对完整性界限,或者识别其不完整的具体原因,将为该领域的理论发展提供重要见解。
    • NISQ 设备的具体噪声模型: 论文目前主要关注近似算法实现导致的偏差。未来可以进一步结合更详细的物理噪声模型(例如,去极化、振幅阻尼等),将这些噪声的影响更直接地整合到 aqRHL 的偏差计算中,从而更全面地评估量子程序的鲁棒性。

相似论文推荐

基于向量语义检索推荐的相关论文。

暂时没有找到相似论文。