Constraint-Based Synthesis of Coupling Proofs
Constraint-Based Synthesis of Coupling Proofs
复制标题
DOI：
10.1007/978-3-319-96145-3_18
复制
发表时间：
2018-04
期刊：
影响因子：
--
通讯作者：
Aws Albarghouthi;Justin Hsu
中科院分区：
文献类型：
--
作者：
Aws Albarghouthi;Justin Hsu
耦合证明是一种经典技术，通过仔细关联（或耦合）两个概率执行来证明随机算法对的属性。在本文中，我们展示了如何自动构建概率程序的此类证明。首先，我们提出 f 耦合后置条件，这是描述两个相关程序执行的抽象。其次，我们展示了 f 耦合后置条件的属性如何暗示原始程序的各种概率属性。第三，我们演示如何将证明搜索问题简化为形式的纯逻辑综合问题，从而使概率推理变得不必要。我们开发了一个原型实现来自动构建概率属性的耦合证明，包括程序表达式的一致性和独立性。
Proof by coupling is a classical technique for proving properties about pairs of randomized algorithms by carefully relating (or coupling) two probabilistic executions. In this paper, we show how to automatically construct such proofs for probabilistic programs. First, we present f-coupled postconditions, an abstraction describing two correlated program executions. Second, we show how properties of f-coupled postconditions can imply various probabilistic properties of the original programs. Third, we demonstrate how to reduce the proof-search problem to a purely logical synthesis problem of the form, making probabilistic reasoning unnecessary. We develop a prototype implementation to automatically build coupling proofs for probabilistic properties, including uniformity and independence of program expressions.