We identify two problems with Wingate et al. lightweight implementation technique for probabilistic programs.  Simple examples demonstrate that common, what should be semantic-preserving program transformations drastically alter the program behavior. We briefly describe an alternative technique that does respect the program refactoring.  There remains a question of how to be really, formally sure that the MCMC acceptance ratio is computed correctly.

Lightweight Problems (extended abstract)

We extend a stream-processing programming language, whose denotational semantics is given using the domain of streams, so that it can support probabilistic action.  We give a denotational semantics to the extended language (which we call SProcP).  We take the domain of probability distributions over streams as the denotational domain; it constitutes a cpo according to Saheb-Djaromi [3].

This work is motivated by the second author’s recent hybrid-system verification work [4].  In this work, we used nonstandard analysis [1] to the denotational semantics of a stream-processing language so that it accommodates infinitesimal values.  The extended language can express continuous signals and computation on them.  We plan to do the same extension to the current language to obtain a language for processing probabilistic continuous-time signal.

The extension is for the most part straightforward.  A tricky part is the denotation of binary operations e1 + e2.  Since the denotation of the expressions e1 and e2 are in general not independent from each other, we cannot write define its denotation using those of e1 and e2.  Our current definition is to assume an opaque function that gives a joint distribution of the denotations of e1 and e2.  If we can reason that e1 is independent from e2 (by some program analysis), the denotation of e1 + e2 can be given in more explicit way.

Our apology that we have not revised our contribution to reflect the reviewers’ valuable comments yet.  We may post an updated version later.

(On Jan. 17, 2016) We have uploaded the (slightly) revised version. PDF

PDF

Poster: posterMiyamotoSuenagaNakazawa

[3] N. Saheb-Djahromi. Cpo’s of measures for nondeterminism. Theor. Comput. Sci., 12:19–37, 1980.

This is an abstract of a poster by Larry Moss,  and Chung-chieh Shan, and Alexandra Silva. The one sentence summary of our proposal is to adapt ideas from coalgebraic semantics to the probabilistic setting, thereby obtaining intuitive semantics for probabilistic processes of various sorts. measures.

We propose to write denotational semantics for a probabilistic programming language in terms of reproducing kernel Hilbert spaces for characteristic kernels. This opens up possibilities for providing convergence guarantees for approximate expansions, as well as practical advantages of using kernel methods for machine learning. At the moment we only write semantics for a simple language for probabilistic expressions, but with time we hope to extend it to general probabilistic programs with conditioning.

Adam Ścibior and Bernhard Schölkopf

Extended abstract

The goal of this paper is to advertise the application of fixed points and $latex \omega$-complete partial orders ($latex \omega$-cpos) in the formalization and analysis of probabilistic programming languages. The presented work is formalized in the Isabelle theorem prover.

By applying $latex \omega$-cpos to the analysis of MDPs we get a nice theory of fixed points. This allows us to transfer least and greatest fixed points through expectation on Markov chains and maximal and minimal expectation on MDPs. One application is to define the operational semantics of pGCL by MDPs, e.g. relating the denotational and operational semantics of pGCL is now a matter of fixed point equations and induction.

Fixed Points for Markov Decision Processes

Note: After acceptance I discovered that large parts of the presented work were already developed by Monniaux [1]. Still, the main contribution of the presented work is the formalization in the interactive theorem prover Isablle/HOL.

[1] David Monniaux: Abstract interpretation of programs as Markov decision processes

We explore the use of parameterized monads for ensuring additional properties of distributions constructed by probabilistic programs. As a specific example we demonstrate how to statically ensure that conditioning in probabilistic programs does not depend on random choices made during execution. This allows us to ensure safety of application of inference algorithms such as Sequential Monte Carlo. We believe there are more potential uses of parameterized monads for probabilistic programming, such as restricting the latent space or keeping track of data types used for conditioning.

Adam Scibior and Andrew D. Gordon

Extended abstract

Probabilistic and nondeterministic choice are two standard examples of computational effect, and it is important for some problems to be able to use them in combination — for example, to model probabilistic systems that depend on nondeterministic inputs. However, the algebraic properties that characterise their interaction are tricky to get right (and we have ourselves got them wrong in the past).

We outline the problem, and present a technique for diagrammatic reasoning about the properties of probability and nondeterminism combined. It turns out to be a matter of linear algebra. We are curious to know whether others find the diagrammatic notation helpful, and whether there are other applications of it.

Reasoning about Probability and Nondeterminism, by Faris Abou-Saleh, Kwok-Ho Cheung, and Jeremy Gibbons, University of Oxford

Diagrammatic Reasoning about Probability and Nondeterminism (poster)

In probabilistic programming languages, model construction and inference are separate tasks. The former is done by the language users and the latter by the language developers. Unfettered by concerns about inference, modelers will want to create big, complex probabilistic programs, which will present familiar problems: Models may become too big to comprehend, debug or validate as wholes. Users building large applications will need to divide and coordinate work among several people and will need to reuse common elements of models without rebuilding them. We hypothesize that model creation will benefit from two linguistic tools that have proven helpful in deterministic programming: types and modules.

With Insomnia, we hope to provide the best of two worlds: to help with the “democratization of machine learning,” we provide a language with abstractions for modular development of complex probabilistic programs. To help with analysis and understanding of models’ properties, we define the meaning of modular models by elaborating them into a small (module-free) core calculus whose semantics may be studied further.

Extended Abstract (PDF)

Insomnia (prototype and examples)

Aleksey Kliger and Sean Stromsten

We define a core calculus for the purpose of investigating reasoning principles of probabilistic programming languages. By using a variation of a technique called higher-order abstract syntax (HOAS), which is common in the implementation of domain-specific languages, the calculus captures the semantics of a stochastic language with observation while being agnostic to the details of its deterministic portions. By remaining agnostic to the non-stochastic portions of the language, this style of semantics enables the discovery of general reasoning principles for the principled manipulation of probabilistic program fragments by programmers, compilers, and analysis tools. This generality allows us to reason about probabilistic program fragments without the need to resort to the underlying measure theory in every instance, by instead enabling reasoning in terms of the core calculus in a way that we believe to be applicable to various surface-level languages.

Extended abstract (PDF)

Theo Giannakopoulos (BAE Systems) and Mitchell Wand & Andrew Cobb (Northeastern University)

(more…)