Developing Bug-Free Machine Learning Systems With Formal Mathematics http://arxiv.org/abs/1706.08605 機械学習システムの検証への対話的定理証明器の応用。

Leanを使い、微積分などを公理化した上で、ケーススタディとして Stochastic Computation Graph (SCG) のバックプロパゲーションの実装が真の勾配の不偏推定になっていることを証明。 得られた実装のテンソル計算をEigenに差し替えたものは、Auto-Encoding Variational Bayes (AEVB) モデルをMNISTでADAMで学習した場合で、Tensorflowと同程度の性能と精度だったのを確認。

コードを見ると、Leanで9千3百行くらい。

arxiv: http://arxiv.org/abs/1706.08605
ICML2017のページ: https://2017.icml.cc/Conferences/2017/Schedule?showEvent=849
実装: https://github.com/dselsam/certigrad