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 JunDisplayed time zone: Eastern Time (US & Canada) change
16:10 - 17:35 | |||
16:10 5mTalk | 5-minute Lightning Talks DeepSpec | ||
16:15 5mTalk | Simplicity for Smart Contracts DeepSpec | ||
16:20 5mTalk | Machine-Verified Machine Learning DeepSpec Gordon Stewart Ohio University | ||
16:25 5mTalk | Verification of Union-Find in C DeepSpec | ||
16:30 5mTalk | Narcissus: Deriving Correct-By-Construction Decoders and Encoders from Binary Formats DeepSpec Clément Pit-Claudel MIT CSAIL | ||
16:35 5mTalk | LLVM's IR and Call-By-Push-Value Lambda Calculus DeepSpec | ||
16:40 5mTalk | A Formal Equational Theory for Call-By-Push-Value DeepSpec Christine Rizkallah The University of Melbourne | ||
16:45 5mTalk | Serializability for Distributed Protocols DeepSpec Joonwon Choi Massachusetts Institute of Technology, USA | ||
16:50 5mTalk | A Quick Hack to ask any SMT Solver if my Coq Goal is True DeepSpec Samuel Gruetter Massachusetts Institute of Technology | ||