6 ms·

Distantly related question. It was claimed that Alpha Zero taught itself to play incredibly high level chess from the very basic point of playing with itself mi

Distantly related question. It was claimed that Alpha Zero taught itself to play incredibly high level chess from the very basic point of playing with itself millions of times after having been fed the basic building block rules of chess and nothing else. Now I'm wondering if something like this can be made to work for discovering new mathematical relationships or solving existing hypothesis by training a neural network with what we know of maths so far and then letting it "play" with the equations? Am I being too naive here?

whatshisface 6y ago
There is a sense in which that is a great idea, and a sense in which it is a not so great idea. If AlphaProof could prove theorems as superhumanly as AlphaGo wins at Go, that would really be something, they might be able to claim all of the millennium prizes. However, the longterm usefulness to mathematics may be somewhat limited. Mathematicians are interested in proofs not so much because of the statements, but because of what those proofs add to our knowledge of the way math fits together. It isn't just about "true" or "false," it's about why. If AlphaProof generated a long and unreadable proof with no discernible structure, it would not be such a large contribution to mathematics as if a human figured out "why" and wrote it in a way other humans could understand. Of course, it is possible that clever users could tease useful information out of the black box truth oracle. Perhaps by modifying the statement of the conjecture and checking each modification, they could discover some parts of the structure of the problem, which would help inspire a useful proof. Furthermore, it would be helpful to never again waste time trying to prove a false conjecture.
- virgil_disgr4ce 6y ago
  True, and important. However, I suppose it could be argued that if the only results AlphaProof could obtain were long and unreadable proof(s) with no discernible structure, it might suggest something about the epistemic assumptions we tend to make about Occam's Razor and the (so-called) beauty and parsimony. On that angle, it could be further argued that humans are biased towards 'readable' proofs and that there are many undiscovered 'unreadable' proofs that we simply have no way of obtaining without automation of some kind. Anyway I assume there are volumes already written on this subject...
  - whatshisface 6y ago
    >the epistemic assumptions we tend to make about Occam's Razor and the (so-called) beauty and parsimony. The vast majority of ways to write a program are unreadable messes. The shortest way to write a program is sometimes an unreadable mess, mainly when it's been code golfed. The longest ways to write a program are always unreadable. Proofs work the same way - and if Alpha Go selects randomly from all of the ways to write a reasonable-length proof, it is virtually guaranteed to pick an unreadable one.
  - postalrat 6y ago
    A long unreadable proof would not mean a small proof doesn't exist. I feel like a unreadable proof would be useful to simply know something is true while a small proof would be more useful to perhaps gain some sort of insight.
  - touisteur 6y ago
    Maybe that'll be time to bring in AlphaProofReductor or AlphaProofCanonizer. I'm finding this worry a bit strange. I'm guessing tools evolve together depending on need, so as long as humans want to know 'why and how' there'll be some effort in reduction?
  - ncmncm 6y ago
    There probably are not. A successful AlphaProof would be trained to favor shorter proofs. It would be fast enough to prove RH myriad different ways, and not be finished until its proof cannot be shortened any more, just as AlphaGo isn't finished until no version of it can beat it. Whether humans could understand the shortest possible proof is another question. It might take generations of study just to understand its outline, and many more to extract all the lemmas implied. Or, it might turn out to be a trivial trick, and not reveal anything new and substantial.
- idolaspecus 6y ago
  Your comment inspired an interesting (to me at least) thought. I'm imagining a world where mathematics becomes too advanced for even the brightest human being, but progress is preserved by proof-generating programs running in data centers. The data centers churn out exabytes of mathematical proofs, and humanity employs an army of what are effectively philologists/semioticians to dissect, mine, and excavate these proofs for meaning.
  - dwohnitmok 6y ago
    Ted Chiang has a (very) short story exploring this idea, with metahumans replacing data centers here: https://www.nature.com/articles/35014679 https://www.nature.com/articles/35014679
    - agar 6y ago
      Thank you for that link. A very interesting story, with surprising philosophical depth given its brevity.
  - brzozowski 6y ago
    And when your surpassing creations find the answers you asked for, you can’t understand their analysis and you can’t verify their answers. You have to take their word on faith—Or you use information theory to flatten it for you, to squash the tesseract into two dimensions and the Klein bottle into three, to simplify reality and pray to whatever Gods survived the millennium that your honorable twisting of the truth hasn’t ruptured any of its load-bearing pylons. You hire people like me; the crossbred progeny of profilers and proof assistants and information theorists… In formal settings you’d call me Synthesist. —Peter Watts, Blindsight (2006) [1]: https://www.rifters.com/real/Blindsight.htm https://www.rifters.com/real/Blindsight.htm
- karmakaze 6y ago
  We already have machine-assisted proofs which are structured by people but executed by machines. AlphaProof would be that but structured by machine. As with the machine-assisted proofs, there's value in knowing and building upon the result even if the methods themselves can't be adapted for other use.
- lacker 6y ago
  If AlphaProof generated a long and unreadable proof with no discernible structure, it would not be such a large contribution to mathematics as if a human figured out "why" and wrote it in a way other humans could understand. Maybe not directly. But if AlphaProof managed to prove the Riemann hypothesis, I bet it wouldn't be long before human mathematicians had managed to decipher the proof and explain it in a way that other mathematicians found useful. It's just a lot easier to re-explain something that other people have already proved, rather than proving it yourself.
  - Jabbles 6y ago
    Gödel's incompleteness theorem doesn't fill me with the same confidence as you that "a true theorem should have a useful explanation". In fact, looking at chess engines tells us that sometimes (though not always) brute-force calculation of many possibilities gives us better moves. In the same way some true statements might just be an exhaustive calculation. Perhaps the four color theorem is the most famous example of a proof that has lacked (still lacks) a lot of useful lemmas in relation to its length: https://en.wikipedia.org/wiki/Four_color_theorem https://en.wikipedia.org/wiki/Four_color_theorem
    - lacker 6y ago
      Yeah, it certainly isn't true that a true theorem should have a useful explanation. I only have my human intuition to go on, but I bet the Riemann hypothesis would not be like the four-color problem. Graph-type problems just seem to lend themselves to exhaustively checking a zillion cases in a boring way, whereas in fields like number theory or analysis that sort of proof hardly ever seems to exist. I hope we do get some famous theorems proved by computers so that we can see whether it's enlightening to humans. I am quite curious whether my intuition is correct and it is a shame to think I might never know....
- 8bitsrule 6y ago
  > If AlphaProof generated a long and unreadable proof... Then how would anyone be sure it isn't wrong? It was great that while Goldston and Yıldırım were wrong, their work proved to be useful. A lot of people are glad that Riemann (and Fermat) didn't their problems!
  - whatshisface 6y ago
    We have automated proof checkers like CoQ. A proof machine would be designed to output proofs in a syntax that could be mechanically checked by an existing verifier.
Bjartr 6y ago
The trick is coming up with a reward function that drives exploration when "played" against itself. Chess has an easy one, win the game. General mathematics doesn't have anything so easily specified.
- whatshisface 6y ago
  It does, math has "prove the conjecture."
  - rfurmani 6y ago
    We can't even solve Sonic the Hedgehog without getting stuck in dead-ends in the game :-) https://openai.com/blog/retro-contest/ https://openai.com/blog/retro-contest/
  - 317070 6y ago
    Well, math is two parts. There is the "prove this conjecture I have" part, which I think will be taken over by machines rather soon (say, within my lifetime). I cannot imagine there is something extra-ordinarily hard that mathematicians do, that is somehow not captured by how a Go player approaches the game. There is also the "come up with an interesting conjecture" part, which I think is a lot harder. It is extra-ordinarily hard to specify what exactly makes some conjectures more interesting than others. So I reckon this part of math will be much harder to automate in the long run. It will probably require a lot of cross-contamination from AI that manage to write interesting books for example.
    - gjulianm 6y ago
      > I cannot imagine there is something extra-ordinarily hard that mathematicians do, that is somehow not captured by how a Go player approaches the game. It's not "extraordinarily hard" but the issue is that math does not have a well-defined search space. A lot of times, proving statements requires quite a lot of intermediate results, additional tools and definitions... There is more creativity in math proofs that people think, and I don't think ML algorithms will be able to reproduce that. At most I see specific algorithms for limited purposes.
TheCraiggers 6y ago
>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).
rfurmani 6y ago
Adding an extra point, one thing that makes this difficult is that a lot of this kind of research is not about applying existing ideas but coming up with something that has never been done before, and neutral networks are a lot worse with creativity than with pattern matching. It's also hard to get enough training examples, especially since you'd either want these to be in strict logical language or train a system to recognize whether a hundred page proof in natural language is rigorous or not. So it's like a very long maze where noody knows if you're getting closer to the exit or not, and in most rooms you have to come up with something original or discover a new dimension. And there's the aspect whereby a lot of significant research is: create a new abstraction, realize and convince others that this abstraction is useful and gives you new intuition that lets you solve new problems.
mensetmanusman 6y ago
From a finite set of axioms you can generate an infinite number of proofs because complexity is unbounded. ‘Proofs’ in human parlance are those which we believe to be interesting or aesthetic or useful.
ellis-bell 6y ago
you might be able to do something like "predict the next prime number" or "predict the next zero of the Riemann zeta function". you could try something like this for statements in a formal axiomatic system, but know that you're running up against things like the halting problem / entscheidungsproblem / godel incompleteness. so it may be possible to train a neural net to decide the veracity of a statement and do so more quickly than a human might, but you would inevitably be running up against things that are truly undecidable in nature. which is not like go or chess where although they are difficult, they are decidable.
- sanxiyn 6y ago
  I am not sure how math is unlike chess. Chess has three outcomes: win, loss, draw. That seems exactly like math, having true, false, undecidable.
  - gjulianm 6y ago
    Yes, but it isn't useful. A conversation also has three outcomes (neutral, you like the person more, or less) and yet it doesn't make conversations similar to chess.
    - whatshisface 6y ago
      Chess and math are both searches over countably infinite trees.
      - gjulianm 6y ago
        And a conversation is a search over a countably infinite tree too. My point is that even though some things have technical similarities, in practice they are very different challenges.
        whatshisface 6y ago
        Math and chess are both very easy to check. Proof checkers and chess rule checkers both exist. "Conversation checkers" do not.
ajnin 6y ago
Your comment reminds me of Gödel's proof of his incompleteness theorem. Basically, he said that if you treat a mathematical statement as a sequence of tokens, and then assign a number to each token, then you can transform the statement into a big number. Then, going one step further, if a mathematical proof is a sequence of statements then it can be too transformed into a really long number. Then you can come up with rules to manipulate these numbers to create new valid statements and proofs. I don't know if there was much work done on this idea beyond Gödel's proof, but I think it's a really neat idea that gives a way to manipulate mathematical proofs as objects and create new ones from a very high level view.

whatshisface 6y ago

There is a sense in which that is a great idea, and a sense in which it is a not so great idea. If AlphaProof could prove theorems as superhumanly as AlphaGo wins at Go, that would really be something, they might be able to claim all of the millennium prizes. However, the longterm usefulness to mathematics may be somewhat limited. Mathematicians are interested in proofs not so much because of the statements, but because of what those proofs add to our knowledge of the way math fits together. It isn't just about "true" or "false," it's about why. If AlphaProof generated a long and unreadable proof with no discernible structure, it would not be such a large contribution to mathematics as if a human figured out "why" and wrote it in a way other humans could understand. Of course, it is possible that clever users could tease useful information out of the black box truth oracle. Perhaps by modifying the statement of the conjecture and checking each modification, they could discover some parts of the structure of the problem, which would help inspire a useful proof. Furthermore, it would be helpful to never again waste time trying to prove a false conjecture.

virgil_disgr4ce 6y ago
True, and important. However, I suppose it could be argued that if the only results AlphaProof could obtain were long and unreadable proof(s) with no discernible structure, it might suggest something about the epistemic assumptions we tend to make about Occam's Razor and the (so-called) beauty and parsimony. On that angle, it could be further argued that humans are biased towards 'readable' proofs and that there are many undiscovered 'unreadable' proofs that we simply have no way of obtaining without automation of some kind. Anyway I assume there are volumes already written on this subject...
- whatshisface 6y ago
  >the epistemic assumptions we tend to make about Occam's Razor and the (so-called) beauty and parsimony. The vast majority of ways to write a program are unreadable messes. The shortest way to write a program is sometimes an unreadable mess, mainly when it's been code golfed. The longest ways to write a program are always unreadable. Proofs work the same way - and if Alpha Go selects randomly from all of the ways to write a reasonable-length proof, it is virtually guaranteed to pick an unreadable one.
- postalrat 6y ago
  A long unreadable proof would not mean a small proof doesn't exist. I feel like a unreadable proof would be useful to simply know something is true while a small proof would be more useful to perhaps gain some sort of insight.
- touisteur 6y ago
  Maybe that'll be time to bring in AlphaProofReductor or AlphaProofCanonizer. I'm finding this worry a bit strange. I'm guessing tools evolve together depending on need, so as long as humans want to know 'why and how' there'll be some effort in reduction?
- ncmncm 6y ago
  There probably are not. A successful AlphaProof would be trained to favor shorter proofs. It would be fast enough to prove RH myriad different ways, and not be finished until its proof cannot be shortened any more, just as AlphaGo isn't finished until no version of it can beat it. Whether humans could understand the shortest possible proof is another question. It might take generations of study just to understand its outline, and many more to extract all the lemmas implied. Or, it might turn out to be a trivial trick, and not reveal anything new and substantial.
idolaspecus 6y ago
Your comment inspired an interesting (to me at least) thought. I'm imagining a world where mathematics becomes too advanced for even the brightest human being, but progress is preserved by proof-generating programs running in data centers. The data centers churn out exabytes of mathematical proofs, and humanity employs an army of what are effectively philologists/semioticians to dissect, mine, and excavate these proofs for meaning.
- dwohnitmok 6y ago
  Ted Chiang has a (very) short story exploring this idea, with metahumans replacing data centers here: https://www.nature.com/articles/35014679 https://www.nature.com/articles/35014679
  - agar 6y ago
    Thank you for that link. A very interesting story, with surprising philosophical depth given its brevity.
- brzozowski 6y ago
  And when your surpassing creations find the answers you asked for, you can’t understand their analysis and you can’t verify their answers. You have to take their word on faith—Or you use information theory to flatten it for you, to squash the tesseract into two dimensions and the Klein bottle into three, to simplify reality and pray to whatever Gods survived the millennium that your honorable twisting of the truth hasn’t ruptured any of its load-bearing pylons. You hire people like me; the crossbred progeny of profilers and proof assistants and information theorists… In formal settings you’d call me Synthesist. —Peter Watts, Blindsight (2006) [1]: https://www.rifters.com/real/Blindsight.htm https://www.rifters.com/real/Blindsight.htm
karmakaze 6y ago
We already have machine-assisted proofs which are structured by people but executed by machines. AlphaProof would be that but structured by machine. As with the machine-assisted proofs, there's value in knowing and building upon the result even if the methods themselves can't be adapted for other use.
lacker 6y ago
If AlphaProof generated a long and unreadable proof with no discernible structure, it would not be such a large contribution to mathematics as if a human figured out "why" and wrote it in a way other humans could understand. Maybe not directly. But if AlphaProof managed to prove the Riemann hypothesis, I bet it wouldn't be long before human mathematicians had managed to decipher the proof and explain it in a way that other mathematicians found useful. It's just a lot easier to re-explain something that other people have already proved, rather than proving it yourself.
- Jabbles 6y ago
  Gödel's incompleteness theorem doesn't fill me with the same confidence as you that "a true theorem should have a useful explanation". In fact, looking at chess engines tells us that sometimes (though not always) brute-force calculation of many possibilities gives us better moves. In the same way some true statements might just be an exhaustive calculation. Perhaps the four color theorem is the most famous example of a proof that has lacked (still lacks) a lot of useful lemmas in relation to its length: https://en.wikipedia.org/wiki/Four_color_theorem https://en.wikipedia.org/wiki/Four_color_theorem
  - lacker 6y ago
    Yeah, it certainly isn't true that a true theorem should have a useful explanation. I only have my human intuition to go on, but I bet the Riemann hypothesis would not be like the four-color problem. Graph-type problems just seem to lend themselves to exhaustively checking a zillion cases in a boring way, whereas in fields like number theory or analysis that sort of proof hardly ever seems to exist. I hope we do get some famous theorems proved by computers so that we can see whether it's enlightening to humans. I am quite curious whether my intuition is correct and it is a shame to think I might never know....
8bitsrule 6y ago
> If AlphaProof generated a long and unreadable proof... Then how would anyone be sure it isn't wrong? It was great that while Goldston and Yıldırım were wrong, their work proved to be useful. A lot of people are glad that Riemann (and Fermat) didn't their problems!
- whatshisface 6y ago
  We have automated proof checkers like CoQ. A proof machine would be designed to output proofs in a syntax that could be mechanically checked by an existing verifier.

Bjartr 6y ago

The trick is coming up with a reward function that drives exploration when "played" against itself. Chess has an easy one, win the game. General mathematics doesn't have anything so easily specified.

whatshisface 6y ago
It does, math has "prove the conjecture."
- rfurmani 6y ago
  We can't even solve Sonic the Hedgehog without getting stuck in dead-ends in the game :-) https://openai.com/blog/retro-contest/ https://openai.com/blog/retro-contest/
- 317070 6y ago
  Well, math is two parts. There is the "prove this conjecture I have" part, which I think will be taken over by machines rather soon (say, within my lifetime). I cannot imagine there is something extra-ordinarily hard that mathematicians do, that is somehow not captured by how a Go player approaches the game. There is also the "come up with an interesting conjecture" part, which I think is a lot harder. It is extra-ordinarily hard to specify what exactly makes some conjectures more interesting than others. So I reckon this part of math will be much harder to automate in the long run. It will probably require a lot of cross-contamination from AI that manage to write interesting books for example.
  - gjulianm 6y ago
    > I cannot imagine there is something extra-ordinarily hard that mathematicians do, that is somehow not captured by how a Go player approaches the game. It's not "extraordinarily hard" but the issue is that math does not have a well-defined search space. A lot of times, proving statements requires quite a lot of intermediate results, additional tools and definitions... There is more creativity in math proofs that people think, and I don't think ML algorithms will be able to reproduce that. At most I see specific algorithms for limited purposes.

TheCraiggers 6y ago

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

rfurmani 6y ago

Adding an extra point, one thing that makes this difficult is that a lot of this kind of research is not about applying existing ideas but coming up with something that has never been done before, and neutral networks are a lot worse with creativity than with pattern matching. It's also hard to get enough training examples, especially since you'd either want these to be in strict logical language or train a system to recognize whether a hundred page proof in natural language is rigorous or not. So it's like a very long maze where noody knows if you're getting closer to the exit or not, and in most rooms you have to come up with something original or discover a new dimension. And there's the aspect whereby a lot of significant research is: create a new abstraction, realize and convince others that this abstraction is useful and gives you new intuition that lets you solve new problems.

mensetmanusman 6y ago

From a finite set of axioms you can generate an infinite number of proofs because complexity is unbounded. ‘Proofs’ in human parlance are those which we believe to be interesting or aesthetic or useful.

ellis-bell 6y ago

you might be able to do something like "predict the next prime number" or "predict the next zero of the Riemann zeta function". you could try something like this for statements in a formal axiomatic system, but know that you're running up against things like the halting problem / entscheidungsproblem / godel incompleteness. so it may be possible to train a neural net to decide the veracity of a statement and do so more quickly than a human might, but you would inevitably be running up against things that are truly undecidable in nature. which is not like go or chess where although they are difficult, they are decidable.

sanxiyn 6y ago
I am not sure how math is unlike chess. Chess has three outcomes: win, loss, draw. That seems exactly like math, having true, false, undecidable.
- gjulianm 6y ago
  Yes, but it isn't useful. A conversation also has three outcomes (neutral, you like the person more, or less) and yet it doesn't make conversations similar to chess.
  - whatshisface 6y ago
    Chess and math are both searches over countably infinite trees.
    - gjulianm 6y ago
      And a conversation is a search over a countably infinite tree too. My point is that even though some things have technical similarities, in practice they are very different challenges.
      - whatshisface 6y ago
        Math and chess are both very easy to check. Proof checkers and chess rule checkers both exist. "Conversation checkers" do not.

ajnin 6y ago

Your comment reminds me of Gödel's proof of his incompleteness theorem. Basically, he said that if you treat a mathematical statement as a sequence of tokens, and then assign a number to each token, then you can transform the statement into a big number. Then, going one step further, if a mathematical proof is a sequence of statements then it can be too transformed into a really long number. Then you can come up with rules to manipulate these numbers to create new valid statements and proofs. I don't know if there was much work done on this idea beyond Gödel's proof, but I think it's a really neat idea that gives a way to manipulate mathematical proofs as objects and create new ones from a very high level view.