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

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

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.