A common way to interpret the results of any computational model is to visualize its output. For probabilistic programming, this often means visualizing a posterior probability distribution. The webppl language has a visualization library called webppl-viz that facilitates this process. A useful feature of webppl-viz is that it does some amount of automatic visualization—the user simply passes in the posterior and the library tries to construct a useful visual representation of it.… Read the rest
Monthly Archives: December 2016
Some of the fundamental errors that occur in probabilistic programs are due
to incorrect statistical models, ignoring dependence between random variables,
or, using wrong hyper-parameters (such as sample size) for inference. To prevent these errors, the solution most probabilistic programming languages adopt is to keep inference external to the core language semantics.… Read the rest
Okay, this isn’t really semantics, just a simple way to use ordinary invariants to reason about probabilistic transition systems (or programs). The trick is to to prove invariants of the form M + L >= 0, where L (“luck”) is a linear combination of “gambling balance” ghost variables that are initially 0 and are only updated with (state-dependent) fair bets on probabilistic choices.… Read the rest
Joint work with Nathan Bowler.
There’s a well-known monad (on Set) for probabilistic choice – the probability distribution monad. And there’s a well-known monad for I/O – the free monad on a signature (set of operations). We’ve developed a new monad for the combination of probabilistic choice and I/O using trace semantics. … Read the rest
We continue our previous work  on giving semantics to probabilistic programs using computable distributions. First, we highlight a gap in our previous semantics involving the measurability of an environment lookup function and address it. Second, we suggest topological domains, a category of domains proposed in the literature that supports both Type-2 computability and domain-theoretic constructions, as an alternative to DCPOs in giving semantics to probabilistic programs based on computable distributions.
Exchangeable sequences are models for homogeneous data sets and serve as building blocks from which more interesting dependency structures in statistical models are produced. A sequence of random variables is exchangeable when its distribution does not depend on the ordering of its elements.… Read the rest
Skorohod’s Theorem is a fundamental result from stochastic process theory. It makes two assertions:
- Any Borel probability measure on a Polish space can be realized as for some random variable , where denotes Lebesgue measure and is the “law of ,” the push forward of under .
Generative modeling languages, i.e., probabilistic programming languages (PPLs), offer only limited support for continuous variables; theorems concerning semantics and algorithmic correctness are often limited to discrete variables or, in some cases, bounded continuous variables.
We show natural examples that violate these restrictions and break standard algorithms.… Read the rest
The design of a general probabilistic programming system involves a balancing act between two deeply conflicting concerns. On the one hand, the system should provide as uniform and flexible an interface for specifying models as possible; on the other, it should be capable of doing efficient inference for any particular model specified.
We propose a weakest-precondition-style calculus for reasoning about the expected values (pre-expectations) of mixed-sign unbounded random variables after execution of a probabilistic program. The semantics of a while-loop is well-defined as the limit of iteratively applying a functional to a zero-element just as in the traditional weakest pre-expectation calculus, even though a standard least fixed point argument is not applicable in this context.… Read the rest