权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。