EAGER: A Measure Theory Semantics of Probability Theory

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

Bayesian probability is an important theory of robust decision making. Domains as diverse as physical science, engineering, medicine, and law have applied Bayesian inference successfully. Nevertheless, Bayesian inference is fraught with problems during practical development and deployment. The standard techniques used to construct the implementations are semantically far from the "whiteboard presentation" (mathematical description), are untrustworthy, and expensive to apply. This research addresses this problem by providing an axiomatic foundation with a built-in approximation system that can verify implementations. This research develops an automatic, trustworthy compiler from the whiteboard math used in the development of a theory to an efficient inference model implementation ready for evaluation. This environment provides compilation to a measure-theoretic model of the theory and to an efficient implementation that is provably connected to the measure-theoretic model. This compilation technique delays approximation as long as possible to achieve correctness and allow varied options for approximation, including the use of a novel algorithmic sampling technique, and performs high-powered optimization to compile them to parallelized implementations.