Developing Bug-Free Machine Learning Systems With Formal Mathematics
D. Selsam, P. Liang, and D. Dill. (2017)cite arxiv:1706.08605Comment: To appear at the Thirty-fourth International Conference on Machine Learning (ICML) 2017.
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 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.
Description
[1706.08605] Developing Bug-Free Machine Learning Systems With Formal Mathematics
%0 Journal Article
%1 selsam2017developing
%A Selsam, Daniel
%A Liang, Percy
%A Dill, David L.
%D 2017
%K debugging learning
%T Developing Bug-Free Machine Learning Systems With Formal Mathematics
%U http://arxiv.org/abs/1706.08605
%X 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.
@article{selsam2017developing,
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 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.},
added-at = {2019-02-28T21:06:58.000+0100},
author = {Selsam, Daniel and Liang, Percy and Dill, David L.},
biburl = {https://www.bibsonomy.org/bibtex/2ad874de962254002611961cf4197e855/kirk86},
description = {[1706.08605] Developing Bug-Free Machine Learning Systems With Formal Mathematics},
interhash = {385c221baddb54a1333c39a442ddad69},
intrahash = {ad874de962254002611961cf4197e855},
keywords = {debugging learning},
note = {cite arxiv:1706.08605Comment: To appear at the Thirty-fourth International Conference on Machine Learning (ICML) 2017},
timestamp = {2019-02-28T21:06:58.000+0100},
title = {Developing Bug-Free Machine Learning Systems With Formal Mathematics},
url = {http://arxiv.org/abs/1706.08605},
year = 2017
}