Federico Olmedo
Skip Abstract Section
Abstract
This article investigates the semantic intricacies of conditioning, a main feature in probabilistic programming. Our study is based on an extension of the imperative probabilistic guarded command language pGCL with conditioning. We provide a weakest precondition (wp) semantics and an operational semantics. To deal with possibly diverging program behavior, we consider liberal preconditions. We show that diverging program behavior plays a key role when defining conditioning. We establish that weakest preconditions coincide with conditional expected rewards in Markov chains—the operational semantics—and that the wp-semantics conservatively extends the existing semantics of pGCL (without conditioning). An extension of these results with nondeterminism turns out to be problematic: although an operational semantics using Markov decision processes is rather straightforward, we show that providing an inductive wp-semantics in this setting is impossible. Finally, we present two program transformations that eliminate conditioning from any program. The first transformation hoists conditioning while updating the probabilistic choices in the program, while the second transformation replaces conditioning—in the same vein as rejection sampling—by a program with loops. In addition, we present a last program transformation that replaces an independent identically distributed loop with conditioning.
- Nathanael Leedom Ackerman, Cameron E. Freer, and Daniel M. Roy. 2011. Noncomputable conditional distributions. In Proc. of LICS. IEEE Computer Society, 107--116. Google Scholar
Digital Library
- Miguel E. Andrés and Peter van Rossum. 2008. Conditional probabilities over probabilistic and nondeterministic systems. In TACAS (LNCS), Vol. 4963. Springer, 157--172.Google Scholar
- Philippe Audebaud and Christine Paulin-Mohring. 2009. Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74, 8 (2009), 568--589. Google ScholarDigital Library
- Ralph-Johan Back and Joakim von Wright. 1998. Refinement Calculus - A Systematic Introduction. Springer. Google ScholarCross Ref
- Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press.Google ScholarDigital Library
- Christel Baier, Joachim Klein, Sascha Klüppelholz, and Steffen Märcker. 2014. Computing conditional probabilities in Markovian models efficiently. In TACAS (LNCS), Vol. 8413. Springer, 515--530.Google Scholar
- Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, and Justin Hsu. 2016. Synthesizing probabilistic invariants via doob’s decomposition. In CAV (LNCS), Vol. 9779. Springer, 43--61.Google Scholar
- Hans Bekić. 1984. Definable operation in general algebras, and the theory of automata and flowcharts. In Programming Languages and Their Definition. Springer, 30--55.Google Scholar
- Johannes Borgström, Andrew D. Gordon, Michael Greenberg, James Margetson, and Jurgen Van Gael. 2011. Measure transformer semantics for Bayesian machine learning. In ESOP (LNCS), Vol. 6602. Springer, 77--96.Google Scholar
- Göran Broström and Leif Nilsson. 2000. Acceptance--rejection sampling from the conditional distribution of independent discrete random variables, given their sum. Statistics J. Theoret. Appl. Stat. 34, 3 (2000), 247--257.Google Scholar
- Michael Carbin, Sasa Misailovic, and Martin C. Rinard. 2013. Verifying quantitative reliability for programs that execute on unreliable hardware. In OOPSLA. ACM Press, 33--52. Google ScholarDigital Library
- Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic program analysis with martingales. In CAV (LNCS), Vol. 8044. Springer, 511--526. Google ScholarCross Ref
- Aleksandar Chakarov and Sriram Sankaranarayanan. 2014. Expectation invariants for probabilistic program loops as fixed points. In SAS (LNCS), Vol. 8723. Springer, 85--100. Google ScholarCross Ref
- Krishnendu Chatterjee, Hongfei Fu, Petr Novotný, and Rouzbeh Hasheminezhad. 2016. Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In POPL. ACM Press, 327--342.Google Scholar
- Guillaume Claret, Sriram K. Rajamani, Aditya V. Nori, Andrew D. Gordon, and Johannes Borgström. 2013. Bayesian inference using data flow analysis. In ESEC/SIGSOFT FSE. ACM Press, 92--102.Google Scholar
- David Cock. 2014. pGCL for Isabelle. Archive of Formal Proofs (2014).Google Scholar
- Patrick Cousot and Michael Monerau. 2012. Probabilistic abstract interpretation. In ESOP (LNCS), Vol. 7211. Springer, 169--193. Google ScholarDigital Library
- Jerry den Hartog and Erik P. de Vink. 2002. Verifying probabilistic programs using a Hoare like logic. Int. J. Found. Comput. Sci. 13, 3 (2002), 315--340. Google ScholarCross Ref
- Edsger W. Dijkstra. 1976. A Discipline of Programming. Prentice Hall.Google ScholarDigital Library
- Anton Dries, Angelika Kimmig, Wannes Meert, Joris Renkens, Guy Van den Broeck, Jonas Vlasselaer, and Luc De Raedt. 2015. ProbLog2: Probabilistic logic programming. In ECML/PKDD (3) (LNCS), Vol. 9286. Springer, 312--315.Google Scholar
- Barbara Espinoza and Geoffrey Smith. 2013. Min-entropy as a resource. Inf. Comput. 226 (2013), 57--75. Google ScholarCross Ref
- Noah D. Goodman and Andreas Stuhlmüller. 2014. The Design and Implementation of Probabilistic Programming Languages. (electronic). http://dippl.org.Google Scholar
- Andrew D. Gordon, Thore Graepel, Nicolas Rolland, Claudio V. Russo, Johannes Borgström, and John Guiver. 2014. Tabular: A schema-driven probabilistic programming language. In POPL. ACM Press, 321--334.Google ScholarDigital Library
- Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. 2014. Probabilistic programming. In FOSE. ACM Press, 167--181. Google ScholarDigital Library
- Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver. 2014. Operational versus weakest pre-expectation semantics for the probabilistic guarded command language. Perform. Eval. 73 (2014), 110--132. Google ScholarDigital Library
- Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. 1999. Stochastic processes as concurrent constraint programs. In POPL. ACM Press, 189--202. Google ScholarDigital Library
- Eric C. R. Hehner. 2011. A probability perspective. Formal Aspects Comput. 23, 4 (2011), 391--419. Google ScholarDigital Library
- Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, and Selva Samuel. 2014. Slicing probabilistic programs. In PLDI. ACM Press, 133--144. Google ScholarDigital Library
- Joe Hurd, Annabelle McIver, and Carroll Morgan. 2005. Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346, 1 (2005), 96--112. Google ScholarDigital Library
- Nils Jansen, Christian Dehnert, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Lukas Westhofen. 2016. Bounded model checking for probabilistic programs. In ATVA (LNCS). Springer, 68--85. Google ScholarCross Ref
- Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Federico Olmedo, Friedrich Gretz, and Annabelle McIver. 2015. Conditioning in probabilistic programming. Electronic Notes in Theoretical Computer Science (ENTCS) 319 (2015), 199--216. DOI:https://doi.org/10.1016/j.entcs.2015.12.013 Google ScholarDigital Library
- Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2015. On the hardness of almost-sure termination. In Mathematical Foundations of Computer Science (MFCS), Part I (LNCS), Vol. 9234. Springer, 307--318. Google ScholarCross Ref
- Benjamin Lucien Kaminski and Joost-Pieter Katoen. 2017. A weakest pre-expectation semantics for mixed-sign expectations. In Proc. of LICS. IEEE Computer Society, 1--12. Google ScholarCross Ref
- Joost-Pieter Katoen, Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, and Federico Olmedo. 2015. Understanding probabilistic programs. In Correct System Design (LNCS), Vol. 9360. Springer, 15--32. Google ScholarCross Ref
- Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll C. Morgan. 2010. Linear-invariant generation for probabilistic programs. In SAS (LNCS), Vol. 6337. Springer, 390--406. Google ScholarCross Ref
- Mark Kattenbelt, Marta Z. Kwiatkowska, Gethin Norman, and David Parker. 2010. A game-based abstraction-refinement framework for Markov decision processes. Formal Methods Syst. Design 36, 3 (2010), 246--280. Google ScholarDigital Library
- Dexter Kozen. 1981. Semantics of probabilistic programs. J. Comput. Syst. Sci. 22, 3 (1981), 328--350. Google ScholarCross Ref
- Dexter Kozen. 1985. A probabilistic PDL. J. Comput. Syst. Sci. 30, 2 (1985), 162--178. Google ScholarCross Ref
- Johan J. Lukkien. 1994. Operational semantics and generalized weakest preconditions. Sci. Comput. Program. 22, 1--2 (1994), 137--155.Google Scholar
- Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer.Google ScholarDigital Library
- Carroll Morgan, Annabelle McIver, and Karen Seidel. 1996. Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. 18, 3 (1996), 325--353. Google ScholarDigital Library
- Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, and Selva Samuel. 2014. R2: An efficient MCMC sampler for probabilistic programs. In AAAI. AAAI Press, 2476--2482.Google Scholar
- Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about recursive probabilistic programs. In Proc. of LICS. ACM Press, 672--682. Google ScholarDigital Library
- Brooks Paige and Frank Wood. 2014. A compilation target for probabilistic programming languages. In ICML (Proc. of JMLR), Vol. 32. 1935--1943.Google Scholar
- Avi Pfeffer. 2016. Practical Probabilistic Programming. Manning Publications Co.Google ScholarDigital Library
- Martin Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming. John Wiley and Sons. Google ScholarCross Ref
- Christian Robert and George Casella. 2013. Monte Carlo Statistical Methods. Springer Science 8 Business Media.Google Scholar
- Adrian Sampson, Pavel Panchekha, Todd Mytkowicz, Kathryn S. McKinley, Dan Grossman, and Luis Ceze. 2014. Expressing and verifying probabilistic assertions. In PLDI. ACM Press, 14. Google ScholarDigital Library
- Victor Shoup. 2009. A Computational Introduction to Number Theory and Algebra. Cambridge University Press.Google Scholar
- Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. 2016. Semantics for probabilistic programming: Higher-order functions, continuous distributions, and soft constraints. In Proc. of LICS. ACM Press, 525--534. Google ScholarDigital Library
- Henk Tijms. 2007. Understanding Probability: Chance Rules in Everyday Life. Cambridge University Press. Google ScholarCross Ref
- Daniele Varacca and Glynn Winskel. 2006. Distributing probability over non-determinism. Math. Structures Comput. Sci. 16, 1 (2006), 87--113. Google ScholarDigital Library
- Wolfgang Wechler. 1992. Universal Algebra for Computer Scientists. EATCS Monographs on Theoretical Computer Science, Vol. 25. Springer. Google ScholarCross Ref
- Herbert Wiklicky. 2016. On dynamical probabilities, or: How to learn to shoot straight. In Proc. of COORDINATION (LNCS), Vol. 9686. Springer, 262--277. Google ScholarCross Ref
Index Terms
- Conditioning in Probabilistic Programming
Recommendations
Conditioning in Probabilistic Programming
In this paper, we investigate the semantic intricacies of conditioning in probabilistic programming, a major feature, e.g., in machine learning. We provide a quantitative weakest pre-condition semantics. In contrast to all other approaches, non-...
A lambda-calculus foundation for universal probabilistic programming
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingWe develop the operational semantics of an untyped probabilistic λ-calculus with continuous distributions, and both hard and soft constraints,as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our ...
A lambda-calculus foundation for universal probabilistic programming
ICFP '16We develop the operational semantics of an untyped probabilistic λ-calculus with continuous distributions, and both hard and soft constraints,as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our ...
Comments