FMitF: Opening Up the Black Box of Probabilistic Program Inference

概率编程语言是一种用于创建、维护和理解广泛的机器学习模型的表达方式，它们已经被研究人员和主要技术公司成功使用。然而，今天的概率编程语言对它们有效的程序类型施加了强烈的限制，从而排除了它们在许多机器学习应用程序中的使用。为了开发概率推理的通用算法，该项目采用并推广了形式方法界对传统程序进行推理的技术，这是概率编程语言必须执行的关键任务。该项目正在一种新的命令性概率编程语言的背景下实现这些算法，并为研究生、本科生和高中生在新兴的概率编程领域提供教育机会。该项目有三个主要的技术推动力。首先，该项目正在通过利用与符号模型检查和加权模型计数技术的联系来开发离散概率程序的精确推理算法。其次，该项目正在开发技术，将一个概率推理查询自动分解为多个更简单的子查询，每个子查询都可以使用最合适的推理方法来解决。这种分解的关键推动因素是一种新的概率程序抽象过程。第三，该项目正在研究使用抽象作为建议分布进行概率推理，从而产生新的抽象制导的近似推理算法。该项目的结果将使概率编程更有效，使概率推理和学习易于处理，适用于更广泛的程序类别。这项研究的成果将开源发布，包括一种新的概率编程语言，它利用了新开发的推理技术。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Probabilistic programming languages are an expressive means for creating, maintaining, and understanding a wide range of machine-learning models, and they have been successfully used by both researchers and major technology companies. However, today's probabilistic programming languages impose strong limitations on the kinds of programs for which they are effective, thereby precluding their use for many machine-learning applications. This project adapts and generalizes techniques from the formal methods community for reasoning about traditional programs, in order to develop general-purpose algorithms for probabilistic inference, which is the key task that a probabilistic programming language must perform. The project is implementing these algorithms in the context of a new imperative probabilistic programming language and is providing educational opportunities in the burgeoning area of probabilistic programming for graduate, undergraduate, and high-school students.This project has three main technical thrusts. First, the project is developing exact inference algorithms for discrete probabilistic programs by exploiting the connection to techniques for symbolic model checking and weighted model counting. Second, the project is developing techniques to automatically decompose a probabilistic inference query into multiple simpler sub-queries, each of which can be solved using the most appropriate inference method. The key enabler of this decomposition is a novel abstraction process for probabilistic programs. Third, the project is investigating the use of abstractions as proposal distributions for probabilistic inference, resulting in new abstraction-guided approximate inference algorithms. The results of this project will make probabilistic programming more effective by making probabilistic inference and learning tractable for a wider class of programs. The artifacts that result from this research will be released open source, including a new probabilistic programming language that leverages the newly developed inference techniques.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.