A Separation Logic for Negative Dependence
A Separation Logic for Negative Dependence
复制标题
DOI：
10.1145/3498719
复制
发表时间：
2022-01-01
影响因子：
1.8
通讯作者：
Tassarotti，Joseph
中科院分区：
文献类型：
--
作者：
Bao，Jialu;Gaboardi，Marco;Tassarotti，Joseph
关于基于哈希的概率数据结构的形式推理通常需要关于随机变量的推理，其中当一个变量变大（例如哈希到一个桶中的元素数量）时，其他变量往往会变小（例如哈希到一个桶中的元素数量）其他桶）。这是一个负相关的例子，概率独立性的推广，最近在算法设计和机器学习中找到了有趣的应用。尽管负相关对于概率数据结构的分析是有用的，但现有的验证方法不能为随机程序建立这种性质，为了填补这一空白，我们设计了LINA，一个概率分离逻辑推理负相关。继近年来概率分离逻辑用分离合取推理随机变量的概率独立性之后，本文用分离合取推理随机变量的负相关性。我们的断言逻辑具有两个分离的合取，一个用于独立，一个用于负依赖。本文将串蕴涵逻辑推广到支持多个分离连词，并给出了一个完善的证明系统。值得注意的是，用于分离合取的语义依赖于用于组合资源的非确定性操作，而不是部分操作。通过利用负依赖的闭包性质，我们的程序逻辑支持一个类似框架的负依赖和单调操作规则。我们演示了LINA如何验证基于哈希的数据结构和balls-into-bin过程的概率属性。
Formal reasoning about hashing-based probabilistic data structures often requires reasoning about random variables where when one variable gets larger (such as the number of elements hashed into one bucket), the others tend to be smaller (like the number of elements hashed into the other buckets). This is an example ofnegative dependence, a generalization of probabilistic independence that has recently found interesting applications in algorithm design and machine learning. Despite the usefulness of negative dependence for the analyses of probabilistic data structures, existing verification methods cannot establish this property for randomized programs.To fill this gap, we design LINA, a probabilistic separation logic for reasoning about negative dependence. Following recent works on probabilistic separation logic usingseparating conjunctionto reason about the probabilistic independence of random variables, we use separating conjunction to reason about negative dependence. Our assertion logic features two separating conjunctions, one for independence and one for negative dependence. We generalize the logic of bunched implications (BI) to support multiple separating conjunctions, and provide a sound and complete proof system. Notably, the semantics for separating conjunction relies on anon-deterministic, rather than partial, operation for combining resources. By drawing on closure properties for negative dependence, our program logic supports a Frame-like rule for negative dependence andmonotoneoperations. We demonstrate how LINA can verify probabilistic properties of hash-based data structures and balls-into-bins processes.