CRII: SHF: Abstract Interpretation of Probabilistic Programs

This project aims to improve the practice of verifying probabilistic programs. Probabilistic programs are a way of capturing randomized behavior using the same kinds of structures we use for regular programming. This kind of randomness is a key component of many machine learning algorithms, so probabilistic programs are an important tool for building safer, more robust machine learning systems. However, techniques for verifying that probabilistic programs behave safely are under-studied compared to traditional deterministic programs. This project's novelties are improved tools for verification of probabilistic programs, allowing more properties to be verified for a larger set of programs. This project's impacts are improved safety and reliability for systems which include probabilistic programs and ultimately for systems with machine learning components. The project will support student learning by providing the undergraduate students working in the project with high-demand skills such as software verification. Concretely, this project builds on the framework of abstract interpretation, an existing methodology for verifying traditional programs. While there has been some work in extending abstract interpretation to probabilistic programs, that work has various drawbacks making it infeasible for analyzing complex programs. This project will develop novel abstract domains for verifying programs with complex, continuous probability distributions modeled by traditional programming constructs. Such problems arise naturally in (for example) continuous control settings. The project aims to equip these domains with the order-theoretic operators required to handle programs with unbounded loops. 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.