I have a couple friends who did the Math tripos at Cambridge (so a pretty high level!) who work in tech and have unanimously said they have 0% expectations of an LLM doing a millennium problem anytime soon
Yeah, millennium problems almost certainly require truly novel nontrivial ideas to solve.
That's a tough thing for AI to do.
On the other hand, Terrence Tao had an interesting article on his blog a while back where he was trying to solve a problem and asked chatGPT about it in a high-level strategy sense. ChatGPT suggested several reasonable approaches, one of which turned out to work.
That's nowhere near solving a millennium problem, but it is very interesting and suggests fairly sophisticated conceptual understanding of mathematics nevertheless.
Current architecture and training methods I don't think are enough to get there. However, with enough compute, I can plausibly envision some sort of meta training of LLMs using an analogy to GANs where one network tries to synthesize new correct ideas and the other shoots them down as not novel, not correct, or not sufficiently interesting.
Such an approach I think could perhaps work, but the compute needed would probably be pretty high.
And also if you could combine that with some kind of representation software like Lean that can validate proofs, perhaps you can generate some kind of targeted search of the problem space and with a combination of a general high level strategy and maybe brute force of some sub-problems, find novel solutions. My understanding is that is the common human approach: gain some kind of intuition of problem, try a few things and then iteratively refine. Sometimes that works, sometimes you need to find a new starting point. It seems plausible we could automate that workflow, with likely mixed but still useful results.
I’m not trying to understate the stuff you can do with LLMs or formal proof tooling that could be attached to randomly try things till it reaches a solution to a novel problem, but some solutions you see to lesser problems are sometimes so pie-in-the-sky I think stumbling on one is barely better than a random walk. And I think mathematicians like Tao are far better at narrowing that down. As an aide I can see it’s use, I just don’t believe we’re going to have LLMs & tooling solve these grand problems until compute power is orders of magnitudes better, and even then I’m still sceptical. BUT I’m not a mathematician and this is based on my intuition from pub talks :)
Yeah, but none of that gets you a solution to a Millennium problem. One needs an AI to do something like what Peter Scholze did in inventing perfectoid spaces or Perelman in introducing his entropy function. You can treat axiom invention as a game, I suppose, but the space of possible moves is uhh rather large.
The field of LLM reasoning is far from stable atm. I think it's pretty hard for anyone to give confident predictions about what they can or cannot do in 5 years. In that light, I am skeptical about any claims that they cannot do something anytime soon.
What does an LLM really do? And can it create sometimes entirely novel math that goes against its training set to solve something, and know it’s right using a proof tool that may not even accept that? I agree but on a different order of magnitude of years.
Yeah, millennium problems almost certainly require truly novel nontrivial ideas to solve.
That's a tough thing for AI to do.
On the other hand, Terrence Tao had an interesting article on his blog a while back where he was trying to solve a problem and asked chatGPT about it in a high-level strategy sense. ChatGPT suggested several reasonable approaches, one of which turned out to work.
That's nowhere near solving a millennium problem, but it is very interesting and suggests fairly sophisticated conceptual understanding of mathematics nevertheless.
Current architecture and training methods I don't think are enough to get there. However, with enough compute, I can plausibly envision some sort of meta training of LLMs using an analogy to GANs where one network tries to synthesize new correct ideas and the other shoots them down as not novel, not correct, or not sufficiently interesting.
Such an approach I think could perhaps work, but the compute needed would probably be pretty high.
And also if you could combine that with some kind of representation software like Lean that can validate proofs, perhaps you can generate some kind of targeted search of the problem space and with a combination of a general high level strategy and maybe brute force of some sub-problems, find novel solutions. My understanding is that is the common human approach: gain some kind of intuition of problem, try a few things and then iteratively refine. Sometimes that works, sometimes you need to find a new starting point. It seems plausible we could automate that workflow, with likely mixed but still useful results.
I’m not trying to understate the stuff you can do with LLMs or formal proof tooling that could be attached to randomly try things till it reaches a solution to a novel problem, but some solutions you see to lesser problems are sometimes so pie-in-the-sky I think stumbling on one is barely better than a random walk. And I think mathematicians like Tao are far better at narrowing that down. As an aide I can see it’s use, I just don’t believe we’re going to have LLMs & tooling solve these grand problems until compute power is orders of magnitudes better, and even then I’m still sceptical. BUT I’m not a mathematician and this is based on my intuition from pub talks :)
Ask yourself what mathematicians do today...
They decompose problems, solve specialized subsets, examine more general cases, use existing proofs, do some numerical analysis, etc.
Yeah, but none of that gets you a solution to a Millennium problem. One needs an AI to do something like what Peter Scholze did in inventing perfectoid spaces or Perelman in introducing his entropy function. You can treat axiom invention as a game, I suppose, but the space of possible moves is uhh rather large.
The field of LLM reasoning is far from stable atm. I think it's pretty hard for anyone to give confident predictions about what they can or cannot do in 5 years. In that light, I am skeptical about any claims that they cannot do something anytime soon.
What does an LLM really do? And can it create sometimes entirely novel math that goes against its training set to solve something, and know it’s right using a proof tool that may not even accept that? I agree but on a different order of magnitude of years.