Comment by TuringTest
4 years ago
Math follows a completely different approach with respect to how machine-learning AIs do their thing.
Reason derives its strength in having a few primitives and creating new assertions through the transformation of symbols by following precise rules (which is how algorithms work).
In ML-based AIs, everything is imprecise and probabilistic, and this kind of generation gets its strength from building recognizable from utterly imprecise inputs and training - quite the opposite of how logic and reason evolve. Now, "classic" AI was a powerful way to derive new knowledge, and automatic theorem proving is a strong discipline; but the recent breakthroughs in AI are not directly applicable to classic techniques.
Do you know what machine-learning AIs could be good for? Generating "insight" in problem solvers for guiding the theorem demonstrations through the proof search space, trying to find the best sub-spaces to explore. If there's a way to create human-like general AI, it will likely combine both kinds of generation - the rational methods of symbolic logic and the "irrational" statistical methods of ML.
Automated theorem proving is the same problem as “complete and label the diagram”, which image generation is okay at.
Work in progress for sure, though.
> Automated theorem proving is the same problem as “complete and label the diagram”, which image generation is okay at.
How so?
I'm no mathematician, but I don't see how these problem types are equivalent. Could you elaborate?
Sure — the connecting topic is topos theory.
For a type theory we might want to reason about, there’s a diagram (in category theory) which represents the same semantic content. These diagrams turn out to have recurring and common structures.
You can represent those diagrams as adjacency matrices, where those structures have a particular “shape” in the entries. Which if you squint hard looks like an image completion problem, ie, finding missing part of the matrix which represents a proof.
2 replies →