5 ms·
Tensorflow Deepmath: Experiments towards neural network theorem proving
- runesoerensen 10y agoRelevant HN discussion about the paper: https://news.ycombinator.com/item?id=12031253 https://news.ycombinator.com/item?id=12031253
- bitL 10y agoWhat logic does it use? Any chance using relevance or linear logic to avoid vacuous truth proofs (like in set theory)?
- cmrx64 10y agoIt's currently integrating higher-order logic (HOL) with a reimplementation of HOL Light.
- jeff_marshall 10y agoI 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.?
- danblick 10y agoCheck 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...
- cmrx64 10y agoNeat! I look forward to seeing what they come up with :) For similar sorts of things, check out NeSy: http://daselab.cs.wright.edu/nesy/NeSy16/ http://daselab.cs.wright.edu/nesy/NeSy16/
- Mao_Zedang 10y agoHook it up to a network that makes theorems.
- SticksAndBreaks 10y agoEvery 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.
- thomasahle 10y ago> Every problem i can break into a sub problem is solveable. Given the sub problems are either solvable or can in turn be broken down, I suppose?