Formal Semantics and Veriﬁed Parsing for an Inference Language
Oracle Principal Investigator
Michael Wick, Principal Member Technical Staff
Stephen Green, Senior Director
One of the fundamental problems one faces when trying to build an ML model of complex processes is that it can be substantially easier to design a model than it can be to understand how to train that model using existing data. Deriving inference algorithms from probabilistic models requires a deep expertise in mathematics and statistics, and implementations tend to be very error prone
We propose are exploring the possibility of building formally verified tools for probabilistic machine learning by defining formally a language for Bayesian networks, building a verified parser for it, defining its semantics formally, all within the framework of the Compcert formally verified compiler.