Project

Formal Semantics and Verified Parsing for an Inference Language

Principal Investigator

Boston College

Summary

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.