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.


Gordon Stewart
Gordon Stewart
Ohio University
Sam Merten
Sam Merten
Ohio University
Alex Bagnall
Alex Bagnall
Ohio University
Charlie Murphy
Charlie Murphy (alum)
Princeton University

Related Research Papers

AAAI 2019
Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees. Alexander Bagnall, Gordon Stewart. AAAI'19: The Thirty-Third AAAI Conference on Artificial Intelligence. [CODE]

Capsule summary: Machine learning in Coq with verified generalization guarantees, applied via TensorFlow to the extended MNIST Digits dataset

ESOP 2018
Verified Learning Without Regret: From Algorithmic Game Theory to Distributed Systems With Mechanized Complexity Guarantees. Samuel Merten, Alexander Bagnall, and Gordon Stewart. ESOP'18: The 27th European Symposium on Programming. [CODE]

Capsule summary: Verified Multiplicative Weights Update in Coq, with applications to online learning and distributed routing games

JFR 2017
A Library for Algorithmic Game Theory in Ssreflect/Coq. Alexander Bagnall, Samuel Merten, and Gordon Stewart. Journal of Formalized Reasoning. December 2017. [CODE]

Capsule summary: Coq library of basic results in algorithmic game theory

PODC 2017
Brief Announcement: Certified Multiplicative Weights Update. Alexander Bagnall, Samuel Merten, and Gordon Stewart. PODC'17: The 36th ACM Symposium on Principles of Distributed Computing.

Capsule summary: Extended abstract introducing at a high level the ideas substantially fleshed out in our ESOP 2018 paper

MAPL 2017
Verified Perceptron Convergence Theorem. Charlie Murphy, Patrick Gray, and Gordon Stewart. MAPL'17: The First ACM SIGPLAN Workshop on Machine Learning and Programming Languages. [CODE]

Capsule summary: Coq implementation of Perceptron learning with proved convergence on linearly separable training sets

Work described on this page is supported in part by the NSF under grant CCF-1657358 and by the Ohio Federal Research Network (OFRN). The documents contained in these pages are included to ensure timely dissemination of scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.