SHF: Medium: Formally Verified Compilation of Probabilistic Programs

SHF：中：概率程序的正式验证编译

基本信息

批准号：
2106559
负责人：
Jean-Baptiste Tristan
金额：
$ 96.32万
依托单位：
Boston College
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2021
资助国家：
美国
起止时间：
2021-05-01 至 2023-06-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2106559&HistoricalAwards=false
关键词：
SHF Medium Formally Verified Compilation

项目摘要

Artificial intelligence is becoming an integral part of society, and is poised to affect increasingly many aspects of life. Like any other software, artificial-intelligence applications can have errors with potentially serious consequences. As a result, improving the quality of artificial-intelligence software is a critical challenge. One promising technology for addressing this challenge is the use of probabilistic programming languages, which let programmers implement artificial-intelligence applications in a simpler and safer way. The focus of this project is to develop techniques and tools to transform probabilistic programs into code executable on a computer. More specifically, the aim is to understand how to make such tools free of errors while being as efficient as possible.This project develops a verified compiler and runtime for the Stan probabilistic programming language. The compiler is developed in the Coq proof assistant, and connects to CompCert, an existing verified compiler for C programs. Programs written in Stan will be compiled to CompCert C through a succession of transformations, each of which handles a specific feature of Stan. These program transformations are specific to probabilistic programming languages, and include truncating distributions and re-parameterizing to support constraints on random variables. The runtime implements a Markov Chain Monte Carlo algorithm that uses the compiled program to perform inference. The formal proof defines the semantics of the Stan program as a probability measure and shows that the compiled program asymptotically generates samples from this measure.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.

人工智能正在成为社会不可或缺的一部分，并将影响生活的方方面面。与任何其他软件一样，人工智能应用程序可能会出现错误，从而造成潜在的严重后果。因此，提高人工智能软件的质量是一项严峻的挑战。解决这一挑战的一项有前景的技术是使用概率编程语言，它可以让程序员以更简单、更安全的方式实现人工智能应用程序。该项目的重点是开发将概率程序转换为计算机上可执行代码的技术和工具。更具体地说，目的是了解如何使此类工具没有错误，同时尽可能高效。该项目为 Stan 概率编程语言开发经过验证的编译器和运行时。该编译器是在 Coq 证明助手中开发的，并连接到 CompCert，这是一个现有的经过验证的 C 程序编译器。用 Stan 编写的程序将通过一系列转换编译为 CompCert C，每个转换处理 Stan 的特定功能。这些程序转换特定于概率编程语言，包括截断分布和重新参数化以支持对随机变量的约束。运行时实现了马尔可夫链蒙特卡罗算法，该算法使用编译的程序来执行推理。正式证明将 Stan 程序的语义定义为概率度量，并表明编译的程序渐近地从该度量生成样本。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响进行评估，被认为值得支持审查标准。