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.