Certified Machine Learning

We now know, in both principle and practice, how to build conventional software systems (compilers, operating systems, program logics) that are mechanically verified against deep specifications. Yet many software systems are no longer conventional, in the sense that critical components — classifiers for recognizing street signs in an autonomous car, for example — are learned from data rather than programmed by humans. The MLCert project uses techniques familiar from traditional software verification, such as theorem proving, to build new architectures for certifying deep properties of the next generation of machine learning (ML) systems, from generalization to robustness to convergence.