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.
