Refuting Equivalence in Probabilistic Programs with Conditioning

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Refuting Equivalence in Probabilistic Programs with Conditioning

Popis výsledku v původním jazyce

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ázev v anglickém jazyce

Refuting Equivalence in Probabilistic Programs with Conditioning

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10200 - Computer and information sciences

Projekt

<a href="/cs/project/GA23-06963S" target="_blank" >GA23-06963S: VESCAA: Verifikovatelná a efektivní syntéza kontrolerů pro autonomní agenty</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2025

Kód důvěrnosti údajů

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

Název statě ve sborníku

Tools and Algorithms for the Construction and Analysis of Systems - 31st International Conference, TACAS 2025

ISBN

9783031906527

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

22

Strana od-do

279-300

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

Hamilton, Kanada

Datum konání akce

1. 1. 2025

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—