Refuting Equivalence in Probabilistic Programs with
Conditioning

D 2025

Refuting Equivalence in Probabilistic Programs with Conditioning

CHATTERJEE, Krishnendu; Ehsan GOHARSHADY; Petr NOVOTNÝ a Djordje ZIKELIC

Základní údaje

Originální název

Refuting Equivalence in Probabilistic Programs with Conditioning

Autoři

CHATTERJEE, Krishnendu; Ehsan GOHARSHADY; Petr NOVOTNÝ a Djordje ZIKELIC

Vydání

Cham, Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025, od s. 279-300, 22 s. 2025

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

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

Forma vydání

elektronická verze "online"

Impakt faktor

Impact factor: 0.402 v roce 2005

Označené pro přenos do RIV

Ano

Kód RIV

RIV/00216224:14330/25:00144669

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-90652-7

ISSN

DOI

https://doi.org/10.1007/978-3-031-90653-4_14

EID Scopus

2-s2.0-105004788224

Klíčová slova anglicky

probabilistic programs; program analysis; martingales; program similarity

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 2. 4. 2026 13:55, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference 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 GOHARSHADY; Petr NOVOTNÝ a Djordje ZIKELIC. Refuting Equivalence in Probabilistic Programs with Conditioning. Online. In Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025. Cham: Springer, 2025, s. 279-300. ISBN 978-3-031-90652-7. Dostupné z: https://doi.org/10.1007/978-3-031-90653-4_14.

@inproceedings{2562503,
   author = {Chatterjee, Krishnendu and Goharshady, Ehsan and Novotný, Petr and Zikelic, Djordje},
   address = {Cham},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025},
   doi = {https://doi.org/10.1007/978-3-031-90653-4_14},
   keywords = {probabilistic programs; program analysis; martingales; program similarity},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham},
   isbn = {978-3-031-90652-7},
   pages = {279-300},
   publisher = {Springer},
   title = {Refuting Equivalence in Probabilistic Programs with Conditioning},
   year = {2025}
}

TY  - CONF
ID  - 2562503
AU  - Chatterjee, Krishnendu - Goharshady, Ehsan - Novotný, Petr - Zikelic, Djordje
PY  - 2025
TI  - Refuting Equivalence in Probabilistic Programs with Conditioning
PB  - Springer
CY  - Cham
SN  - 9783031906527
KW  - probabilistic programs
KW  - program analysis
KW  - martingales
KW  - program similarity
N2  - We consider the problem of refuting equivalence of probabilistic programs, i.e., the problem of proving that two probabilistic programs induce different output distributions. We study this problem in the context of programs with conditioning (i.e., with observe and score statements), where the output distribution is conditioned by the event that all the observe statements along a run evaluate to true, and where the probability densities of different runs may be updated via the score statements. Building on a recent work on programs without conditioning, we present a new equivalence refutation method for programs with conditioning. Our method is based on weighted restarting, a novel transformation of probabilistic programs with conditioning to the output equivalent probabilistic programs without conditioning that we introduce in this work. Our method is the first to be both a) fully automated, and b) providing provably correct answers. We demonstrate the applicability of our method on a set of programs from the probabilistic inference literature.
ER  -

CHATTERJEE, Krishnendu; Ehsan GOHARSHADY; Petr NOVOTNÝ a Djordje ZIKELIC. Refuting Equivalence in Probabilistic Programs with Conditioning. Online. In \textit{Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025}. Cham: Springer, 2025, s.~279-300. ISBN~978-3-031-90652-7. Dostupné z: https://doi.org/10.1007/978-3-031-90653-4\_{}14.

Přehled o publikaci