Making our Own Luck: A Language for Writing Random Generators

QuickCheck-style property-based random testing requires efficient generators for well-distributed random data satisfying complex logical predicates.  Writing such generators by hand can be difficult and error prone.

We propose a domain-specific language, Luck, in which generators are expressed by decorating predicates with lightweight annotations controlling both the distribution of generated values and the amount of constraint solving that happens before each variable is instantiated.  Generators in
Luck are compact, readable, and maintainable, with efficiency close to custom handwritten generators.

We give a precise denotational semantics for Luck, reminiscent of those of probabilistic programming languages, and prove key theorems about its behavior, including the soundness and completeness of random generation with respect to a straightforward predicate semantics.  We evaluate Luck on a collection of common examples from the random testing literature and on two significant case studies showing how Luck can be used for complex bug-finding tasks with comparable effectiveness and an order of magnitude reduction in testing code size, compared to handwritten generators.

Extended Abstract: Making Our Own Luck

Slides: LuckSlides

by Leonidas Lampropoulos, Benjamin C. Pierce, Cătălin Hriţcu, John Hughes, Zoe Paraskevopoulou and Li-yao Xia

Posted in Uncategorized | Comments Off on Making our Own Luck: A Language for Writing Random Generators

eXchangeable Random Primitives

In our view, one of the key contributions of the probabilistic programming language Church is a class of constructs, called exchangeable random primitives (or XRPs for short), that can be used to extend the language with stochastic primitives whose implementations use stateful computation.

Surprisingly, XRPs are not mentioned in the paper introducing the language [GMRBT08] and are buried in the original implementation, dubbed MIT-Church. Despite being reimplemented and generalized in several languages descending from Church, XRPs are poorly documented and, as a result, poorly understood.

XRPs are built from three components: a sampler, an unsampler, and a scorer. We give a rigorous definition for the samplers of XRPs, and give a representation theorem characterizing their essential form and conditional independence structure. A formalization like the one we provide could serve as part of a foundation for deriving a semantics for Church programs with XRPs. A formalization of all three components of XRPs — including the unsampler and scorer — would be necessary to prove the correctness of the MCMC Church algorithm in the presence of XRPs. We highlight some challenges associated with formalizing the scorer. (We also have some ideas for circumventing these obstacles that do not appear in the paper but that we would be happy to discuss.) We are also looking forward to discussing semantic questions surrounding XRPs, especially those involving purity and referential transparency, and would be interested to learn of other possible connections between XRPs and the PL theory literature.

Extended abstract: eXchangeable Random Primitives by Nathanael L. Ackerman, Cameron E. Freer, and Daniel M. Roy

Related work by the authors:

[FR10] C. E. Freer and D. M. Roy. Posterior distributions are computable from predictive distributions. In: Proc. 13th Int. Conf. on Artificial Intelligence and Statistics (AISTATS 2010). Vol. 9. J. Machine Learning Research W&CP. 2010.

[FR12] C. E. Freer and D. M. Roy. Computable de Finetti measures. Ann. Pure Appl. Logic 163.5 (2012), pp. 530–546.

[GMRBT08] N. D. Goodman, V. K. Mansinghka, D. M. Roy, K. Bonawitz, and J. B. Tenenbaum. Church: A language for generative models. In: Proc. 24th Conf. on Uncertainty in Artificial Intelligence (UAI 2008). Corvalis, Oregon: AUAI Press, 2008, pp. 220–229.

[RMGT08] D. M. Roy, V. K. Mansinghka, N. D. Goodman, and J. B. Tenenbaum. A stochastic programming perspective on nonparametric Bayes. Nonparametric Bayesian Workshop, Int. Conf. on Machine Learning. 2008.

Posted in Uncategorized | Comments Off on eXchangeable Random Primitives

Models for Probabilistic Programs with an Adversary

While working on a Hoare logic for probabilistic programs [1], we encountered an interesting choice for how to define the operational semantics of the underlying probabilistic imperative language PRIMP. We could either define commands as mapping from states to states and then “lift” those commands to apply to distributions, or define those commands over state distributions as a whole. Consider, for example, the conditional if b then c1 else c2. We could either apply this to all the states in the distribution’s support, where b would evaluate to true or false, or we could apply c1 to the entire sub-distribution where b was true and c2 to the complementary sub-distribution. We showed in our Coq development that both approaches were equivalent. Interestingly, when we looked at the non-deterministic choice c1 ⊔ c2 this wasn’t true at all. If we reduced c1 ⊔ c2 to c1 or c2 for the whole distribution, we restricted the non-determinism from reacting to the random events that had already occurred. And this allowed us to verify many properties that wouldn’t hold if we reduced c1 ⊔ c2 at the state level.

We soon realized that the distinction between these evaluation strategies corresponded to the distinction between the Arthur-Merlin (AM) and Interactive Polynomial (IP) complexity classes. AM uses public coins, meaning that the adversary knows the outcome of every random event. By contrast, in IP the hidden coins are used to thwart the prover, as in the simple protocol for verifying that two graphs are non-isomorphic by asking the prover to identify which of the graphs was randomly selected.

It turns out that there are a variety of interesting operational semantics for programs combining probability and non-determinism (we’ve identified eight so far) which are appropriate for domains ranging from security to game theory. All of these can be thought of as encoding what information is available to a non-deterministic adversary. We identified a few of these models in a recent ICFP poster competition.

Five different models of adversary strength.
Five different models of adversary strength.

Which raises two questions: Which models are worth exploring in detail and how many are we missing?

Models for Probabilistic Programs with an Adversary: Extended Abstract, Slides

Robert Rand and Steve Zdancewic, University of Pennsylvania

[1] Rand, R. and S. Zdancewic, “VPHL: A verified partial-correctness logic for probabilistic programs”, Mathematical Foundations of Programming Semantics, 2015.

Posted in Uncategorized | Tagged , , | Comments Off on Models for Probabilistic Programs with an Adversary

Reproducing kernel Hilbert space semantics for probabilistic programs

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

Posted in Uncategorized | Tagged | Comments Off on Reproducing kernel Hilbert space semantics for probabilistic programs

Fixed Points for Markov Decision Processes

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

Posted in Uncategorized | Tagged | Comments Off on Fixed Points for Markov Decision Processes

An application of computable distributions to the semantics of probabilistic programs

Our attempt to give semantics to a core, functional probabilistic programming language uses computable distributions. The semantics uses largely standard techniques from denotational semantics. One nice property of computable distributions is that they are completely characterized by a sampling algorithm. Hence, it is possible to faithfully implement (in a Turing-complete language) a semantics based on computable distributions as a sampling library. We are interested in the pros and cons of using computable distributions as opposed to measure theory in giving semantics to probabilistic programming languages.

This is joint work with Greg Morrisett.

comp_sem

Posted in Uncategorized | Comments Off on An application of computable distributions to the semantics of probabilistic programs

Parameterized probability monad

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

Posted in Uncategorized | Tagged | Comments Off on Parameterized probability monad

Semantics of Higher-order Probabilistic Programs

For about an year or so, we have been working on the semantics of higher-order probabilistic programming languages that support continuous distributions, such as Church, Venture and Anglican. Our goal was to verify the correctness of program optimisations that we developed for Anglican, and to understand unusual programming concepts in Anglican, such as nested query and distribution object. Defining the semantics of such a language turns out to be very challenging because the combination of higher-order functions and continuous distributions poses a nontrivial technical problem. In order to handle continuous distributions properly, we need to use tools from measure theory, but the standard setting of measure theory lacks a proper notion of function space: the category of measurable spaces is not cartesian closed. After a lot of struggles with this problem, we learnt that abstract tools from category theory can be used to resolve this problem and to lead to a semantics of a call-by-value higher-order probabilistic programming language with continuous distributions. Our two-page abstract below contains a summary of our findings. We plan to (and hope to) give a more accessible presentation of the work in PPS’16.

This is joint work with Sam Staton, Chris Heunen, Ohad Kammar and Frank Wood.

The abstract is available here: semantics-higher-order-ppl

Posted in Uncategorized | Comments Off on Semantics of Higher-order Probabilistic Programs

Reasoning about Probability and Nondeterminism

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)

Posted in Uncategorized | Tagged | Comments Off on Reasoning about Probability and Nondeterminism

On The Semantic Intricacies of Conditioning

We discuss semantic intricacies of conditioning, a main feature in probabilistic programming, and propose how to deal with these issues in an operational way and in a weakest pre-condition semantics. This includes the interplay between conditioning and possible non-termination as well as between conditioning and non-determinism.
Furthermore, we propose a program transformation that eliminates conditioning from programs at the expense of introducing loops.

Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Federico Olmedo (RWTH Aachen University)

On The Semantic Intricacies of Conditioning (Extended Abstract, PDF)

Conditioning in Probabilistic Programming (Technical Report, PDF)

Posted in Uncategorized | Comments Off on On The Semantic Intricacies of Conditioning