对抗垃圾产物的轶事

# 反对粗糙制品的轶事 来源：https://www.markusde.ca/pages/noslop.html --- 这是一则警示故事。 ## 第一幕 我最新的论文《用离散程序逻辑验证连续分布的精确采样器》涉及大量证明工作。我们在文中展示了如何运用程序逻辑技术证明关于实数特定实现（惰性比特流）的性质，并使用Rocq中的Iris框架进行了形式化验证。 这篇论文核心的“程序逻辑”要点既简洁又优雅；当然，这都得益于Joe处于“狼性模式”，在单个周末内完成了这部分工作。我对论文的主要贡献在于探索这个技巧的适用边界，最终将其扩展至验证一系列令人惊叹且反直觉的采样算法。 具体而言，我花了数月时间钻研这个想法，在此过程中几近崩溃。我含着泪水在Rocq中验证了上万个不同的黎曼积分的存在性、绝对收敛性和交换性，而我们的分析库对此支持有限且不一致。当时我并非AI重度使用者——这种精神折磨完全源于有机体验。结果是，我忘记了喜悦的感觉，但我对仓库的每一行代码都了如指掌。 ## 第二幕 由于我们采用非常规方式表示实数，我们的*充分性定理*（程序逻辑正确性的核心元定理）必须以非标准形式陈述。陈述大抵如下： > 定理**充分性** > - 设`e`为程序，`mu`为实数域上的合法分布 > - 设`P/2^Q`为任意二进制有理数 > - 若证明了`HasDistribution(e, mu)`（我们逻辑中的主要“判断式”） > - 且假设`IsLessThanDyadic(e, P/2^Q)`以概率1终止 > 则`IsLessThanDyadic(e, P/2^Q)`返回`true`的概率等于`mu(P/2^Q)` 所有特殊性都与`IsLessThanDyadic`相关——这是在没有实数类型的语言中模拟实数的必要层。该程序通过迭代比较`e`返回的实数的近似值与`P/2^Q`的近似值来工作。例如，若`P/2^Q`是二进制数`b0.110111...`，程序将迭代地比较`e`越来越精细的近似值，直到首次确定`e`所在区间： - `b0.0 < e < b0.1`？ - `b0.10 < e < b0.11`？ - `b0.110 < e < b0.111`？ - `b0.1100 < e < b0.1101`？ - 如此继续 当然，当`e`从足够光滑的概率分布（如高斯分布）中随机采样时，`e`恰好等于`P/2^Q`的概率为零，因此通过简单归纳论证可知`IsLessThanDyadic`的直观实现确实会以概率1终止。且容易论证（在我们的逻辑中也可证明）：若`e < P/2^Q`则输出`true`，若`P/2^Q < e`则输出`false`。借助基础测度论，由于我们已知每个二进制数`P/2^Q`对应的`IsLessThanDyadic(e, P/2^Q)`，这足以刻画`e`在整个实数轴上的累积密度函数，因此我们在逻辑中进行的证明是实质性的。 最终成果包含针对实值、真正的高斯和拉普拉斯分布的随机采样算法，以及足以填补先前工作未验证缺口的验证算术库。投稿时我对此非常自豪，特别是考虑到我投入了大量工作确保每个数学细节都完美无缺。 审稿人一致认为很出色，论文被接受了。太棒了！ ## 第三幕 虽然我们的充分性定理很好，但第四点有些特殊。我们在论文中提到，诸如Total Eris之类的外部工具在Rocq中证明`IsLessThanDyadic(e, P/2^Q)`以概率1终止毫无困难。在反驳阶段，我们决定实际坐下来完成这项工作，至少针对`[0,1]`上的均匀采样器。当时我坐在普罗维登斯的酒店房间里，编写Total Eris证明时突然意识到 ## 崩溃时刻 我们对`IsLessThanDyadic`的实现并未比较`P/2^Q`越来越精确的近似值。由于代码中的符号错误，它实际上在将`e`的结果与二进制数越来越*粗糙*的近似值进行比较： - `0 < e < 1` - `0 < e < 2` - `0 < e < 4` - `0 < e < 8` - 无限继续，哈哈，糟糕，我有麻烦了 因此，比不可证明更糟的是，程序实际上*不会终止*！ 为什么证明检查器仍然接受它？因为Eris是*部分正确性逻辑*，它自然接受任何关于非终止程序的陈述（事实上，部分正确性是逻辑主要技巧生效的必要条件）。而我们用以验证`IsLessThanDyadic`性质的Loeb归纳原理，仅假设程序处于终止轨迹中，导致我们草草带过的终止假设最终蔓延至充分性定理。当你深陷Loeb归纳证明时，正确证明与因非终止而无效的证明看起来几乎相同。 唯一（微小）的区别在于：如果证明因非终止而无效，你可以用Loeb归纳证明*任何东西*，但*无法*在充分性定理中完成最终终止假设的闭合。这正是我在普罗维登斯那个可怕夜晚的处境。 论文绝不能以此状态发表，我已在心理上准备撤回投稿。 ## 第五幕 我恐慌了一阵，但随后停止惊慌并修正了符号错误。证明依然有效，我得以完成Total Eris证明，闭合了最后的假设。 ## 尾声...什么情况？ 我也这么想。 虽然我写的证明原本无效，但实际上我写的是一个*正确*证明，只是处于无效语境中。修正符号错误后，我的部分正确性论证没有变化，但终止陈述从假变为真（通常这是个好的改变）。 之所以进展顺利，是因为我没有“恶意利用”Loeb归纳假设。最终证明仍通过Loeb归纳完成，关键在于我的证明中仍有部分真实依赖于能够避免非终止轨迹这一事实！区分“漏洞利用”与“正确证明”可能很困难，对证明工程而言理解其区别至关重要。 这个错误并非大问题，但后果可能很严重。我花费数月深入理解这些论证细节，因此完全掌握了它们，确信即使不正确也可修复。我正是这样做的。 几小时后，我们自信地提交反驳，声称确实验证了那个显然的假设。好险，牛仔。 ## 结语 这是一则警示故事。既然AI已普及且通常相当出色，有人认为可以随意堆砌证明并提交以获取论文封面的额外徽章。我不确定自己能否发现利用非终止程序漏洞的AI。但我很确定无法如此快速修复——仅从头重建正确版本所需的时间可能就太长了。 对待这些事务必须谨慎。形式化方法仍然艰深，需要专家解读结果。当你的粗糙制品与论文文本不完全匹配时，我得说，曾经受过教训的我就不会买账了。