> Note: building Certigrad currently takes ~15 minutes and consumes ~7 GB of memory.
Why does it take so long and use so much memory?
Why does it take so long and use so much memory?
Building Certigrad involves replaying all tactic scripts in the entire project to reconstruct all of the formal proofs, and then checking each of the formal proof objects in Lean's small trusted kernel. Proving (and checking) the main correctness theorem for stochastic backpropagation is very fast. The vast majority of the time and memory is spent verifying that a specific machine learning model (AEVB) satisfies all the preconditions for backprop. This involves proving several technical conditions, e.g. that various large terms are (uniformly) integrable. We have not experimented much with simplification strategies, and there is probably a lot of room for improvement in bringing these numbers down. It would also be good to provide an option to build the system without reconstructing the proofs; checking the proofs is analogous to running the entire test suite, and most users do not do this for every tool they build.
Now in Isabelle most strutures are encoded as type class, but when your type is not anymore in the type class suddenly you need to proof a lot of theorems yourself, and the automation does not work as nice as with type classes. Generally, in HOL provers you want at least that your type at least has nice algebraic properties on the entire type. If this is not the case proofs get much more convoluted. Isabelle's simplifier supports this case using conditional rewrite rules, but it still does not work as nice as using type inference to handle this cases.
In dependent type theorem provers it isn't a problem to proof everything on tensors with a fixed dimension. When a proof requires to do induction on the dimension itself these kind of shape can always constructed in the proof itsefl.
In Isabelle one might want to trust the code generator to evaluate certain computations in ML.
I worry slightly about Lean being immature, and lacking a big library eco-system in 2017. OTOH, it's also good to be at the cutting edge.