Bayesian Separation Logic

on YouTube ↗23m

" summary

Introduces a separation logic that actually models Bayesian updating and scoring, proving an internal Bayes' theorem by invoking the Rokhlin‑Simmons disintegration result and constructing semantics over σ‑finite measure spaces (Hilbert cube) compatible with s‑finite kernels. Provides axioms for observe/score and a conditional sampling rule, uses them to derive Beta posteriors and show the coin‑flip program has expected value 1/2, proves conditional dependence examples, and verifies posterior/estimation results for burglar‑alarm and Gaussian mixture models.

AI-written summary · about

" chapters (12)

1. 0:00Introduction
2. 1:06Goal of probabilistic separation logic
3. 3:59Probabilistic programming example
4. 6:12Syntax and semantics of PSL
5. 7:55Bayesian separation logic features
6. 9:24Proof rules for sampling and observation
7. 12:18Proving expected value of a program
8. 14:48Conditional dependency and correlation
9. 16:35Semantics of probabilistic separation logic
10. 18:00Internal base theorem explanation
11. 19:27Conclusion and future work
12. 20:23Q&A