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

FMITF：第一轨：模块化概率编程和推理原理

• 批准号: 2220408
• 负责人: Steven Holtzen
• 金额: $ 75万
• 依托单位: Northeastern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2026-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2220408&HistoricalAwards=false
• 关键词: FMitF; Track; Principles; Modular; Probabilistic

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.

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

项目成果

Lilac: A Modal Separation Logic for Conditional Probability

Lilac：条件概率的模态分离逻辑

• DOI: 10.1145/3591226
• 发表时间: 2023
• 期刊: Proceedings of the ACM on Programming Languages
• 作者: Li, John M.;Ahmed, Amal;Holtzen, Steven
• 通讯作者: Holtzen, Steven