SHF: Medium: Language Support for Sound and Efficient Programmable Inference

该项目的目标是使强大的贝叶斯模型和推理算法在具有挑战性的数据科学问题中更可用、更易于访问和更可靠。贝叶斯推理通过将先前的建模假设与观测数据相结合，提供了一种原则性的方法来学习概率模型。它使生物统计学、机器人、计算物理、定量金融、认知科学和机器学习等不同领域的问题得到最先进的结果。贝叶斯推理的优点包括能够整合先前的特定领域知识，量化参数和预测的不确定性，以及很好地推广到新数据。然而，一个关键的挑战是正确实现和诊断贝叶斯推理算法，特别是那些针对复杂概率模型的算法。该项目的新颖之处在于，通过开发严格的编程语言技术来解决这一挑战，使可靠有效的贝叶斯推理更容易应用。该项目的影响是促进研究人员对更灵活的贝叶斯方法的开发和探索，并帮助领域专家更可靠地利用这些技术解决现实问题。该项目的研究计划建立在概率编程语言（ppl）的基础上，如Stan、Gen和Pyro，这些语言提供的接口将模型开发与相应推理算法的规范清晰地分离开来。为了使贝叶斯学习适用于更灵活的模型和更大的数据集，一些ppp允许用户通过“可编程推理”接口编写自定义概率推理算法，该接口自动执行开发有效推理算法所需的许多复杂计算。然而，用户很容易意外地编写不正确的推理程序，从而破坏收敛并导致不可靠的结果。更糟糕的是，这样的错误常常被忽视。本项目的研究旨在通过以下方式缓解可编程推理的稳健性和灵活性之间的根本紧张关系：(1)应用新的编程语言技术，如静态分析和类型系统，来验证用户编写的推理程序是否满足稳健性的理论条件；(2)开发新的动态统计程序分析，以经验评估由声音推理程序产生的近似后验样本的质量。通过这种方式，系统保证了近似推理算法不仅可以很好地实现，而且在实践中对于给定的问题是有效的。通过对具有挑战性的数据科学问题的评估，验证了所开发技术的实用性。并将研究成果整合到卡内基梅隆大学的研究生和本科教育中。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The goal of this project is to make powerful Bayesian models and inference algorithms more usable, accessible, and reliable in challenging data science problems. Bayesian inference provides a principled approach to learning probabilistic models by combining prior modeling assumptions with observed data. It enables state-of-the-art results in problems from diverse areas including biostatistics, robotics, computational physics, quantitative finance, cognitive science, and machine learning. Advantages of Bayesian inference include the ability to incorporate prior domain-specific knowledge, to quantify uncertainty about parameters and predictions, and to generalize well to novel data. A key challenge, however, is correctly implementing and diagnosing Bayesian inference algorithms, especially those that target sophisticated probabilistic models. The project's novelty is to address this challenge by developing rigorous programming-language techniques that make sound and effective Bayesian inference more easily applicable. The project's impact is to boost the development and exploration of more flexible Bayesian methods among researchers and help domain experts more reliably leverage these technologies for real-world problems.The research plan of the project builds on probabilistic programming languages (PPLs) such as Stan, Gen, and Pyro, which provide interfaces that cleanly separate model development from the specification of the corresponding inference algorithm. To make Bayesian learning feasible for more flexible models and larger data sets, several PPLs have enabled users to write custom probabilistic inference algorithms through "programmable inference" interfaces that automate many complex computations needed to develop effective inference algorithms. However, it is easily possible for users to accidentally write incorrect inference programs in such a way that breaks convergence and leads to unsound results. Even worse, such mistakes often go unnoticed. The research in this project aims to alleviate the fundamental tension between soundness and flexibility of programmable inference by (1) applying new programming-language techniques such as static analysis and type systems to verify whether a user-written inference program satisfies theoretical conditions for soundness; and (2) developing new dynamic statistical program analyses to empirically assess the quality of approximate posterior samples produced from the sound inference program. In this way, the system ensures that approximate inference algorithms are not only soundly implemented but are also effective for a given problem in practice. The practicality of the developed techniques is validated through evaluations on challenging data science problems. Moreover, the research results are integrated in the graduate and undergraduate education at Carnegie Mellon University.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.