Equivalence and similarity refutation for probabilistic programs

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 implementati...

Full description

Saved in:
Bibliographic Details
Main Authors: CHATTERJEE, Krishnendu, GOHARSHADY, Ehsan Kafshdar, NOVOTNÝ, Petr, ZIKELIC, Dorde
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2025
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/9063
https://ink.library.smu.edu.sg/context/sis_research/article/10066/viewcontent/3656462.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
id sg-smu-ink.sis_research-10066
record_format dspace
spelling sg-smu-ink.sis_research-100662024-08-01T15:31:59Z Equivalence and similarity refutation for probabilistic programs CHATTERJEE, Krishnendu GOHARSHADY, Ehsan Kafshdar NOVOTNÝ, Petr ZIKELIC, Dorde 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. 2025-08-01T07:00:00Z text application/pdf https://ink.library.smu.edu.sg/sis_research/9063 info:doi/10.1145/3656462 https://ink.library.smu.edu.sg/context/sis_research/article/10066/viewcontent/3656462.pdf http://creativecommons.org/licenses/by-nc-nd/4.0/ Research Collection School Of Computing and Information Systems eng Institutional Knowledge at Singapore Management University Probabilistic programming Static program analysis Probability distribution equivalence Kantorovich distance Martingales Programming Languages and Compilers
institution Singapore Management University
building SMU Libraries
continent Asia
country Singapore
Singapore
content_provider SMU Libraries
collection InK@SMU
language English
topic Probabilistic programming
Static program analysis
Probability distribution equivalence
Kantorovich distance
Martingales
Programming Languages and Compilers
spellingShingle Probabilistic programming
Static program analysis
Probability distribution equivalence
Kantorovich distance
Martingales
Programming Languages and Compilers
CHATTERJEE, Krishnendu
GOHARSHADY, Ehsan Kafshdar
NOVOTNÝ, Petr
ZIKELIC, Dorde
Equivalence and similarity refutation for probabilistic programs
description 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.
format text
author CHATTERJEE, Krishnendu
GOHARSHADY, Ehsan Kafshdar
NOVOTNÝ, Petr
ZIKELIC, Dorde
author_facet CHATTERJEE, Krishnendu
GOHARSHADY, Ehsan Kafshdar
NOVOTNÝ, Petr
ZIKELIC, Dorde
author_sort CHATTERJEE, Krishnendu
title Equivalence and similarity refutation for probabilistic programs
title_short Equivalence and similarity refutation for probabilistic programs
title_full Equivalence and similarity refutation for probabilistic programs
title_fullStr Equivalence and similarity refutation for probabilistic programs
title_full_unstemmed Equivalence and similarity refutation for probabilistic programs
title_sort equivalence and similarity refutation for probabilistic programs
publisher Institutional Knowledge at Singapore Management University
publishDate 2025
url https://ink.library.smu.edu.sg/sis_research/9063
https://ink.library.smu.edu.sg/context/sis_research/article/10066/viewcontent/3656462.pdf
_version_ 1814047721253765120