5 ms·
Check out the "Deepmath" paper linked above. (The paper is from a few months ago, the source code is new IIUC.) https://arxiv.org/abs/1606.04442 https://arxiv.
by danblick 10y ago
Check out the "Deepmath" paper linked above. (The paper is from a few months ago, the source code is new IIUC.)
https://arxiv.org/abs/1606.04442 https://arxiv.org/abs/1606.04442
- jeff_marshall 10y agothanks! (edit) I still don't see any rationale for the theorem prover kernel re-implementation. Again, pointers appreciated.
- posterboy 10y agoMy bet is on concurrency optimizations
- dgacmu 10y agoHOL 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.) [1] https://www.quora.com/Which-programming-languages-does-Google-use-internally https://www.quora.com/Which-programming-languages-does-Googl...