💻 computer science

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic

本文介绍了 Continuous-Eris，这是一种在 Rocq 证明助手中的高阶分离逻辑，用于形式化验证高斯分布和拉普拉斯分布等连续分布的精确采样算法的正确性，以解决浮点近似在安全性和准确性方面的局限性。

原作者： Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti

发布于 2026-05-14

📖 1 分钟阅读☕ 轻松阅读

原作者： Markus de Medeiros, Puming Liu, Kwing Hei Li, Alejandro Aguirre, Lars Birkedal, Joseph Tassarotti

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

想象一下，你正在尝试烤蛋糕，但不用标准的量杯，而是必须把桶里的水一滴一滴地倒进一个小杯子里来测量每种配料。如果你倒了 100 滴就停下，你得到的只是用量的近似值。如果你倒了 1,000 滴，结果会更接近。但只要你中途停下，从技术上讲你就犯了一个微小的错误，因为你没有获得精确的量。

在计算机科学的世界里，计算机处理实数（如 3.14159...）时正是如此。它们使用“浮点数”，这就像那些 100 滴水的近似值。对于大多数任务来说，这没问题。但对于敏感任务——例如在医学研究或财务记录中保护隐私数据——那些微小的“舍入误差”可能会累积成巨大的安全漏洞。

本文介绍了一种解决此问题的新方法。作者开发了一个名为 Continuous-Eris 的工具，帮助程序员证明他们的代码正在从连续分布中进行精确采样（例如在 0 到 1 之间选取一个完全随机的数），而从未产生任何舍入误差。

以下是他们是如何做到的，运用了一些富有创意的类比：

1. 问题所在：“懒惰”的厨师

通常，为了获得 0 到 1 之间的随机数，计算机可能会试图一次性生成整个无限序列的数字（如 0.101101...）。但这不可能；你无法写下无限长的列表。

相反，作者采用了一种“懒惰”的方法。想象一位厨师，他只在被要求时才一层一层地剥洋葱。

代码：程序 U（均匀分布）不会立即生成整个数字。它只是创建一个空列表。
请求：当你请求前几位数字时（使用一个名为 GetBits 的函数），程序会剥下一层（生成一个随机位，0 或 1）。
魔法：如果你稍后请求更多数字，它会再剥下一层。它按需逐位构建数字，速度与你需要的速度保持一致。这确保了你永远不需要处理无限列表，但你可以获得任意精度的答案。

2. 挑战：证明厨师是诚实的

难点不在于编写代码，而在于证明这位懒惰的厨师实际上是在公平地选取数字。

如果厨师剥了一层，那真的是随机的吗？
如果你要求剥 10 层，生成的数字是否真的均匀分布在整个范围内？
当厨师甚至还没剥完洋葱时，你如何证明这一点？

以前的工具只能证明简单离散事物（如掷骰子）的情况。它们无法处理连续数字这种“无限洋葱”，尤其是当代码复杂、使用内存并动态改变值时。

3. 解决方案：“无限磁带”与“时间收据”

为了解决这个问题，作者发明了一种新的逻辑系统（一套用于证明代码正确性的规则），结合了三个巧妙的技巧：

A. “预先绘制的磁带”（预采样）

想象你是一位魔术师。为了证明你的戏法有效，你在表演开始前就偷偷写下了你将要从牌堆中抽出的整张牌序列。
在他们的逻辑中，他们使用一条“磁带”作为这个预先写好的列表。尽管计算机是一次生成一个位，但证明假设整个无限位序列已经预先写在了一条魔法磁带上。这使得数学家能够推理“整个数字”，即使程序一次只看到“一个位”。

B. “时间收据”（预算）

这里是棘手之处：在计算机证明中，磁带实际上不能是无限的。
因此，他们使用了一个名为时间收据的概念。将其视为一种“步骤预算”。

逻辑规定：“我们只观察程序运行100 步。”
因为程序每生成一个位只需一步，如果我们只观察 100 步，我们就只需要知道魔法磁带上的前 100 个位。
“时间收据”是一个令牌，表示“我还剩 100 步”。每走一步，你就花费一张收据。
这使他们能够假装磁带是无限的，因为在证明的任何特定时刻，他们只需要有限数量的位，并且他们有“收据”来支付这些位。

C. “误差积分”（安全网）

最后，他们使用了误差积分。想象你有一个允许犯错的“预算”。

如果你想证明程序有 99.9% 的正确性，你就花费 0.1% 的积分。
作者开发了一种方法来“花费”这些积分，以证明程序行为错误的概率微乎其微。
他们想出了如何将离散的“错误预算”转化为平滑的连续数学工具（使用积分），以便他们能够证明代码适用于整个实数范围，而不仅仅是特定点。

4. 他们实际证明了什么

使用这个新系统，作者不仅谈论理论，还构建并验证了以下实际代码：

均匀分布：在 0 到 1 之间选取一个随机数。
高斯分布（钟形曲线）：选取一个围绕平均值聚集的数字（如人类身高）。
拉普拉斯分布：一种用于差分隐私（一种在不泄露个人秘密的情况下共享数据的方法）的特定噪声类型。

他们证明了这些分布的代码在数学上是精确的。如果你使用他们的代码，你得到的不是一个“差不多”的浮点数；你得到的是一个保证逐位遵循完美数学规则的数字。

结论

本文提出了一套新的“规则手册”（Continuous-Eris），允许程序员编写复杂、懒惰且精确的采样代码，并证明其 100% 正确。他们通过将“魔法预写磁带”与“步骤预算”系统相结合来实现这一点，使他们能够利用有限、可管理的步骤来推理无限的可能性。这是确保隐私保护算法和其他关键系统不因舍入误差而产生隐藏数学漏洞的重大进展。

技术摘要：使用离散程序逻辑验证连续分布的精确采样器

问题陈述

大多数连续概率分布的采样算法实现都依赖于浮点运算。虽然这对许多应用而言是可以接受的，但浮点运算会引入难以分析的舍入误差，并可能导致关键的安全漏洞，特别是在差分隐私领域，其中的算法通常是在假设精确算术的前提下进行形式化开发的。

另一种方法是使用基于可计算实数的精确采样算法，这些算法可以按需生成连续样本的数字，直至任意精度。然而，这些算法非常复杂。它们需要结合语义上具有挑战性的语言特性，包括概率选择、高阶函数以及动态分配的可变状态。现有的概率验证程序逻辑不足以完成此任务：先前的工作要么将推理限制在离散分布上，要么假设存在从连续分布采样的原语（通常依赖于不可计算的实数算术）。因此，目前缺乏形式化技术来验证在离散、有状态的编程模型中运行的、针对连续分布的可计算精确采样器的正确性。

方法论

作者提出了Continuous-Eris，这是一种用于验证可计算分布精确采样算法正确性的高阶分离逻辑。Continuous-Eris 扩展了Eris（一种用于验证离散概率程序近似正确性的逻辑），并构建于Iris分离逻辑框架之上。

核心方法论依赖于通过三个关键逻辑要素来弥合离散推理与连续推理之间的差距：

误差积分（Error Credits）： 借用于 Eris，这些是分离逻辑资源 $E(r)$ ，表示规范失效概率的上界。它们通过“消耗”积分来排除低概率的误差事件，从而实现对概率程序的模块化推理。
时间收据（Time Receipts）： 改编自 Mével 等人，用于将逻辑的部分正确性内化。通过跟踪剩余的执行步数（$StepsLeft(k)$），该逻辑可以推理潜在无限执行的有限前缀。这一点至关重要，因为精确采样器通常涉及惰性求值，其中无限位的序列永远不会被完全生成。
预采样带（Pre-sampling Tapes）： 改编自 Clutch，允许证明预先确定未来随机采样命令的结果。虽然标准磁带是有限的，但作者将它们与时间收据相结合，以模拟无限预采样带。这种机制允许逻辑将误差积分条件化于特定的实数 $r$ （由无限位串表示），即使程序在任何有限执行期间仅生成有限数量的位。

理论基础

该逻辑将 Marionneau 等人的离散正确性规范推广到了连续场景。Continuous-Eris 不是通过离散概率质量函数来刻画采样器，而是通过概率密度函数上的黎曼积分来刻画采样器。

生成 $[0, 1]$ 区间内均匀实数的采样器 $U$ 的核心规范模式为：
$\forall F \in PC([0, 1]), \quad \left\{ E\left(\int_0^1 F(x) dx\right) \right\} U() \{ v. \exists r. E(F(r)) * IsReal\ v\ r \}$
在此， $F$ 是有界的、分段连续的函数。该逻辑允许将积分条件化于采样值 $r$ ，仿佛它是均匀抽取的，前提是积分的期望值得以保持。这种方法的可靠性基于这样一个事实：（源自有限预采样的）黎曼和可以任意精确地逼近积分，而离散化误差则由“凭空产生”的误差积分来支付。

主要贡献

Continuous-Eris 逻辑： 一种新颖的程序逻辑，结合了误差积分、时间收据和预采样带，用于验证可计算的连续采样算法。它支持高阶函数、可变状态和动态分配。
精确采样器的形式化验证： 作者提供了以下精确采样器的形式化验证实现：
- $[0, 1]$ 上的均匀分布。
- 高斯（正态）分布。
- 拉普拉斯分布。
  这些实现基于 Karney 的算法，并利用惰性位列表表示。
已验证的构造性实数算术： 一个在 Continuous-Eris 内验证的精确实数算术库（CReal 的改编版）。该库支持对惰性实数执行运算（加法、取反、缩放、比较），从而能够从更简单的分布构建复杂的分布。
差分隐私的精度界： 形式化证明了已验证的拉普拉斯采样器满足差分隐私文献中使用的特定精度界。这证明了采样器的输出符合隐私保护机制所需的理论保证，而无需依赖浮点近似。
机械化： 所有结果均在Rocq 证明助手（前身为 Coq）中进行了机械化，基于 Iris 框架和 Coquelicot 实分析库构建。

结果

本文通过验证MaxU2程序（计算两个均匀样本的最大值）和完整的Karney 高斯采样器，展示了 Continuous-Eris 的实用性。

MaxU2： 作者证明了该程序返回的值服从概率密度为 $\mu_{max}(x) = 2x$ 的分布。证明涉及迭代积分和 Löb 归纳法，以处理递归的位比较。
高斯采样器： 验证遵循模块化结构，验证了伯努利试验、整数部分和拒绝采样循环的子程序。证明确立了采样器生成的值具有正确的高斯密度。
拉普拉斯采样器： 作者验证了拉普拉斯分布的采样器，并直接从逻辑中推导出了尾部界 $P[|L_{\epsilon, \mu} - \mu| > \frac{\log(1/\beta)}{\epsilon}] \leq \beta$ ，而无需将其作为基本公理添加。

意义与主张

本文声称填补了形式化验证中的一个关键空白，提供了第一种能够验证利用可变状态和高阶函数的连续分布的精确、可计算采样器的技术。

无近似的正确性： 与假设连续原语或使用浮点运算的先前的工作不同，Continuous-Eris 验证了仅使用离散原语（伯努利试验）生成精确样本（至任意精度）的算法。
处理复杂性： 该逻辑成功管理了结合随机性、可变状态和高阶函数的语义挑战，这些通常在指称语义推理中难以处理。
实际相关性： 通过验证拉普拉斯采样器及其精度界，这项工作为构建具有针对浮点误差的严格保证的差分隐私系统奠定了基础。
谦逊性： 作者承认了局限性。当前的方法依赖于黎曼积分，要求积分分布函数是分段连续的。这阻止了对具有不可数不连续点（例如，避开所有有理点）的分布的推理。此外，本文侧重于部分正确性；证明这些采样器的几乎必然终止性留待未来的工作或其他逻辑（如 Total Eris）来完成。

总之，Continuous-Eris 提供了一个严谨的、机械化的框架，用于验证复杂的、有状态的程序是否正确实现了从连续分布的精确采样，弥合了理论可计算分析与实际程序验证之间的差距。