Programmable MCMC with Soundly Composed Guide Programs
summary
Implements a coroutine-based framework and a type system that encodes the message protocol between a model program and a sequence of block-wise guide programs, translates guide types to context-free processes with finite norms, and leverages a 1994 decidability result to achieve polynomial-time structural equality checks. Adds a coverage-checking algorithm that statically verifies every latent variable is freshly sampled in the guide composition; evaluation on prior benchmarks shows fast type inference and detection of unsound guides for finite-state cases but notes possible false negatives when guide types have infinite state spaces. Artifacts and reproduction data are provided.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 1:45Bayesian polynomial regression
- 3:30Limitations of inference
- 4:36Blockwise Metropolis-Hastings
- 6:42BMH soundness condition
- 7:47Static verification of BMH
- 8:30Sequential composition
- 12:29Type equality check
- 13:32Guide program coverage
- 15:37Implementation results
- 17:01Summary
- 17:47Q&A
related talks
23mType-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortize...
14mSequential Monte Carlo Program Synthesis with Refinement Proposals
12mLanguage-Model Probabilistic Programming for Improving Autoformalization via Cycle(…)
20mProbabilistic Programming with Stochastic Probabilities
11mEffective Sequential Monte Carlo for Language Model Probabilistic Programs
19mIncremental Computation for Efficient Programmable Inference in Probabilistic Programs
49mSemantic Foundations for Probabilistic Programming
16mJust-in-Time Learning for Bottom-Up Enumerative Synthesis