Tue 19 Jun 2018 16:20 - 16:25 at Columbus Ballroom B - Lightning Talks

We now know, both in principle and practice, how to build conventional software systems (compilers, operating systems, program logics) that are mechanically verified against deep functional specifications. In this lightning talk, I’ll highlight new directions in machine verification of machine learning (ML) systems, those that learn from data to perform tasks such as image classification. In particular, I’ll briefly describe (1) what it means for an ML algorithm to be correct (and why one should care), (2) how to go about representing and mechanically verifying such correctness specifications, and (3) some recent work at Ohio University on verified Perceptron learning, verified online learning (Multiplicative Weights), and a work-in-progress certificate architecture for validating neural network generalization.

Tue 19 Jun

Displayed time zone: Eastern Time (US & Canada) change