6 ms·

This is the opposite direction to what I expected to see for new theorem proving efforts: "Good old fashioned AI" vs leveraging advances of deep learning for na

by dzdt 4y ago

This is the opposite direction to what I expected to see for new theorem proving efforts: "Good old fashioned AI" vs leveraging advances of deep learning for natural language. I think the direction that is ripe for advance is a two-part process: (1) translating from human-language mathematics proof to computer-verifiable formal proof language combine with (2) GPT3-style automated generation of plausible next-steps in human language proofs. Gowers emphasizes the success of humans at "pruning" to only consider potentially useful next steps in a proof. I think GPT3 demonstrates such pruning in generating plausible natural language text continuations. And the success of natural language translation between natural languages suggests natural->formal language translation may also be ripe. Combined with the success of formal language automated theorem provers, it seems plausible to build on current technologies a stack that produces formally verified natural language proofs.

ImprobableTruth 4y ago
Human-language proofs for anything non-trivial are really just proof sketches, that's why you can't really meaningfully separate this into a two step process.
yaseer 4y ago
I don't think Gowers is trying to build a better theorem prover. An AI researcher would be trying to build a better prover. Gowers is a mathematician looking for mathematical insight. This project's success would be based on how well it answers those fundamental questions he posed (i.e How does a human generate proofs, given no algorithm exists to solve the halting problem?) The output might be more like meta mathematics, with insights provided by software, rather than ML software optimised for a goal.
- amelius 4y ago
  They can still use ML to prune the search space, I suppose?
  - yaseer 4y ago
    For a mathematician, it's not the output of pruning the search space, but understanding how the search space is pruned. Understanding how ML models work is a notorious problem. A classical algorithm can be formally understood better - I think it's this mathematical understanding Gowers is looking for.
    - amelius 4y ago
      But isn't that how humans do it too? They have a hunch, pursue it, and if it doesn't work out, they backtrack. Of course, some people have better hunches than others, but that doesn't change the global idea.
      - jhgb 4y ago
        ...and they largely don't know where those hunches came from.
        tsukikage 4y ago
        ...well, quite. But that's not really the "move along, nothing to see here" it first sounds like. "Hunch" is a label we use for "I don't know explicitly how I came up with this". Generally, when we have a label for a concept the description of which starts with "I don't know...", some people try and follow up with questions: is that a thing it is possible, in principle, to know? How could we find out for certain? If it's knowable, how do we get to know what it is? Sometimes, they succeed, and generations of such successes is how we end up with the modern world.
      - yaseer 4y ago
        > They have a hunch, pursue it There's a lot to unpack in just this. Can we define an algorithm to generate hunches? (mathematical intuition). Given infinite hunches, can we define an algorithm to order hunches by priority, to search? That's the kind of question they'll be thinking about using the symbolic logic/classical algorithms in GOFAI approaches.
- gnramires 4y ago
  > How does a human generate proofs, given no algorithm exists to solve the halting problem? To be fair, this has some trivial answers -- despite being a fascinating question. For example, given a formal proof verification system (e.g. Lean), you can search for proofs (either by brute force or hopefully using heuristics) and if a proof exists, you will find it after some finite time. The problem is that sometimes no proof exists. You may be thinking of getting "smart", and also trying to prove no proof exists in parallel. But that's just another proof, such that this recursion tower (proof that (proof that (... proof doesn't exist)) doesn't resolve. But I think overall this mostly means you should be able to accept non-existence or arbitrary proving times of proofs (maybe also a sociological problem for mathematicians!). That's of course how human mathematics works: no one now if any famous theorem (e.g. Riemann hypothesis) will be proven within some time frame, or maybe never.
tgb 4y ago
I’m also skeptical of the approach here but for the opposite reason. ML will conquer proofs by an AlphaZero approach of ignoring all human training data. You can generate arbitrary problems easily enough and doing some GAN like system of both generating problems that yet can’t be solved and a solver to solve them seems to obviate the need for human training data. I’d be really hesitant to be a PhD student in the GOFAI or natural language datamining approaches since I think this could easily be solved by ML in the next five or ten years by ML (specifically at least one well known unsolved research problem being solved by AI). I hope that I’m wrong… I like math as a human endeavor.
- deadbeef57 4y ago
  Such an "AlphaZero approach" will only knock Gowers's GOFAI approach out of business if the AI can also "justify" its proofs, in the sense that Gowers explains in his blogpost. Do you think that will happen in 5 years?
  - btilly 4y ago
    I find myself doubting that this goal makes any sense. One mathematician often cannot "justify" their reasoning process to another if their thinking is even slightly different. For example what is intuitive for one side of the algebra/analysis divide is often not to people on the other side. It is therefore unlikely that a human level computer program will think enough like humans that it can be justified to any human. And vice versa. For it to do so, it has to be better than the human, also have a model of how the human thinks, and then be able to break down thinking it arrived at one way to something that makes sense to the human. If a computer succeeded in this endeavor, it would almost certainly come up with new principles of doing mathematics that would then have to be taught to humans to for humans to appreciate what it is doing. Something like this has already happened with Go, see https://escholarship.org/uc/item/6q05n7pz https://escholarship.org/uc/item/6q05n7pz for example. Even so, humans are still unable to learn to play the game at the same level as the superhuman program. And the same would be true in mathematics.
    - deadbeef57 4y ago
TimPC 4y ago
GPT3 style automated generation of plausible next steps in human language proofs is a disaster waiting to happen. GPT3 generates vaguely plausible text sequences without understanding the material. It relies heavily on the imprecision of language and the fact that there are many plausible words in sentences. It doesn't even perfectly capture the rules of grammar as it sometimes makes mistakes of a grammatical nature. Consider that mathematics requires greater precision in that the language has more exacting meanings and fewer plausible alternatives. Also consider that the bar to doing something useful in mathematics is extremely high. We're not trying to GPT3 a plausible sentence now, we're trying to guide GPT3 to producing the complete works of shakespeare. GPT3 demonstrates a kind of pruning for generating viable text in natural language continuations but I'd argue it is nothing like pruning useful next steps of a proof. The pruning in GPT3 works as a probability model and is derived from a good data set of human utterances. Generating a good dataset of plausible and implausible next steps in mathematical proofs is a much harder problem. The cost per instance is extremely high as all of the proofs have to be translated into a specific precise formal language (otherwise you explode the search space to be any plausible utterance in some form of English+Math Symbols making the problem much harder). Even worse, different theorem provers want to use different formal languages making the reusability of the data set less than typical in ML problems. The dataset is also far smaller. How many interesting proofs in mathematics are at a suitable depth from the initialization of a theorem prover with just some basic axioms? Even if you solve the dataset problem though there are further problems. GPT3 isn't designed to evaluate the interestingness of a sentence, only the plausibility with hopes that the context in which the sentence is generated provides enough relevance. In short, I'm highly skeptical that benefits in natural language translation will translate to formal languages. I'd also argue the problems you classify into "formal language translation" aren't even translation problems. I also think very few people see the technologies you've mentioned as related (for good reason) and I think a program that attempts to build on them is likely to fail.
- dzdt 4y ago
  Fair enough to be skeptical. Some responses to your points: > the bar to doing something useful in mathematics is extremely high Ah but the bar to do something interesting in automated theorem proving is much lower. Solving exercises from an advanced undergraduate class involving proofs would already be of interest. > Generating a good dataset of plausible and implausible next steps in mathematical proofs is a much harder problem. There are thousands of textbooks, monographs, and research mathematical journals. There really is a gigantic corpus of natural language mathematical proofs to study. In graduate school there were a bunch of homework proofs which the professors would describe as "follow your nose" : after you make an initial step in the right direction the remaining steps followed the kind of pattern that quickly becomes familiar. I think it is very plausible that a GPT3 style system trained on mathematical writing could learn these "follow your nose" patterns. > problems you classify into "formal language translation" aren't even translation problems Fair. Going from natural language proofs like from a textbook to a formal language like automatic theorem provers use has similarities to a natural language translation problem but it would be fair to say that this is its own category of problem.

by dzdt 4y ago

ImprobableTruth 4y ago

Human-language proofs for anything non-trivial are really just proof sketches, that's why you can't really meaningfully separate this into a two step process.

yaseer 4y ago

I don't think Gowers is trying to build a better theorem prover. An AI researcher would be trying to build a better prover. Gowers is a mathematician looking for mathematical insight. This project's success would be based on how well it answers those fundamental questions he posed (i.e How does a human generate proofs, given no algorithm exists to solve the halting problem?) The output might be more like meta mathematics, with insights provided by software, rather than ML software optimised for a goal.

amelius 4y ago
They can still use ML to prune the search space, I suppose?
- yaseer 4y ago
  For a mathematician, it's not the output of pruning the search space, but understanding how the search space is pruned. Understanding how ML models work is a notorious problem. A classical algorithm can be formally understood better - I think it's this mathematical understanding Gowers is looking for.
  - amelius 4y ago
    But isn't that how humans do it too? They have a hunch, pursue it, and if it doesn't work out, they backtrack. Of course, some people have better hunches than others, but that doesn't change the global idea.
    - jhgb 4y ago
      ...and they largely don't know where those hunches came from.
      - tsukikage 4y ago
        ...well, quite. But that's not really the "move along, nothing to see here" it first sounds like. "Hunch" is a label we use for "I don't know explicitly how I came up with this". Generally, when we have a label for a concept the description of which starts with "I don't know...", some people try and follow up with questions: is that a thing it is possible, in principle, to know? How could we find out for certain? If it's knowable, how do we get to know what it is? Sometimes, they succeed, and generations of such successes is how we end up with the modern world.
    - yaseer 4y ago
      > They have a hunch, pursue it There's a lot to unpack in just this. Can we define an algorithm to generate hunches? (mathematical intuition). Given infinite hunches, can we define an algorithm to order hunches by priority, to search? That's the kind of question they'll be thinking about using the symbolic logic/classical algorithms in GOFAI approaches.
gnramires 4y ago
> How does a human generate proofs, given no algorithm exists to solve the halting problem? To be fair, this has some trivial answers -- despite being a fascinating question. For example, given a formal proof verification system (e.g. Lean), you can search for proofs (either by brute force or hopefully using heuristics) and if a proof exists, you will find it after some finite time. The problem is that sometimes no proof exists. You may be thinking of getting "smart", and also trying to prove no proof exists in parallel. But that's just another proof, such that this recursion tower (proof that (proof that (... proof doesn't exist)) doesn't resolve. But I think overall this mostly means you should be able to accept non-existence or arbitrary proving times of proofs (maybe also a sociological problem for mathematicians!). That's of course how human mathematics works: no one now if any famous theorem (e.g. Riemann hypothesis) will be proven within some time frame, or maybe never.

tgb 4y ago

I’m also skeptical of the approach here but for the opposite reason. ML will conquer proofs by an AlphaZero approach of ignoring all human training data. You can generate arbitrary problems easily enough and doing some GAN like system of both generating problems that yet can’t be solved and a solver to solve them seems to obviate the need for human training data. I’d be really hesitant to be a PhD student in the GOFAI or natural language datamining approaches since I think this could easily be solved by ML in the next five or ten years by ML (specifically at least one well known unsolved research problem being solved by AI). I hope that I’m wrong… I like math as a human endeavor.

deadbeef57 4y ago
Such an "AlphaZero approach" will only knock Gowers's GOFAI approach out of business if the AI can also "justify" its proofs, in the sense that Gowers explains in his blogpost. Do you think that will happen in 5 years?
- btilly 4y ago
  I find myself doubting that this goal makes any sense. One mathematician often cannot "justify" their reasoning process to another if their thinking is even slightly different. For example what is intuitive for one side of the algebra/analysis divide is often not to people on the other side. It is therefore unlikely that a human level computer program will think enough like humans that it can be justified to any human. And vice versa. For it to do so, it has to be better than the human, also have a model of how the human thinks, and then be able to break down thinking it arrived at one way to something that makes sense to the human. If a computer succeeded in this endeavor, it would almost certainly come up with new principles of doing mathematics that would then have to be taught to humans to for humans to appreciate what it is doing. Something like this has already happened with Go, see https://escholarship.org/uc/item/6q05n7pz https://escholarship.org/uc/item/6q05n7pz for example. Even so, humans are still unable to learn to play the game at the same level as the superhuman program. And the same would be true in mathematics.
  - deadbeef57 4y ago

TimPC 4y ago

GPT3 style automated generation of plausible next steps in human language proofs is a disaster waiting to happen. GPT3 generates vaguely plausible text sequences without understanding the material. It relies heavily on the imprecision of language and the fact that there are many plausible words in sentences. It doesn't even perfectly capture the rules of grammar as it sometimes makes mistakes of a grammatical nature. Consider that mathematics requires greater precision in that the language has more exacting meanings and fewer plausible alternatives. Also consider that the bar to doing something useful in mathematics is extremely high. We're not trying to GPT3 a plausible sentence now, we're trying to guide GPT3 to producing the complete works of shakespeare. GPT3 demonstrates a kind of pruning for generating viable text in natural language continuations but I'd argue it is nothing like pruning useful next steps of a proof. The pruning in GPT3 works as a probability model and is derived from a good data set of human utterances. Generating a good dataset of plausible and implausible next steps in mathematical proofs is a much harder problem. The cost per instance is extremely high as all of the proofs have to be translated into a specific precise formal language (otherwise you explode the search space to be any plausible utterance in some form of English+Math Symbols making the problem much harder). Even worse, different theorem provers want to use different formal languages making the reusability of the data set less than typical in ML problems. The dataset is also far smaller. How many interesting proofs in mathematics are at a suitable depth from the initialization of a theorem prover with just some basic axioms? Even if you solve the dataset problem though there are further problems. GPT3 isn't designed to evaluate the interestingness of a sentence, only the plausibility with hopes that the context in which the sentence is generated provides enough relevance. In short, I'm highly skeptical that benefits in natural language translation will translate to formal languages. I'd also argue the problems you classify into "formal language translation" aren't even translation problems. I also think very few people see the technologies you've mentioned as related (for good reason) and I think a program that attempts to build on them is likely to fail.

dzdt 4y ago
Fair enough to be skeptical. Some responses to your points: > the bar to doing something useful in mathematics is extremely high Ah but the bar to do something interesting in automated theorem proving is much lower. Solving exercises from an advanced undergraduate class involving proofs would already be of interest. > Generating a good dataset of plausible and implausible next steps in mathematical proofs is a much harder problem. There are thousands of textbooks, monographs, and research mathematical journals. There really is a gigantic corpus of natural language mathematical proofs to study. In graduate school there were a bunch of homework proofs which the professors would describe as "follow your nose" : after you make an initial step in the right direction the remaining steps followed the kind of pattern that quickly becomes familiar. I think it is very plausible that a GPT3 style system trained on mathematical writing could learn these "follow your nose" patterns. > problems you classify into "formal language translation" aren't even translation problems Fair. Going from natural language proofs like from a textbook to a formal language like automatic theorem provers use has similarities to a natural language translation problem but it would be fair to say that this is its own category of problem.