Tensorflow Deepmath: Experiments towards neural network theorem proving

https://github.com/tensorflow/deepmath

by runesoerensen • 10 years ago

142 12 10 years ago

github.com

runesoerensen• 10 years ago

Relevant HN discussion about the paper: https://news.ycombinator.com/item?id=12031253

bitL• 10 years ago

What logic does it use? Any chance using relevance or linear logic to avoid vacuous truth proofs (like in set theory)?

cmrx642• 10 years ago

It's currently integrating higher-order logic (HOL) with a reimplementation of HOL Light.

jeff_marshall2• 10 years ago

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.?

cmrx642• 10 years ago

Neat! 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/

Mao_Zedang• 10 years ago

Hook it up to a network that makes theorems.

SticksAndBreaks• 10 years ago

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.

thomasahle• 10 years 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?

Tensorflow Deepmath: Experiments towards neural network theorem proving

Related Stories