SHF: Medium: Formally Verified Compilation of Probabilistic Programs

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

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.