Document Open Access Logo

On Iteration in Discrete Probabilistic Programming

Authors Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva, Fabio Zanasi

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.20.pdf
  • Filesize: 0.97 MB
  • 21 pages

Document Identifiers

Author Details

Mateo Torres-Ruiz
  • University College London, United Kingdom
Robin Piedeleu
  • University College London, United Kingdom
Alexandra Silva
  • Cornell University, Ithaca, NY, United States of America
Fabio Zanasi
  • University College London, United Kingdom
  • University of Bologna, OLAS team (INRIA), Italy

Funding

This work was partially supported by ERC grant Autoprobe (no. 101002697; Piedeleu, Silva, and Torres-Ruiz).
  • Zanasi, Fabio: Fabio Zanasi acknowledges support from EPSRC EP/V002376/1 and MIUR P2022HXNSC (PRIN 2022 PNRR - Next Generation EU).

Acknowledgements

The authors would like to thank the anonymous reviewers for their helpful comments and suggestions.

Cite AsGet BibTex

Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva, and Fabio Zanasi. On Iteration in Discrete Probabilistic Programming. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 20:1-20:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.20

Abstract

Discrete probabilistic programming languages provide an expressive tool for representing and reasoning about probabilistic models. These languages typically define the semantics of a program through its posterior distribution, obtained through exact inference techniques. While the semantics of standard programming constructs in this context is well understood, there is a gap in extending these languages with tools to reason about the asymptotic behaviour of programs. In this paper, we introduce unbounded iteration in the context of a discrete probabilistic programming language, give it a semantics, and show how to compute it exactly. This allows us to express the stationary distribution of a probabilistic function while preserving the efficiency of exact inference techniques. We discuss the advantages and limitations of our approach, showcasing their practical utility by considering examples where bounded iteration poses a challenge due to the inherent difficulty of assessing the proximity of a distribution to its stationary point.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • Probabilistic programming
  • Programming languages semantics
  • Unbounded iteration

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella-Béguelin. Probabilistic relational verification for cryptographic implementations. SIGPLAN Not., 49(1):193-205, January 2014. URL: https://doi.org/10.1145/2578855.2535847.
  2. Riddhipratim Basu, Jonathan Hermon, and Yuval Peres. Characterization of cutoff for reversible markov chains. The Annals of Probability, 45(3), May 2017. URL: https://doi.org/10.1214/16-aop1090.
  3. Randal E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Comput. Surv., 24(3):293-318, September 1992. URL: https://doi.org/10.1145/136035.136043.
  4. Dmitry Bugaychenko. On application of multi-rooted binary decision diagrams to probabilistic model checking. In Proceedings of the 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI'12, pages 104-118, Berlin, Heidelberg, 2012. Springer-Verlag. URL: https://doi.org/10.1007/978-3-642-27940-9_8.
  5. Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6):772-799, 2008. URL: https://doi.org/10.1016/j.artint.2007.11.002.
  6. Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, and Tobias Winkler. Does a program yield the right distribution? verifying probabilistic programs via generating functions. In International Conference on Computer Aided Verification, pages 79-101. Springer, 2022. Google Scholar
  7. Guillaume Claret, Sriram K. Rajamani, Aditya V. Nori, Andrew D. Gordon, and Johannes Borgström. Bayesian inference using data flow analysis. In Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC/FSE 2013, pages 92-102, New York, NY, USA, 2013. Association for Computing Machinery. URL: https://doi.org/10.1145/2491411.2491423.
  8. Fredrik Dahlqvist, Alexandra Silva, and Dexter Kozen. Semantics of Probabilistic Programming: A Gentle Introduction, pages 1-42. Cambridge University Press, 2020. URL: https://doi.org/10.1017/9781108770750.002.
  9. Swaraj Dash, Younesse Kaddar, Hugo Paquet, and Sam Staton. Affine monads and lazy structures for bayesian programming. Proc. ACM Program. Lang., 7(POPL), January 2023. URL: https://doi.org/10.1145/3571239.
  10. Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker, 2017. URL: https://arxiv.org/abs/1702.04311.
  11. P Diaconis. The cutoff phenomenon in finite markov chains. Proceedings of the National Academy of Sciences of the United States of America, 93(4):1659-1664, February 1996. URL: https://doi.org/10.1073/pnas.93.4.1659.
  12. Persi Diaconis. The markov chain monte carlo revolution. Bulletin of the American Mathematical Society, 46(2):179-205, November 2008. URL: https://doi.org/10.1090/s0273-0979-08-01238-x.
  13. Persi Diaconis and Mehrdad Shahshahan. Time to reach stationarity in the bernoulli-laplace diffusion model. Siam Journal on Mathematical Analysis, 18:208-218, 1987. Google Scholar
  14. Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic netkat. In Peter Thiemann, editor, Programming Languages and Systems, pages 282-309, Berlin, Heidelberg, 2016. Springer Berlin Heidelberg. Google Scholar
  15. Timon Gehr, Sasa Misailovic, Petar Tsankov, Laurent Vanbever, Pascal Wiesmann, and Martin Vechev. Bayonet: Probabilistic inference for networks. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pages 586-602, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3192366.3192400.
  16. Timon Gehr, Sasa Misailovic, and Martin Vechev. Psi: Exact symbolic inference for probabilistic programs. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification, pages 62-83, Cham, 2016. Springer International Publishing. Google Scholar
  17. Noah D. Goodman, Vikash K. Mansinghka, Daniel Roy, Keith Bonawitz, and Joshua B. Tenenbaum. Church: A language for generative models. In Proceedings of the Twenty-Fourth Conference on Uncertainty in Artificial Intelligence, UAI'08, pages 220-229, Arlington, Virginia, USA, 2008. AUAI Press. Google Scholar
  18. Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. Probabilistic programming. In Proceedings of the on Future of Software Engineering, pages 167-181. ACM, 2014. URL: https://doi.org/10.1145/2593882.2593900.
  19. Maria I. Gorinova, Andrew D. Gordon, and Charles Sutton. Probabilistic programming with densities in SlicStan: efficient, flexible, and deterministic. Proceedings of the ACM on Programming Languages, 3(POPL):1-30, January 2019. URL: https://doi.org/10.1145/3290348.
  20. Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Form. Asp. Comput., 6(5):512-535, September 1994. URL: https://doi.org/10.1007/BF01211866.
  21. Holger Hermanns, Marta Kwiatkowska, Gethin Norman, David Parker, and Markus Siegle. On the use of mtbdds for performability analysis and verification of stochastic systems. The Journal of Logic and Algebraic Programming, 56(1):23-67, 2003. Probabilistic Techniques for the Design and Analysis of Systems. URL: https://doi.org/10.1016/S1567-8326(02)00066-8.
  22. Steven Holtzen. RSDD. https://github.com/neuppl/rsdd/, 2023.
  23. Steven Holtzen, Sebastian Junges, Marcell Vazquez-Chanlatte, Todd Millstein, Sanjit A. Seshia, and Guy Van Den Broeck. Model checking finite-horizon markov chains with probabilistic inference, 2021. URL: https://arxiv.org/abs/2105.12326.
  24. Steven Holtzen, Guy Van den Broeck, and Todd Millstein. Scaling exact inference for discrete probabilistic programs. Proc. ACM Program. Lang., 4(OOPSLA), November 2020. URL: https://doi.org/10.1145/3428208.
  25. Roger A. Horn and Charles R. Johnson. Matrix Analysis. Cambridge University Press, 1985. URL: https://doi.org/10.1017/CBO9780511810817.
  26. Joe Hurd. Formal verification of probabilistic algorithms. Technical Report UCAM-CL-TR-566, University of Cambridge, Computer Laboratory, May 2003. URL: https://doi.org/10.48456/tr-566.
  27. Joost-Pieter Katoen. Model checking meets probability: A gentle introduction. In Manfred Broy, Doron A. Peled, and Georg Kalus, editors, Engineering Dependable Software Systems, volume 34 of NATO Science for Peace and Security Series, D: Information and Communication Security, pages 177-205. IOS Press, 2013. URL: https://doi.org/10.3233/978-1-61499-207-3-177.
  28. D. Knuth and A. Yao. Algorithms and Complexity: New Directions and Recent Results, chapter The complexity of nonuniform random number generation. Academic Press, 1976. Google Scholar
  29. Dexter Kozen. Semantics of probabilistic programs. Journal of Computer and System Sciences, 22(3):328-350, 1981. URL: https://doi.org/10.1016/0022-0000(81)90036-2.
  30. Marta Kwiatkowska, Gethin Norman, and David Parker. Prism 4.0: Verification of probabilistic real-time systems. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, pages 585-591, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  31. D.A. Levin and Y. Peres. Markov Chains and Mixing Times. MBK. American Mathematical Society, 2017. Google Scholar
  32. Thierry Martinez. pyml. https://opam.ocaml.org/packages/pyml/, 2023.
  33. A.J. Menezes, J. Katz, P.C. van Oorschot, and S.A. Vanstone. Handbook of Applied Cryptography. Discrete Mathematics and Its Applications. CRC Press, 1996. Google Scholar
  34. Carl D. Meyer. Matrix Analysis and Applied Linear Algebra. Society for Industrial and Applied Mathematics, USA, 2000. Google Scholar
  35. T. Minka, J.M. Winn, J.P. Guiver, Y. Zaykov, D. Fabian, and J. Bronskill. /Infer.NET 0.3, 2018. Microsoft Research Cambridge. http://dotnet.github.io/infer. Google Scholar
  36. T. Minka, J.M. Winn, J.P. Guiver, Y. Zaykov, D. Fabian, and J. Bronskill. /Infer.NET 0.3, 2018. Microsoft Research Cambridge. http://dotnet.github.io/infer. Google Scholar
  37. Praveen Narayanan, Jacques Carette, Wren Romano, Chung-chieh Shan, and Robert Zinkov. Probabilistic inference by program transformation in Hakaru (system description). In Oleg Kiselyov and Andy King, editors, Functional and Logic Programming, pages 62-79, Cham, 2016. Springer International Publishing. Google Scholar
  38. Frank Noé. Probability distributions of molecular observables computed from Markov models. The Journal of Chemical Physics, 128(24):244103, June 2008. URL: https://doi.org/10.1063/1.2916718.
  39. Fritz Obermeyer, Eli Bingham, Martin Jankowiak, Justin Chiu, Neeraj Pradhan, Alexander Rush, and Noah Goodman. Tensor variable elimination for plated factor graphs, 2019. URL: https://arxiv.org/abs/1902.03210.
  40. Dan Roth. On the hardness of approximate reasoning. Artificial Intelligence, 82(1):273-302, 1996. URL: https://doi.org/10.1016/0004-3702(94)00092-1.
  41. Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva. Cantor meets Scott: semantic foundations for probabilistic networks. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages. ACM, January 2017. URL: https://doi.org/10.1145/3009837.3009843.
  42. Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva. Scalable verification of probabilistic networks. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, June 2019. URL: https://doi.org/10.1145/3314221.3314639.
  43. Sam Staton. Commutative semantics for probabilistic programming. In Hongseok Yang, editor, Programming Languages and Systems, pages 855-879, Berlin, Heidelberg, 2017. Springer Berlin Heidelberg. Google Scholar
  44. David Tolpin, Jan-Willem van de Meent, Hongseok Yang, and Frank Wood. Design and implementation of probabilistic programming language anglican. In Proceedings of the 28th Symposium on the Implementation and Application of Functional Programming Languages, IFL 2016, New York, NY, USA, 2016. Association for Computing Machinery. URL: https://doi.org/10.1145/3064899.3064910.
  45. Mateo Torres-Ruiz. Dice. https://bitbucket.org/dice-iter/dice, 2024.
  46. Glynn Winskel. The formal semantics of programming languages - an introduction. In Foundation of computing series, 1993. URL: https://api.semanticscholar.org/CorpusID:7767429.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact