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

SHF：中：对健全且高效的可编程推理的语言支持

• 批准号: 2311983
• 负责人: Jan Hoffmann
• 金额: $ 90万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-10-01 至 2027-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2311983&HistoricalAwards=false
• 关键词: SHF; Medium; Language; Support; Sound

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.

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