Refuting Equivalence in Probabilistic Programs with Conditioning

Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F25%3A00144669" target="_blank" >RIV/00216224:14330/25:00144669 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-031-90653-4_14" target="_blank" >http://dx.doi.org/10.1007/978-3-031-90653-4_14</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-90653-4_14" target="_blank" >10.1007/978-3-031-90653-4_14</a>

Result language
angličtina
Original language name
Refuting Equivalence in Probabilistic Programs with Conditioning
Original language description
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.
Czech name
—
Czech description
—

Project
<a href="/en/project/GA23-06963S" target="_blank" >GA23-06963S: VESCAA: Verifiable and Efficient Synthesis of Controllers for Autonomous Agents</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year
2025
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection
Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025
ISBN
9783031906527
ISSN
0302-9743
e-ISSN
—
Number of pages
22
Pages from-to
279-300
Publisher name
Springer
Place of publication
Cham
Event location
Hamilton, Kanada
Event date
Jan 1, 2025
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—

Similar results(10)