一句话：提出首个全自动、可处理无限状态、带形式保证的概率程序等价性与相似性反驳方法
本文研究如何静态反驳一对概率程序所定义的输出分布之间的等价性与相似性，这两个关系性质对程序实现与编译的正确性都至关重要。作者提出一种新方法：通过计算一个定义在程序输出上的函数，使其在两个程序输出分布下的期望值不同，从而反驳等价性或相似性；该函数与两个程序各自的上期望超鞅和下期望次鞅同时计算，二者共同构成反驳的形式化证书。据作者所知，这是首个同时具备以下三个特征的关系程序分析方法：完全自动化、适用于无限状态概率程序、并对结果正确性提供形式化保证。作者实现了方法原型，并在文献中收集的多个例子上实验，验证了其反驳等价性与相似性的有效性。
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. CCS Concepts: • Theory of computation → Program verification; Program analysis; • Software and its engineering → Formal software verification; • Mathematics of computing → Probability and statistics .
@article{paperbot2504,
title = {Equivalence and Similarity Refutation for Probabilistic Programs},
author = {Krishnendu Chatterjee and Ehsan Kafshdar Goharshady and Petr Novotný and Đorđe Žikelić},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656462}
}