Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2023
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866911789409632256 |
|---|---|
| author | Klinkenberg, Lutz Blumenthal, Christian Chen, Mingshuai Haase, Darion Katoen, Joost-Pieter |
| author_facet | Klinkenberg, Lutz Blumenthal, Christian Chen, Mingshuai Haase, Darion Katoen, Joost-Pieter |
| contents | We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly unbounded loops. Our method is built on a denotational semantics represented by probability generating functions, which resolves semantic intricacies induced by intertwining discrete probabilistic loops with conditioning (for encoding posterior observations). We implement our method in a tool called Prodigy; it augments existing computer algebra systems with the theory of generating functions for the (semi-)automatic inference and quantitative verification of conditioned probabilistic programs. Experimental results show that Prodigy can handle various infinite-state loopy programs and exhibits comparable performance to state-of-the-art exact inference tools over loop-free benchmarks. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2307_07314 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions Klinkenberg, Lutz Blumenthal, Christian Chen, Mingshuai Haase, Darion Katoen, Joost-Pieter Programming Languages Logic in Computer Science We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring possibly unbounded loops. Our method is built on a denotational semantics represented by probability generating functions, which resolves semantic intricacies induced by intertwining discrete probabilistic loops with conditioning (for encoding posterior observations). We implement our method in a tool called Prodigy; it augments existing computer algebra systems with the theory of generating functions for the (semi-)automatic inference and quantitative verification of conditioned probabilistic programs. Experimental results show that Prodigy can handle various infinite-state loopy programs and exhibits comparable performance to state-of-the-art exact inference tools over loop-free benchmarks. |
| title | Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions |
| topic | Programming Languages Logic in Computer Science |
| url | https://arxiv.org/abs/2307.07314 |