5 ms·

>Am I being too naive here? I don't think so, but I think the trick will be how to score a new mathematical relationship as "interesting". Basically, a fitness

>Am I being too naive here? I don't think so, but I think the trick will be how to score a new mathematical relationship as "interesting". Basically, a fitness metric. With Chess, you have the obvious win/loss metric, and also number of turns and possibly time. With math, how do you quantify the level of interestingness between 2+2=4 and p=np? This isn't a snarky question, by the way. I'm genuinely interested in how this might be done.

whatshisface 6y ago
It would be sufficiently amazing for AlphaProof to simply answer the questions posed to it. The training data would be pairs of theorems and proofs as already existing in the CoQ and other proof checker literature.
- groby_b 6y ago
  Unless you have a prover that can answer "is this actually a correct proof", your fitness function is essentially "does this look like a proof" And if you have a prover that can answer that question, you don't need to train a neural network to give you the answer. Proving maths demands 100% precision and recall, at which point employing ML doesn't make sense - the point of ML is (horribly simplified) stochastic reasoning, not finding truths.
  - PartiallyTyped 6y ago
    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.
  - whatshisface 6y ago
    Proof checkers are an existing technology. That's what CoQ is.
    - groby_b 6y ago
      Yes. My formulation was sloppy - I didn't mean "unless" to imply that there can't be a prover. My argument was that without a full prover, you won't have a useful fitness function at all. And even then recall/precision need to be 100%. And even if you could achieve that, you still end up with something that... generates statements that are provably true. Mild yay. But that's not the problem. We can generate plenty of those. You want to identify the ones that actually advance the state of knowledge usefully.
lacker 6y ago
Indeed, existing automated theorem provers do spend a lot of time discarding true statements as "insufficiently interesting". In general, the longer a statement the less interesting it is. The easier it is to prove with simpler statements, the less interesting it is. And if it's superceded by a more general rule it is less interesting. For example, an automated theorem prover can easily prove many statements of the form "A or not-A or (any long statement)". Those are all uninteresting tautologies that should be discarded. It's interesting to theorize about improving these heuristics with AI methods, there is some work along these lines like ENIGMA-NG.

whatshisface 6y ago

It would be sufficiently amazing for AlphaProof to simply answer the questions posed to it. The training data would be pairs of theorems and proofs as already existing in the CoQ and other proof checker literature.

groby_b 6y ago
Unless you have a prover that can answer "is this actually a correct proof", your fitness function is essentially "does this look like a proof" And if you have a prover that can answer that question, you don't need to train a neural network to give you the answer. Proving maths demands 100% precision and recall, at which point employing ML doesn't make sense - the point of ML is (horribly simplified) stochastic reasoning, not finding truths.
- PartiallyTyped 6y ago
  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.
- whatshisface 6y ago
  Proof checkers are an existing technology. That's what CoQ is.
  - groby_b 6y ago
    Yes. My formulation was sloppy - I didn't mean "unless" to imply that there can't be a prover. My argument was that without a full prover, you won't have a useful fitness function at all. And even then recall/precision need to be 100%. And even if you could achieve that, you still end up with something that... generates statements that are provably true. Mild yay. But that's not the problem. We can generate plenty of those. You want to identify the ones that actually advance the state of knowledge usefully.

lacker 6y ago

Indeed, existing automated theorem provers do spend a lot of time discarding true statements as "insufficiently interesting". In general, the longer a statement the less interesting it is. The easier it is to prove with simpler statements, the less interesting it is. And if it's superceded by a more general rule it is less interesting. For example, an automated theorem prover can easily prove many statements of the form "A or not-A or (any long statement)". Those are all uninteresting tautologies that should be discarded. It's interesting to theorize about improving these heuristics with AI methods, there is some work along these lines like ENIGMA-NG.