Source-linked AI summary
Church: a language for generative models
Noah Goodman, Vikash Mansinghka, Daniel M. Roy, Keith Bonawitz, Joshua B. Tenenbaum
TL;DR
Probabilistic models are often specified informally and require hand-built inference, motivating a reusable language for stochastic generative processes. Church provides Lisp-based semantics, stochastic memoization, and generic query procedures, while illustrating applications and noting that efficient inference remains challenging.
Problem
Probabilistic models commonly require model-specific descriptions and hand-implemented inference, motivating formal, reusable stochastic programming languages.
Method
Church combines a Lisp-like language with evaluation-as-sampling semantics, stochastic memoization, and generic exact and approximate inference schemes for query.
Results
Church supports descriptions of generative processes and conditional queries, including non-parametric models, with query applicable to any Church program.
Takeaways & Limitations
Church unifies stochastic processes, expressions, and uncertain beliefs in a language that can serve both declarative and procedural roles.
Takeaways & Limitations
Efficient query remains a critical challenge because the current implementation is not yet efficient enough for typical machine learning applications.
Abstract
from arXiv · showhide
We introduce Church, a universal language for describing stochastic generative processes. Church is based on the Lisp model of lambda calculus, containing a pure Lisp as its deterministic subset. The semantics of Church is defined in terms of evaluation histories and conditional distributions on such histories. Church also includes a novel language construct, the stochastic memoizer, which enables simple description of many complex non-parametric models. We illustrate language features through several examples, including: a generalized Bayes net in which parameters cluster over trials, infinite PCFGs, planning by inference, and various non-parametric clustering models. Finally, we show how to implement query on any Church program, exactly and approximately, using Monte Carlo techniques.
1 INTRODUCTION
Church presents a universal stochastic programming language for describing generative processes and conditional queries. It aims to make probabilistic model building more formal, reusable, and compatible with generic inference techniques.
- Church is a universal language for describing generative processes and conditional queries over them.
- Its Lisp-like foundation lets expressions representing generative models be composed and abstracted arbitrarily.
- A stochastic memoizer lets separate evaluations share generative history and supports descriptions of non-parametric probabilistic models.
- Generic exact and approximate inference schemes implement query for any Church program without special-purpose inference code.
2 THE CHURCH LANGUAGE
Church is a Scheme-based stochastic language whose expressions describe generative processes through evaluation and conditional query. Its semantics uses evaluation histories and distributions, while memoization and DPmem support persistent and non-parametric stochastic structure.
- Language foundations: Church is a dynamically typed, applicative-order language based on a pure Scheme subset, with first-class procedures and expressions as values.Its expressions can represent generative processes and be composed within the language.
- Stochastic computation: Church combines stochastic primitive procedures with memoization, allowing random computations to be reused and giving memoized programs a random-world semantics.Memoization can change stochastic meaning: two calls to memoized flip return the same value, unlike ordinary independent calls.
- Evaluation semantics: Church expressions are evaluated recursively in environments, with histories recording evaluation calls and return values to define distributions over results.The probability of a finite history is determined by the probabilities of its elementary random procedure evaluations.
- Conditional inference: The query procedure extends eval by sampling from distributions conditioned on assertions, such as requiring at least one of two flips to be heads.The query result is undefined when its expression or predicate is not admissible in the environment.
- Stochastic memoization: DPmem generalizes memoization using a Dirichlet process, interpolating between memoization at a=0 and identity at a=∞.The construction is expressed directly in Church through a stick-breaking representation and is semantically well-formed for admissible procedures.
- Semantic correctness: The language's semantic foundations establish that admissible expressions define distributions and that query is well posed under stated support and non-zero-probability conditions.Theorem 2.3 precedes the paper's discussion of exact and Monte Carlo implementations of query.
3 EXAMPLE PROGRAMS
Church programs express causal models, clustered non-parametric processes, stochastic transition models, and planning problems as composable generative programs queried conditionally.
- Causal models: Church represents causal models by defining functions for causes and effects, such as rain, sprinkler activation, and grass wetness.
- Causal models: Persistent memoization makes repeated evaluations of rain, sprinkler, and grass-wetness functions consistent for the same day.
- Causal models: Conditioning on observations from other days implicitly learns unknown probability weights through a hyper-prior.
- Non-parametric clustering: Stochastically memoized beta distributions extend the model into an infinite mixture in which days co-cluster into types.
- Stochastic transition models: Church compactly specifies stochastic transition models including PCFGs, HMMs, and infinite analogs; adapted memoization yields adaptor grammars and additional models.
- Planning by inference: Planning-as-inference transforms rewards into the probability of an ultimate reward, with inference producing softmax decisions; in the red-light game, cheating declines near the goal.
4 CHURCH IMPLEMENTATION
Church implementation requires finite representations for memoization and generic methods for conditional sampling. The paper implements exact collapsed rejection sampling and approximate MCMC over computation traces, while noting important efficiency and coverage limitations.
- Implementation challenges: Memoization and query are the two implementation complications beyond evaluating ordinary lexically scoped Lisp.Memoization must avoid requiring infinite structures, while query requires sampling from the appropriate conditional distribution.
- Exact query: Collapsed rejection sampling integrates out randomness in predicates and exactly queries the infinite Gaussian-mixture model.The method accepts or rejects a value using the marginal probability that the predicate is true.
- Exact query: Church’s metacircular query implementation expresses conditional sampling as a Church program that repeatedly evaluates an expression until its predicate accepts.The implementation is presented as an ordinary Church definition using eval and query.
- Approximate query: MCMC performs stochastic local search over evaluation histories, proposing changes to elementary random returns while preserving the conditioned result.The algorithm uses computation traces, transition kernels, consistency updates, and Metropolis-Hastings acceptance.
- Approximate query: The computation trace is a directed acyclic graph linking evaluation calls with environment extensions and corresponds one-to-one with evaluation-history equivalence classes.This trace representation supports consistent proposal updates when random values change.
- Limitations: The MCMC implementation converges on the sprinkler example, but does not yet support programs using mem and remains inefficient for typical machine-learning applications.The paper also identifies chain initialization and queries across deterministic programs as challenges for future work.
5 DISCUSSION
Church’s Lisp and lambda-calculus foundation makes stochastic processes composable, self-reflective, and usable as both declarative beliefs and procedural programs. This flexibility broadens modeling possibilities but increases inference complexity and leaves efficiency as a central challenge.
- Church uses lambda calculus to represent higher-order logic, with generative processes as first-class objects rather than propositions or first-order structures.
- Its sampling-based semantics derives distributions from evaluation, distinguishing Church from approaches that define distributions directly.
- Because eval and query define Church’s meaning within Church itself, programs can contain nested queries and reason about other programs.
- Church expressions unify stochastic processes, programs, data, and uncertain beliefs, enabling models such as learned programs and agents reasoning about agents.
- Representational flexibility substantially increases inference complexity, and the current query implementation is not yet efficient enough for typical machine learning applications.
- Church aims to support model exchange, reuse, and machine execution as probabilistic models and stochastic algorithms become more intricate.