FMitF: Opening Up the Black Box of Probabilistic Program Inference

点击翻译按钮获取中文摘要

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.