Equivalence and Similarity Refutation for Probabilistic Programs

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F24%3A00139770" target="_blank" >RIV/00216224:14330/24:00139770 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1145/3656462" target="_blank" >http://dx.doi.org/10.1145/3656462</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/3656462" target="_blank" >10.1145/3656462</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Equivalence and Similarity Refutation for Probabilistic Programs

Popis výsledku v původním jazyce

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

Equivalence and Similarity Refutation for Probabilistic Programs

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

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í

2024

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

Proceedings of the ACM on Programming Languages, Volume 8, Issue ACM SIGPLAN Conference on Programming Languages Design and Implementation (PLDI 2024)

ISBN

—

ISSN

2475-1421

e-ISSN

—

Počet stran výsledku

25

Strana od-do

2098-2122

Název nakladatele

ACM

Místo vydání

New York

Místo konání akce

New York

Datum konání akce

1. 1. 2024

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

CST - Celostátní akce

Kód UT WoS článku

001264464100087