Bit Blasting Probabilistic Programs
summary
Presents a new discretization called bit blasting that encodes continuous variables as Boolean bits so a domain of 2^b points becomes a discrete program over poly(b) Boolean variables; shows mixed gamma families (uniform, exponential, gamma, Laplace) admit exact bit-blast encodings (e.g., 2^32 uniform points via 32 biased coin flips) that compile to BDDs of polynomial size and support polytime inference. Implements the idea in HyBit (open source) and beats prior samplers and symbolic tools on 11/19 benchmarks within a 20-minute timeout.
AI-written summary · about
chapters (23)
- 0:00Probabilistic programming intro
- 0:21Speaker and session overview
- 0:44Probabilistic programming languages
- 1:26Hybrid probabilistic programs
- 2:10Inference challenges for hybrids
- 3:11Sampling inference limitations
- 3:53Symbolic inference approaches
- 4:15Hybd PPL and bit blasting
- 5:19Discretization trade-offs
- 6:01Bit blasting solution
- 7:06Bit blasting distributions
- 7:48Polynomial-time inference
- 8:09Hybd PPL system
- 8:50Succinct mixed gamma representation
- 10:15Uniform distribution example
- 10:36Exponential distribution bit blasting
- 11:17Gamma distribution bit blasting
- 12:43Knowledge compilation for inference
- 13:28Polynomial-size BDDs
- 14:33Hybrid PPL API
- 15:18Benchmark results
- 15:39Conclusion
- 16:26Q&A
related talks
30mBit-Precise Reasoning via Int-Blasting
13mInteractive Bit Vector Reasoning using Verified Bitblasting
05mOn Iteration in Discrete Probabilistic Programming
06mStatic Delayed Sampling for Probabilistic Programming Languages
19mPanel: Compilation Frameworks
13mProgram Analysis via Efficient Symbolic Abstraction
15mPolynomial Bounds of CFLOBDDs against BDDs
14mFast and Efficient Bit-Level Precision Tuning