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.