CAREER: SHF: Compositional Analysis of Randomized Algorithms

随机算法在包括机器学习、数据隐私和密码学在内的重要应用中发挥着核心作用。像所有的软件一样，概率程序容易受到错误的影响。此外，正确性的性质依赖于数学证明；这些参数中的错误可能导致算法在实现之前就出现错误。不管它们的来源是什么，错误可能会在数年内被忽视，随着概率程序得到更广泛的采用，它们带来的风险越来越大。本提案旨在推进概率程序验证的理论和实践，开发技术以增加我们对这些程序正确性的信心。该项目开发了一个软件系统，通过利用三个互补的思想来正式验证随机算法：(1)使用更高级别的属性，使每一步的正式证明都能覆盖更多的领域；(2)争取组合推理，通过单独分析各个组成部分来验证复杂系统；(3)形式化人类证明技术，为验证方法提供信息。在短期内，结果将使新算法得到验证。从长远来看，这一建议将朝着这样一个世界发展：在部署之前，所有随机程序都可以通过计算机检查其正确性。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Randomized algorithms play a central role in important applications, including machine learning, data privacy, and cryptography. Like all software, probabilistic programs are susceptible to bugs. Furthermore, correctness properties rest on mathematical proof; missteps in these arguments can render algorithms incorrect before they are even implemented. Regardless of their source, errors may go unnoticed for years, posing increasing risks as probabilistic programs see broader adoption. This proposal seeks to advance the theory and practice of verification for probabilistic programs, developing technology to increase our confidence that these programs are correct. This project develops a software system to formally verify randomized algorithms, by leveraging three complementary ideas: (1) Employ higher-level properties that allows formal proofs to cover more ground with each step; (2) Strive for compositional reasoning which can allow complex systems to be verified by analyzing each component separately; and (3) Formalize human proof techniques which should inform verification methods. In the near term, results will enable verification for new algorithms. In the long term, this proposal works towards a world where all randomized programs can be computer-checked for correctness prior to deployment.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.