4 ms·

But ML could in theory accelerate the process. For example, AlphaZero uses ML to highlight the correct paths in search algorithms. The same search algorithms ex

But ML could in theory accelerate the process. For example, AlphaZero uses ML to highlight the correct paths in search algorithms. The same search algorithms exist for stockfish and both can reach the same conclusions, but, AlphaZero ends up looking up much shorter distance than stockfish, yet it wins. If anything, it is significantly more human-like than stockfish.

gjulianm 6y ago
The search space for proofs is far bigger and less structured than a Go game. A lot of proofs also require creativity, in the sense that they aren't just "find the set of logical steps from 'initial condition' to 'proof'", but they require auxiliary theorems, definitions and constructions that help make the problem manageable. Another problem is that a lot of proofs starts by exploration. For example, certain bounds for functions or convergence rates are proved without knowing what will be the end result. Of all the problems that ML could be applied to, I find mathematical proofs one of the least promising. One, I don't see enough similarity between proofs that would allow any algorithm to learn useful patterns; and two, I don't think most mathematicians would trust a proof that cannot be understood (even if the output is a set of steps for a formal system, I imagine translating that to human language could be quite difficult).
- touisteur 6y ago
  I wish we'd start with general loop variant/invariant generation...
- PartiallyTyped 6y ago
  I would like to bring up Gödel and his idea that you could construct theorems by multiplying equivalent numbers that represent theorems but I am sure you are well aware of it. My argument is that it all happens through the application of operators and abstractions i.e. other numbers going through Gödel's approach. In the same vein, we "should" in theory produce something similar. In RL, we have agents that learn to 'imagine' goals and then achieve them. Given the correct representation of such 'dreams' the models 'could' in theory learn to achieve such auxiliary theorems.

gjulianm 6y ago

The search space for proofs is far bigger and less structured than a Go game. A lot of proofs also require creativity, in the sense that they aren't just "find the set of logical steps from 'initial condition' to 'proof'", but they require auxiliary theorems, definitions and constructions that help make the problem manageable. Another problem is that a lot of proofs starts by exploration. For example, certain bounds for functions or convergence rates are proved without knowing what will be the end result. Of all the problems that ML could be applied to, I find mathematical proofs one of the least promising. One, I don't see enough similarity between proofs that would allow any algorithm to learn useful patterns; and two, I don't think most mathematicians would trust a proof that cannot be understood (even if the output is a set of steps for a formal system, I imagine translating that to human language could be quite difficult).

touisteur 6y ago
I wish we'd start with general loop variant/invariant generation...
PartiallyTyped 6y ago
I would like to bring up Gödel and his idea that you could construct theorems by multiplying equivalent numbers that represent theorems but I am sure you are well aware of it. My argument is that it all happens through the application of operators and abstractions i.e. other numbers going through Gödel's approach. In the same vein, we "should" in theory produce something similar. In RL, we have agents that learn to 'imagine' goals and then achieve them. Given the correct representation of such 'dreams' the models 'could' in theory learn to achieve such auxiliary theorems.