SHF: Small: Semantics of Higher Order Probabilistic Programs

点击翻译按钮获取中文摘要

Probabilistic programming is a powerful programming paradigm that focuses on the use of randomness to model uncertainty. The topic has enjoyed a recent resurgence of interest spurred by new applications in machine learning and statistical analysis of large datasets. Several new probabilistic programming languages such as Church, Anglican, and Venture have emerged in the last few years that allow statisticians to construct statistical models, sample probability distributions, condition on events, and perform Bayesian inference. The rapid development of these languages has created a need for sound semantic foundations and logical tools for specification and reasoning about probabilistic program behavior. Describing the behavior of probabilistic programs with higher-order features and mechanisms for sampling and conditioning presents enormous mathematical challenges. A variety of diverse mathematical structures for capturing the most salient properties of these languages have recently been proposed, similar in spirit but diverging markedly in execution. The objective of this project is to isolate the fundamental principles at work in each case and ultimately determine whether and how these diverse approaches can be reconciled. The project investigates useful semantic and logical tools to guide the future development of probabilistic languages and logics. The project provides fundamental knowledge and insights that will inform the design of next-generation higher-order probabilistic programming languages with conditioning and Bayesian inference, along with compiler technology and runtime support for these languages. The research results and software artifact from this project will be made publicly available. The project personnel will organize two annual summer research workshops, and participate by giving introductory lectures on probabilistic programming and Bayesian inference, and supervise followup projects with interested students.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.