Refuting Equivalence in Probabilistic Programs with Conditioning
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917889811939328 |
|---|---|
| author | Chatterjee, Krishnendu Goharshady, Ehsan Kafshdar Novotný, Petr Žikelić, Đorđe |
| author_facet | Chatterjee, Krishnendu Goharshady, Ehsan Kafshdar Novotný, Petr Žikelić, Đorđe |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2501_06579 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Refuting Equivalence in Probabilistic Programs with Conditioning Chatterjee, Krishnendu Goharshady, Ehsan Kafshdar Novotný, Petr Žikelić, Đorđe Programming Languages Formal Languages and Automata Theory 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. |
| title | Refuting Equivalence in Probabilistic Programs with Conditioning |
| topic | Programming Languages Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2501.06579 |