Developing Bug-Free Machine Learning Systems Using Formal Mathematics

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 in which developers use an interactive proof assistant to both implement their system and to state a formal theorem defining what it means for their system to be 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 we generate a formal (i.e. 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 the performance comparable to training the same model in TensorFlow. 

[officebatman]

Very interesting work! Sometimes it’s hard to see the applications of theorem proving in production code but this talk showed a great example! And the speaker was great at speaking

[derschutz]

Jeez, does that dude in the audience lack critical thinking? He just assumes Daniel is saying formally proving these systems is going to fix all problems. All of his questions are not steel manning but just going to random tangents that are easy to dismiss after maybe 5 seconds of thought and he just goes on and on. Maybe ask a question that weighs the pros and cons of formal verification like, "What is the tradeoff we are making in terms of speed of development and minimization of bugs?" or something that is slightly interesting. Instead of being curious, dude was just instantly objecting and not even objecting with interesting challenging questions. Just as simple as asking yourself would you rather have systems that are formally proven or not (ofc everyone wants formally proven systems) and if so, what is too much of a cost where that would change, instead of probing a conversation like that he just says "well I don't think it would matter that much".

[ster]

Tough crowd. They seemed very skeptical couldn't get Daniel to blink

[mohammadnrg]

Oh look at Sheldon, but wtf happend you're working for microsoft now?