概率程序的等价性与相似性反驳
Equivalence and Similarity Refutation for Probabilistic Programs
AI总结：
本文提出一种全自动的静态方法，通过同时计算输出函数、上期望上鞅和下期望下鞅来反驳无限状态概率程序的等价性与相似性，并提供形式化正确性保证。
摘要：
我们考虑静态反驳由一对概率程序定义的输出分布的等价性与相似性问题。等价性和相似性是概率程序的两个基本关系性质，对于其在实现和编译中的正确性至关重要。在这项工作中，我们提出了一种新的静态等价性与相似性反驳方法。我们的方法通过计算一个作用于程序输出的函数来反驳等价性和相似性，该函数关于两个程序输出分布的期望值不同。该函数与两个程序的上期望上鞅和下期望下鞅同时计算，我们证明它们共同为反驳等价性和相似性提供了形式化证明。据我们所知，我们的方法是关系程序分析中第一个同时具备以下理想特征的方法：（1）完全自动化，（2）适用于无限状态概率程序，（3）对其结果的正确性提供形式化保证。我们实现了该方法的一个原型，实验结果表明我们的方法能够有效反驳从文献中收集的多个示例的等价性和相似性。
英文摘要：
We consider the problems of statically refuting equivalence and similarity of output distributions defined by a pair of probabilistic programs. Equivalence and similarity are two fundamental relational properties of probabilistic programs that are essential for their correctness both in implementation and in compilation. In this work, we present a new method for static equivalence and similarity refutation. Our method refutes equivalence and similarity by computing a function over program outputs whose expected value with respect to the output distributions of two programs is different. The function is computed simultaneously with an upper expectation supermartingale and a lower expectation submartingale for the two programs, which we show to together provide a formal certificate for refuting equivalence and similarity. To the best of our knowledge, our method is the first approach to relational program analysis to offer the combination of the following desirable features: (1) it is fully automated, (2) it is applicable to infinite-state probabilistic programs, and (3) it provides formal guarantees on the correctness of its results. We implement a prototype of our method and our experiments demonstrate the effectiveness of our method to refute equivalence and similarity for a number of examples collected from the literature.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
