I wonder what the reason for the re-implementation is. Perhaps the existing kernel isn't fast enough at evaluation for training (wild guess)? I'll have to RTFM...
(update)
their doesn't appear to be any FM. Can anyone post any links to papers/lists/etc.?
HOL is written in OCaml. The likely answer is because integrating OCaml and TensorFlow would be painful -- and OCaml isn't one of the languages Google supports internally [1]. Probably was easier to reimplement than to try to do all the contortions needed to use it in this context.
(I work part time on the Brain team, but I haven't asked the authors about this -- this is a best guess based upon knowing TF, not an informed statement.)
Every problem i can break into a sub problem is solveable.
Thus proofen by induction that i can break recursively down every problem, i deduce- that i crashed with a NN-Stackoverflow.
12 comments
[ 3.2 ms ] story [ 35.8 ms ] thread(update) their doesn't appear to be any FM. Can anyone post any links to papers/lists/etc.?
https://arxiv.org/abs/1606.04442
(edit) I still don't see any rationale for the theorem prover kernel re-implementation. Again, pointers appreciated.
(I work part time on the Brain team, but I haven't asked the authors about this -- this is a best guess based upon knowing TF, not an informed statement.)
[1] https://www.quora.com/Which-programming-languages-does-Googl...
Given the sub problems are either solvable or can in turn be broken down, I suppose?