{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:16:58Z","timestamp":1784837818751,"version":"3.55.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["2285273, EP\/T006579"],"award-info":[{"award-number":["2285273, EP\/T006579"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001381","name":"National Research Foundation Singapore","doi-asserted-by":"publisher","award":["NRF-RSS2022-009"],"award-info":[{"award-number":["NRF-RSS2022-009"]}],"id":[{"id":"10.13039\/501100001381","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    We study the problem of bounding the posterior distribution of discrete probabilistic programs with unbounded support, loops, and conditioning. Loops pose the main difficulty in this setting: even if exact Bayesian inference is possible, the state of the art requires user-provided loop invariant templates. By contrast, we aim to find\n                    <jats:italic toggle=\"yes\">guaranteed bounds<\/jats:italic>\n                    , which sandwich the true distribution. They are fully automated, applicable to more programs and provide more provable guarantees than approximate sampling-based inference. Since lower bounds can be obtained by unrolling loops, the main challenge is upper bounds, and we attack it in two ways. The first is called\n                    <jats:italic toggle=\"yes\">residual mass semantics<\/jats:italic>\n                    , which is a flat bound based on the residual probability mass of a loop. The approach is simple, efficient, and has provable guarantees.\n                  <\/jats:p>\n                  <jats:p>\n                    The main novelty of our work is the second approach, called\n                    <jats:italic toggle=\"yes\">geometric bound semantics<\/jats:italic>\n                    . It operates on a novel family of distributions, called\n                    <jats:italic toggle=\"yes\">eventually geometric distributions<\/jats:italic>\n                    (EGDs), and can bound the distribution of loops with a new form of loop invariants called\n                    <jats:italic toggle=\"yes\">contraction invariants<\/jats:italic>\n                    . The invariant synthesis problem reduces to a system of polynomial inequality constraints, which is a decidable problem with automated solvers. If a solution exists, it yields an exponentially decreasing bound on the\n                    <jats:italic toggle=\"yes\">whole<\/jats:italic>\n                    distribution, and can therefore bound moments and tail asymptotics as well, not just probabilities as in the first approach.\n                  <\/jats:p>\n                  <jats:p>\n                    Both semantics enjoy desirable theoretical properties. In particular, we prove soundness and convergence, i.e. the bounds converge to the exact posterior as loops are unrolled further. We also investigate sufficient and necessary conditions for the existence of geometric bounds. On the practical side, we describe\n                    <jats:italic toggle=\"yes\">Diabolo<\/jats:italic>\n                    , a fully-automated implementation of both semantics, and evaluate them on a variety of benchmarks from the literature, demonstrating their general applicability and the utility of the resulting bounds.\n                  <\/jats:p>","DOI":"10.1145\/3704874","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1104-1135","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5158-2002","authenticated-orcid":false,"given":"Fabian","family":"Zaiser","sequence":"first","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4725-410X","authenticated-orcid":false,"given":"Andrzej S.","family":"Murawski","sequence":"additional","affiliation":[{"name":"University of Oxford, Oxford, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7509-680X","authenticated-orcid":false,"given":"C.-H. Luke","family":"Ong","sequence":"additional","affiliation":[{"name":"Nanyang Technological University, Singapore, Singapore"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-22308-2_3"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591220"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/301308.301358"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523721"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4939-7049-0"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/968708.968710"},{"key":"e_1_3_2_11_1","unstructured":"Azucena Campillo Navarro. 2018. Order statistics and multivariate discrete phase-type distributions. Ph. D. Dissertation. DTU Compute."},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649824"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0004-3702(93)90036-B"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1201\/b16018"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(90)90107-9"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428208"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/93385.93409"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","unstructured":"Nils Jansen Christian Dehnert Benjamin Lucien Kaminski Joost-Pieter Katoen and Lukas Westhofen. 2016. Bounded Model Checking for Probabilistic Programs. In ATVA 2016: Automated Technology for Verification and Analysis - 14th International Symposium Chiba Japan October 17-20 2016 Proceedings (Lecture Notes in Computer Science Vol. 9938). 68\u201385. https:\/\/doi.org\/10.1007\/978-3-319-46520-3_5 10.1007\/978-3-319-46520-3_5","DOI":"10.1007\/978-3-319-46520-3_5"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-62-48057-1_24"},{"key":"e_1_3_2_24_1","unstructured":"Diederik P. Kingma and Jimmy Ba. 2015. Adam: A Method for Stochastic Optimization. In ICLR 2015: 3rd International Conference on Learning Representations San Diego CA USA May 7-9 2015 Conference Track Proceedings. http:\/\/arxiv.org\/abs\/1412.6980"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-68446-4_12"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3649844"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3641545"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"e_1_3_2_30_1","unstructured":"Feynman T. Liang Liam Hodgkinson and Michael W. Mahoney. 2023. A Heavy-Tailed Algebra for Probabilistic Programming. In NeurIPS 2023: Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023 New Orleans LA USA December 10-16 2023. http:\/\/papers.nips.cc\/paper_files\/paper\/2023\/hash\/3d8f7945cd7f4446cb05a390d4c00558-Abstract-Conference.html"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563341"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_3_2_34_1","unstructured":"Marcel F Neuts. 1975. Probability distributions of phase type. Liber Amicorum Prof. Emeritus H. Florin (1975)."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192394"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454078"},{"key":"e_1_3_2_37_1","unstructured":"Jan-Willem van de Meent Brooks Paige Hongseok Yang and Frank Wood. 2018. An Introduction to Probabilistic Programming. CoRR abs\/1809.10756 (2018). arXiv:1809.10756 http:\/\/arxiv.org\/abs\/1809.10756"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10107-004-0559-Y"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454062"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314581"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656432"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","unstructured":"Fabian Zaiser. 2024a. Artifact for: Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops (POPL 2025). https:\/\/doi.org\/10.5281\/zenodo.14169507 10.5281\/zenodo.14169507","DOI":"10.5281\/zenodo.14169507"},{"key":"e_1_3_2_43_1","unstructured":"Fabian Zaiser. 2024b. Towards Formal Verification of Bayesian Inference in Probabilistic Programming via Guaranteed Bounds. Ph. D. Dissertation. University of Oxford."},{"key":"e_1_3_2_44_1","unstructured":"Fabian Zaiser Andrzej S. Murawski and C.-H. Luke Ong. 2023. Exact Bayesian Inference on Discrete Models via Probability Generating Functions: A Probabilistic Programming Approach. In NeurIPS 2023: Advances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023 New Orleans LA USA December 10-16 2023. http:\/\/papers.nips.cc\/paper_files\/paper\/2023\/hash\/0747af6f877c0cb555fea595f01b0e83-Abstract-Conference.html"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","unstructured":"Fabian Zaiser Andrzej S. Murawski and C.-H. Luke Ong. 2024. Guaranteed Bounds on Posterior Distributions of Discrete Probabilistic Programs with Loops. https:\/\/doi.org\/10.48550\/arXiv.2411.10393 10.48550\/arXiv.2411.10393","DOI":"10.48550\/arXiv.2411.10393"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704874","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:18:14Z","timestamp":1770200294000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":44,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704874"],"URL":"https:\/\/doi.org\/10.1145\/3704874","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}