从程序逻辑看概率耦合

### 从程序逻辑看概率耦合 概率程序的形式验证是一个活跃的研究领域，旨在推理概率计算的安全性和活性属性。许多重要的概率程序属性自然地用两个程序执行来表达，这些属性被称为关系属性。然而，推理概率程序的关系属性比确定性程序更具挑战性。本文将介绍一种强大的方法——耦合证明，并探讨概率程序逻辑pRHL与耦合证明之间的联系。 #### 1. 耦合证明简介 耦合证明最初由概率论学者为分析马尔可夫链而开发，现在在形式验证中也有惊人的应用。它可以用于建立广泛的关系属性，包括： - **概率等价（也称为差分隐私）**：两个程序产生的分布从观察者的角度来看是等价的或足够接近。 - **随机支配**：一个概率程序比另一个更有可能产生大的输出。 - **收敛（也称为混合）**：两个概率循环的输出分布随着循环迭代次数的增加而相互接近。 - **真实性（也称为纳什均衡）**：当代理报告真实值而不是偏离到误导性值时，其平均效用更大。 耦合证明的基本思想是通过耦合中间样本为输出分布构建一个耦合。通过仔细安排相关性，我们可以将两个执行视为以某种方便的方式链接在一起。这种方法可以显著简化概率推理，具体体现在以下几个方面： - **减少到单一随机源**：将两个运行视为共享一个单一的随机源，从而将两个程序视为一个进行推理。 - **抽象掉概率**：将概率推理与证明的非概率部分分离，只在选择采样指令的耦合时考虑概率方面。 - **实现组合性、结构化推理**：通过分别关注算法的每个步骤，然后平滑地组合结果，实现高度模块化的推理方式。 #### 2. 概率基础 在深入探讨耦合证明之前，我们需要了解一些概率理论的基础知识。我们使用离散子分布来建模可能不终止的程序。 **定义1**：一个可数集A上的（离散）子分布是一个映射μ : A → [0, 1]，使得所有元素的权重之和至多为1，即$\sum_{a\in A} \mu(a) \leq 1$。当权重之和为1时，我们称μ为适当分布。 我们还需要一些与离散分布相关的概念和符号： - **集合S的概率**：$\mu(S) \triangleq \sum_{a\in S} \mu(a)$ - **子分布的支持**：$supp(\mu) \triangleq \{a \in A | \mu(a) > 0\}$ - **子分布的权重**：$|\mu| \triangleq \sum_{a\in A} \mu(a)$ - **实值函数f在子分布μ上的期望值**：$E_{\mu}[f] \triangleq E_{a\sim\mu}[f(a)] \triangleq \sum_{a\in A} f(a) \cdot \mu(a)$ #### 3. 耦合和提升的定义及基本性质 概率耦合用一个联合分布来建模两个分布。 **定义2**：给定A1和A2上的子分布μ1和μ2，A1 × A2上的子分布μ是(μ1, μ2)的耦合，如果π1(μ) = μ1且π2(μ) = μ2，其中π1和π2是概率投影。 耦合通常不是唯一的，不同的见证表示不同的共享随机方式。以下是一些常见的耦合示例： - **恒等耦合**：$\mu_{id}(a_1, a_2) \triangleq \begin{cases} \mu(a) & : a_1 = a_2 = a \\ 0 & : otherwise \end{cases}$ - **否定耦合**：$\mu_{\neg}(a_1, a_2) \triangleq \begin{cases} 1/2 & : a_1 = 1 - a_2 \\ 0 & : otherwise \end{cases}$ - **独立或平凡耦合**：$\mu_{\times}(a_1, a_2) \triangleq \mu_1(a_1) \cdot \mu_2(a_2)$ 提升是耦合的一个重要概念，它可以用于证明概率属性。 **定义3**：设μ1和μ2是A1和A2上的子分布，R是A1 × A2上的关系。A1 × A2上的子分布μ是(μ1, μ2)的R - 提升的见证，如果： - μ是(μ1, μ2)的耦合。 - $supp(\mu) \subseteq R$。 如果存在满足这两个条件的μ，我们说μ1和μ2通过R的提升相关，记为$\mu_1 R^{\sharp} \mu_2$。 耦合和提升有许多有用的性质，例如： - **权重相等**：如果μ1和μ2存在耦合μ，则$|\mu_1| = |\mu_2|$。 - **分布相等**：$\mu_1 = \mu_2$当且仅当$\mu_1 (=)^{\sharp} \mu_2$。 - **随机支配**：$\mu_1 (\leq_A)^{\sharp} \mu_2$意味着$\mu_1 \leq_{sd} \mu_2$，反之亦然（在一定条件下）。 - **总变差距离**：$d_{tv}(\mu_1, \mu_2) \leq Pr_{(a_1, a_2)\sim\mu}[a_1 \neq a_2]$ #### 4. 耦合和提升的组合性质 耦合和提升在各种组合概念下是封闭的，其中最重要的是顺序组合。 **定理1**：设$\mu \in Distr(A_1 \times A_2)$见证$\mu_1 R^{\sharp} \mu_2$，$M : A_1 \times A_2 \to Distr(B_1 \times B_2)$使得对于每个$(a_1, a_2) \in R$，$M(a_1, a_2)$见证$M_1(a_1) S^{\sharp} M_2(a_2)$。则$bind(\mu, M)$见证$bind(\mu_1, M_1) S^{\sharp} bind(\mu_2, M_2)$。 这个定理允许我们通过为每个部分构建耦合来为两个过程的顺序组合构建一个耦合。 #### 5. 马尔可夫链的耦合和提升 耦合和R - 提升自然地扩展到离散时间马尔可夫链。 **定义4**：两个由初始子分布μ1和μ2以及转移函数t1和t2给出的马尔可夫链之间的耦合是一个由初始子分布μ和联合转移函数t : (A × A) → Distr(A × A)给出的马尔可夫链，使得： - μ是μ1和μ2的耦合。 - 对于每个x1和x2，t(x1, x2)是t1(x1)和t2(x2)的耦合。 R - 提升的概念也类似地扩展到马尔可夫链。 #### 6. 耦合证明示例 考虑一个概率过程，它抛掷一枚公平硬币T次并返回正面的数量。如果μ1和μ2分别是运行这个过程T = T1和T2次迭代的输出分布，且T1 ≤ T2，则$\mu_1 \leq_{sd} \mu_2$。 **耦合证明**：在前T1次迭代中，将硬币翻转耦合为相等，确保在前T1次迭代后，耦合的计数相等。第二次运行中剩余的T2 - T1次硬币翻转只能增加第二次计数，同时保持第一次计数不变。因此，在耦合下，终止时第一次计数不超过第二次计数，从而证明了$\mu_1 \leq_{sd} \mu_2$。 #### 7. pRHL逻辑简介 为了形式化耦合证明，我们引入概率关系Hoare逻辑pRHL。 ##### 7.1 程序逻辑基础 逻辑由一组公式（也称为判断）和一个解释组成，解释描述了判断为真（有效）的含义。许多逻辑提供一个证明系统，由一组逻辑规则组成，描述如何组合已知判断（前提）来证明一个新判断（结论）。 程序逻辑最初由Hoare在1969年引入，基于Floyd的早期思想。程序逻辑由断言逻辑和程序逻辑本身组成。一个程序逻辑判断由一个程序c和两个断言Φ和Ψ组成，其中Φ是执行c之前的初始条件，Ψ是执行c之后的最终条件。 ##### 7.2 pRHL的编程语言 pRHL中的程序由表达式和命令组成。表达式包括常量、变量和基本操作，命令包括跳过、赋值、采样、顺序组合、条件语句和循环。 表达式可以引用两类变量：程序变量和逻辑变量。程序状态是从程序变量到值的映射，逻辑上下文是从逻辑变量到值的映射。 我们使用分布表达式来建模程序可以采样的原始分布，例如硬币翻转和均匀分布。 命令的语义是一个从状态到输出状态子分布的数学函数。我们使用离散版本的语义，通过单位函数和绑定函数来解释命令。 ##### 7.3 pRHL的判断和有效性 pRHL的判断形式为$c_1 \sim c_2 : \Phi \Rightarrow \Psi$，其中c1和c2是命令，Φ和Ψ是对内存对的谓词。判断有效意味着对于任何满足Φ的两个内存(m1, m2)，存在一个Ψ的提升将两个输出分布相关联。 ##### 7.4 pRHL的证明规则 pRHL包括一组逻辑规则，用于归纳地从已知判断构建新判断。这些规则可以分为三类： - **双边规则**：当结论判断中的两个程序具有相同的顶层形状时适用。 - **Skip规则**：$\vdash skip \sim skip : \Phi \Rightarrow \Phi$ - **Assn规则**：$\vdash x_1 \leftarrow e_1 \sim x_2 \leftarrow e_2 : \Psi \{e_1^{\langle 1 \rangle}, e_2^{\langle 2 \rangle} / x_1^{\langle 1 \rangle}, x_2^{\langle 2 \rangle}\} \Rightarrow \Psi$ - **Sample规则**：如果$f : supp(d_1) \to supp(d_2)$是一个双射，则$\vdash x_1 \$ \leftarrow d_1 \sim x_2 \$ \leftarrow d_2 : \forall v \in supp(d_1), \Psi \{v, f(v) / x_1^{\langle 1 \rangle}, x_2^{\langle 2 \rangle}\} \Rightarrow \Psi$ - **Seq规则**：$\vdash c_1 \sim c_2 : \Phi \Rightarrow \Psi$，$\vdash c_1' \sim c_2' : \Psi \Rightarrow \Theta$，则$\vdash c_1; c_1' \sim c_2; c_2' : \Phi \Rightarrow \Theta$ - **Cond规则**：如果$\vDash \Phi \to e_1^{\langle 1 \rangle} = e_2^{\langle 2 \rangle}$，$\vdash c_1 \sim c_2 : \Phi \land e_1^{\langle 1 \rangle} \Rightarrow \Psi$，$\vdash c_1' \sim c_2' : \Phi \land \neg e_1^{\langle 1 \rangl