FMitF: Track I: Principles for Modular Probabilistic Programming and Inference

模型的概念是机器学习领域的核心：它是世界的简化表示，有助于自动推理和学习。设计这些模型是任何机器学习项目的关键部分，并且迫切需要工具，使该领域的从业者更容易、更快速地将机器学习应用于不断扩大的应用程序。概率编程语言（ppl）是对这一迫切需求的回答：它们赋予了一种典型的编程语言操纵和推理概率分布的能力，使那些不太熟悉机器学习标准工具和技术的软件开发人员能够建立自己的机器学习模型。然而，今天在ppp中编程仍然非常困难，即使对于经验丰富的程序员也是如此。这个项目解决了当今ppp的一个主要缺点：缺乏强大的模块化概念。模块化是设计可伸缩和高效软件系统的关键属性。该项目的影响是为可扩展和模块化概率编程语言开发新的基础，使更广泛的受众能够创建和维护机器学习和人工智能模型，从而改变当今机器学习模型的开发和部署方式。这个项目的新颖之处在于：(1)开发了一种名为ModPPL的新PPL，使程序员能够开发模块化机器学习模型；(2)创建大规模ModPPL程序的新方法。这个项目的主要目标是开发一组新的ppp，这些ppp具有丰富的通用模块化概念。要做到这一点，需要将形式化方法中的技术深度整合到语言的基础中。该方法的核心将是一种新的分离逻辑，用于指定概率程序的独立性结构。研究者将把这种逻辑整合到ModPPL中，借用Hoare类型理论的思想；在这样做的过程中，类型系统本身将获得必要的结构，使程序员能够对他们的程序进行本地推理。接下来，将利用该类型系统的结构来声明和验证异构推理算法的正确性标准，并进一步利用它来设计新的、更具可扩展性的异构推理策略。最后，类型系统将通过使其具有成本意识而得到丰富。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The concept of a model is central to the field of machine learning: it is a simplified representation of the world that facilitates automated reasoning and learning. Designing these models is a critical part of any machine-learning project, and there is a pressing need for tools that make it easier and faster for practitioners in the field to apply machine learning to a relentlessly broadening set of applications. Probabilistic programming languages (PPLs) are an answer to this pressing need: they endow a typical programming language with the ability to manipulate and reason about probability distributions, empowering software developers who are less comfortable with the standard tools and techniques of machine learning with the ability to make their own machine-learning models. However, programming in PPLs today remains very difficult, even for experienced programmers. This project tackles one of the main shortcomings of today's PPLs: a lack of strong notions of modularity. Modularity is a critical property for designing scalable and efficient software systems. This project's impact is to develop a new foundation for scalable and modular probabilistic programming languages that empower a broader audience to create and maintain machine learning and AI models, transforming the way machine learning models are developed and deployed today. This project's novelties are (1) the development of a new PPL called ModPPL that enables programmers to develop modular machine learning models; and (2) new methods for creating large-scale ModPPL programs.The primary aim of this project is to develop a new family of PPLs with a rich and general-purpose notion of modularity. Accomplishing this will require deeply integrating techniques from formal methods into the foundations of the language. The core of the approach will be a new separation logic for specifying the independence structure of probabilistic programs. The investigators will integrate this logic into ModPPL, borrowing ideas from Hoare Type Theory; in doing so, the type system itself will capture the necessary structure to empower programmers to reason locally about their programs. Next, the structure of this type system will be leveraged to state and certify correctness criteria for heterogeneous inference algorithms, and further leveraged to design new and more scalable heterogeneous inference strategies. Finally, the type system will be enriched by making it cost-aware.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.