About The Forum
Calendar 2017 Poster Sessions : Developing Bug-Free Machine Learning Systems With Formal Mathematics
Abstract:
Noisy data, non-convex objectives, model misspecification, and numerical instability can all cause undesired behaviors in machine learning systems. As a result, detecting actual implementation errors can be extremely difficult. We demonstrate a methodology based on an interactive proof assistant, in which one writes an implementation of a machine learning system along with a formal theorem stating that the implementation is correct. The process of proving this theorem interactively in the proof assistant exposes all implementation errors since any error in the program would cause the proof to fail. As a case study, we implement a new system, Certigrad, for optimizing over stochastic computation graphs and generate a machine-checkable proof that the gradients sampled by the system are unbiased estimates of the true mathematical gradients. We train a variational autoencoder using Certigrad and find it nearly as efficient as TensorFlow.
Bio:
Daniel Selsam is a Ph.D. candidate in Computer Science at Stanford
University. His research aim is to develop tools based on formal logic
that assist with mentally demanding tasks such as programming,
algorithm design and mathematical problem-solving.
Noisy data, non-convex objectives, model misspecification, and numerical instability can all cause undesired behaviors in machine learning systems. As a result, detecting actual implementation errors can be extremely difficult. We demonstrate a methodology based on an interactive proof assistant, in which one writes an implementation of a machine learning system along with a formal theorem stating that the implementation is correct. The process of proving this theorem interactively in the proof assistant exposes all implementation errors since any error in the program would cause the proof to fail. As a case study, we implement a new system, Certigrad, for optimizing over stochastic computation graphs and generate a machine-checkable proof that the gradients sampled by the system are unbiased estimates of the true mathematical gradients. We train a variational autoencoder using Certigrad and find it nearly as efficient as TensorFlow.
Bio:
Daniel Selsam is a Ph.D. candidate in Computer Science at Stanford
University. His research aim is to develop tools based on formal logic
that assist with mentally demanding tasks such as programming,
algorithm design and mathematical problem-solving.