Equivalence and Similarity Refutation for Probabilistic
Programs

D 2024

Equivalence and Similarity Refutation for Probabilistic Programs

CHATTERJEE, Krishnendu; Ehsan Kafshdar GOHARSHADY; Petr NOVOTNÝ a Djordje ŽIKELIĆ

Základní údaje

Originální název

Equivalence and Similarity Refutation for Probabilistic Programs

Autoři

CHATTERJEE, Krishnendu; Ehsan Kafshdar GOHARSHADY; Petr NOVOTNÝ a Djordje ŽIKELIĆ

Vydání

New York, Proceedings of the ACM on Programming Languages, Volume 8, Issue ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI 2024), od s. 2098-2122, 25 s. 2024

Nakladatel

ACM

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Impakt faktor

Impact factor: 2.800

Kód RIV

RIV/00216224:14330/24:00139770

Organizační jednotka

Fakulta informatiky

ISSN

DOI

https://doi.org/10.1145/3656462

UT WoS

001264464100087

EID Scopus

2-s2.0-85197909455

Klíčová slova anglicky

probabilistic programs; formal methods; martingales

Štítky

core_A, firank_1

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 4. 4. 2025 05:36, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GA23-06963S, projekt VaV

Název: VESCAA: Verifikovatelná a efektivní syntéza kontrolerů pro autonomní agenty

Investor: Grantová agentura ČR, VESCAA: Verifikovatelná a efektivní syntéza kontrolerů pro autonomní agenty

Citovat

CHATTERJEE, Krishnendu; Ehsan Kafshdar GOHARSHADY; Petr NOVOTNÝ a Djordje ŽIKELIĆ. Equivalence and Similarity Refutation for Probabilistic Programs. Online. In Proceedings of the ACM on Programming Languages, Volume 8, Issue ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI 2024). New York: ACM, 2024, s. 2098-2122. ISSN 2475-1421. Dostupné z: https://doi.org/10.1145/3656462.

@inproceedings{2486807,
   author = {Chatterjee, Krishnendu and Goharshady, Ehsan Kafshdar and Novotný, Petr and Žikelić, Djordje},
   address = {New York},
   booktitle = {Proceedings of the ACM on Programming Languages, Volume 8, Issue ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI 2024)},
   doi = {https://doi.org/10.1145/3656462},
   keywords = {probabilistic programs; formal methods; martingales},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {New York},
   pages = {2098-2122},
   publisher = {ACM},
   title = {Equivalence and Similarity Refutation for Probabilistic Programs},
   year = {2024}
}

TY  - CONF
ID  - 2486807
AU  - Chatterjee, Krishnendu - Goharshady, Ehsan Kafshdar - Novotný, Petr - Žikelić, Djordje
PY  - 2024
TI  - Equivalence and Similarity Refutation for Probabilistic Programs
PB  - ACM
CY  - New York
KW  - probabilistic programs
KW  - formal methods
KW  - martingales
N2  - 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.
ER  -

CHATTERJEE, Krishnendu; Ehsan Kafshdar GOHARSHADY; Petr NOVOTNÝ a Djordje ŽIKELI$\backslash$'C. Equivalence and Similarity Refutation for Probabilistic Programs. Online. In \textit{Proceedings of the ACM on Programming Languages, Volume 8, Issue ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI 2024)}. New York: ACM, 2024, s.~2098-2122. ISSN~2475-1421. Dostupné z: https://doi.org/10.1145/3656462.

Přehled o publikaci