6 ms·

> First, the problems were manually translated into formal mathematical language for our systems to understand. In the official competition, students submit ans

> First, the problems were manually translated into formal mathematical language for our systems to understand. In the official competition, students submit answers in two sessions of 4.5 hours each. Our systems solved one problem within minutes and took up to three days to solve the others. Three days is interesting... Not technically silver medal performance I guess, but let's be real I'd be okay waiting a month for the cure to cancer.

ZenMikey 2y ago
I haven't read TFA as I'm at work, but I would be very interested to know what the system was doing in those three days. Were there failed branches it explored? Was it just fumbling its way around until it guessed correctly? What did the feedback loop look like?
- qsort 2y ago
  I can't find a link to an actual paper, that just seems to be a blog post. But from what I gather the problems were manually translated to Lean 4, and then the program is doing some kind of tree search. I'm assuming they are leveraging the proof checker to provide feedback to the model.
- tsoj 2y ago
  This is NOT the paper, but probably a very similar solution: https://arxiv.org/abs/2009.03393 https://arxiv.org/abs/2009.03393
- visarga 2y ago
  > just fumbling its way around until it guessed correctly As opposed to 0.999999% of the human population who can't do it even if their life depends on it?
  - dsign 2y ago
    I was going to come here to say that. I remember being a teenager and giving up in frustration at IMO problems. And I was competing at IPhO.
    - kevinventullo 2y ago
      Yeah, as a former research mathematician, I think “fumbling around blindly” is not an entirely unfair description of the research process. I believe even Wiles in a documentary described his search for the proof of Fermat’s last theorem as groping around in a pitch black room, but once the proof was discovered it was like someone turned the lights on.
  - logicchains 2y ago
    I guess you mean 99.9999%?
- lacker 2y ago
  The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found. So they had three days to keep training the model, on synthetic variations of each IMO problem.
- thomasahle 2y ago
  They just write "it's like alpha zero". So presumably they used a version of MCTS where each terminal node is scored by LEAN as either correct or incorrect. Then they can train a network to evaluate intermediate positions (score network) and one to suggest things to try next (policy network).
- utopcell 2y ago
  I'm at work and reading this article is the first thing I did this morning. What's your point ?
ComplexSystems 2y ago
Or the simultaneous discovery of thousands of cryptographic exploits...
- poincaredisk 2y ago
  Still waiting for the first one. I'm not holding my breath - just like fuzzing found a lot of vulnerabilities in low-level software, I expect novel automated analysis approaches will yield some vulnerabilities - but that won't be a catastrophic event just like fuzzing wasn't.
  - sqeaky 2y ago
    I hope it doesn't find a new class of bug. Find another thing like Spectre could be problematic. EDIT - I hope if that new class of bug exists that it is found. I hope that new class of bug doesn't exist.
  - throwaway240403 2y ago
    Hope that's true. Really mucks up the world a bit if not.
  - criddell 2y ago
    It's rumored that the NSA has 600 mathematicians working for them. If they are the ones finding the exploits you will probably never hear about them until they are independently discovered by someone who can publish.
  - ComplexSystems 2y ago
    Why don't you think that AI models will, perhaps rather soon, surpass human capabilities in finding security vulnerabilities? Because an AI that's even equally competent would be a fairly catastrophic event.
nnarek 2y ago
"three days" does not say anything about how much computational power is used to solve problems, maybe they have used 10% of all GCP :)
- vlovich123 2y ago
  The thing is though, once we have a benchmark that we pass, it’s pretty typical to be able to bring down time required in short order through performance improvements and iterating on ideas. So if you knew you had GAI but it took 100% of all GCP for 3 years to give a result, within the next 5 years that would come down significantly (not least of which you’d build HW dedicated to accelerating the slow parts).
  - tsimionescu 2y ago
    That's patently false for many classes of problems. We know exactly how to solve the traveling salesman problem, and have for decades, but we're nowhere close to solving a random 1000 city case (note: there are approximate methods that can find good, but not optimal, results on millions of cities). Edit: I should say 1,000,000 city problem, as there are some solutions for 30-60k cities from the 2000s. And there are good reasons to believe that theorem finding and proof generation are at least NP-hard problems.
    - rowanG077 2y ago
      The person said typical not always the case. Just because there are obviously cases where it didn't happen does mean it it's still not typically the case.
    - vlovich123 2y ago
      We're not talking about mathematical optimality here, both from the solution found and for the time taken. The point is whether this finds results more cheaply than a human can and right now it's better on some problems while others it's worse. Clearly if a human can do it, there is a way to solve it in a cheaper amount of time and it would be flawed reasoning to think that improving the amount of time would be asymptotically optimal already. While I agree that not all problems show this kind of acceleration in performance, that's typically only true if you've already spent so much time trying to solve it that you've asymptoted to the optimal solution. Right now we're nowhere near the asymptote for AI improvements. Additionally, there's so many research dollars flowing into AI precisely because the potential upside here is nowhere near realized and there's lots of research lines still left to be explored. George Hinton ended the AI winter.
wongarsu 2y ago
The problem solved "within minutes" is also interesting. I'd interpret that as somewhere between 2 and 59 minutes. Given the vagueness probably on the higher end, otherwise they'd celebrate it more. The students had 6 tasks in 9 hours, so on average 1.5h per task. If you add the time a student would take to (correctly!) translate the problems to their input format, their best-case runtime is probably about as fast as a silver-medalist would take to solve the problem on their own. But even if they aren't as fast as humans yet this is very valuable. Both as a stepping stone, and because at a certain scale compute is much easier to scale than skilled mathematicians.
- gjm11 2y ago
  They say "our systems" (presumably meaning AlphaProof and AlphaGeometry 2) solved one problem "within minutes", and later on the page they say that the geometry question (#4) was solved by AlphaGeometry in 19 seconds. So either (1) "within minutes" was underselling the abilities of the system, or (2) what they actually meant was that the geometry problem was solved in 19 seconds, one of the others "within minutes" (I'd guess #1 which is definitely easier than the other two they solved), and the others in unspecified times of which the longer was ~3 days. I'd guess it's the first of those. (Euclidean geometry has been a kinda-solved domain for some time; it's not super-surprising that they were able to solve that problem quickly.) As for the long solve times, I would guess they're related to this fascinating remark: > The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found.
  - visarga 2y ago
    Euclidian Geometry still requires constructions to solve, and those are based in intuition.
    - gjm11 2y ago
      There are known algorithms that can solve _all_ problems in euclidean (ruler-and-compasses) geometry, no intuition required. The most effective algorithms of this type are quite inefficient, though, and (at least according to DeepMind) don't do as well as AlphaGeometry does at e.g. IMO geometry problems.
lolinder 2y ago
It feels pretty disingenuous to claim silver-medal status when your machine played by significantly different rules. The article is light on details, but it says they wired it up to a theorem prover, presumably with feedback sent back to the AI model for re-evaluation. How many cycles of guess-and-check did it take over the course of three days to get the right answer? If the IMO contestants were allowed to use theorem provers and were given 3 days (even factoring in sleep) would AlphaProof still have gotten silver? > let's be real I'd be okay waiting a month for the cure to cancer. I don't think these results suggest that we're on the brink of knowledge coming at a substantially faster rate than before. Humans have been using theorem provers to advance our understanding for decades. Now an LLM has been wired up to one too, but it still took 8x as long to solve the problems as our best humans did without any computer assistance.
- ToucanLoucan 2y ago
  I am so exhausted of the AI hype nonsense. LLMs are not fucking curing cancer. Not now, not in five years, not in a hundred years. That's not what they do. LLM/ML is fascinating tech that has a lot of legitimate applications, but it is not fucking intelligent, artificial or otherwise, and I am sick to death of people treating it like it is.
  - apsec112 2y ago
    What observation, if you saw it, do you think would falsify that hypothesis?
    - necovek 2y ago
      It seems unlikely people will employ only ML models, especially LLM, to achieve great results: they will combine it with human insights (through direction and concrete algorithms). It's obvious that's happening with LLMs even today to ensure they don't spew out too much bullshit or harmful content. So let's get to a point where we can trust AI as-is first, and let's talk about what's needed to achieve the next milestone after and if we get there. And I love asking every new iteration of ChatGPT/Gemini something along the lines of "What day was yesterday if yesterday was a Thursday?" It just makes me giggle.
10100110 2y ago
Don't confuse interpolation with extrapolation. Curing cancer will require new ideas. IMO requires skill proficiency in tasks where the methods of solving are known.
- trueismywork 2y ago
  They are the same things
- golol 2y ago
  Mathematicians spend most of their time interpolating between known ideas and it would be extremely helpful to have computer assistance with that.
- visarga 2y ago
  Search is extrapolation. Learning is interpolation. Search+Learn is the formula used by AZ. Don't forget AZ taught us humans a thing or two about a game we had 2000 years head start in, and starting from scratch not from human supervision.
  - xdavidliu 2y ago
    no, search is not extrapolation. Extrapolation means taking some data and projecting out beyond the limits of that data. For example, if my bank account had $10 today and $20 tomorrow, then I can extrapolate and say it might have $30 the day after tomorrow. Interpolation means taking some data and inferring the gaps of that data. For example, if I had $10 today and $30 the day after tomorrow, I can interpolate and say I probably had $20 tomorrow. Search is different from either of those things, it's when you have a target and a collection of other things, and are trying to find the target in that collection.
    - visarga 2y ago
      Search can go from a random init model to beating humans at Go. That is not interpolation. - Search allows exploration of the game tree, potentially finding novel strategies. - Learning compresses the insights gained from search into a more efficient policy. - This compressed policy then guides future searches more effectively. Evolution is also a form of search, and it is open-ended. AlphaProof solved IMO problems, those are chosen to be out of distribution, simple imitation can't solve them. Scientists do (re)search, they find novel insights nobody else discovered before. What I want to say is that search is on a whole different level than what neural nets do, they can only interpolate their training data, search pushes outside of the known data distribution. It's actually a combo of search+learning that is necessary, learning is just the little brother of search, it compresses novel insights into the model. You can think of training a neural net also as search - the best parameters that would fit the training set.

ZenMikey 2y ago

I haven't read TFA as I'm at work, but I would be very interested to know what the system was doing in those three days. Were there failed branches it explored? Was it just fumbling its way around until it guessed correctly? What did the feedback loop look like?

qsort 2y ago
I can't find a link to an actual paper, that just seems to be a blog post. But from what I gather the problems were manually translated to Lean 4, and then the program is doing some kind of tree search. I'm assuming they are leveraging the proof checker to provide feedback to the model.
tsoj 2y ago
This is NOT the paper, but probably a very similar solution: https://arxiv.org/abs/2009.03393 https://arxiv.org/abs/2009.03393
visarga 2y ago
> just fumbling its way around until it guessed correctly As opposed to 0.999999% of the human population who can't do it even if their life depends on it?
- dsign 2y ago
  I was going to come here to say that. I remember being a teenager and giving up in frustration at IMO problems. And I was competing at IPhO.
  - kevinventullo 2y ago
    Yeah, as a former research mathematician, I think “fumbling around blindly” is not an entirely unfair description of the research process. I believe even Wiles in a documentary described his search for the proof of Fermat’s last theorem as groping around in a pitch black room, but once the proof was discovered it was like someone turned the lights on.
- logicchains 2y ago
  I guess you mean 99.9999%?
lacker 2y ago
The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found. So they had three days to keep training the model, on synthetic variations of each IMO problem.
thomasahle 2y ago
They just write "it's like alpha zero". So presumably they used a version of MCTS where each terminal node is scored by LEAN as either correct or incorrect. Then they can train a network to evaluate intermediate positions (score network) and one to suggest things to try next (policy network).
utopcell 2y ago
I'm at work and reading this article is the first thing I did this morning. What's your point ?

ComplexSystems 2y ago

Or the simultaneous discovery of thousands of cryptographic exploits...

poincaredisk 2y ago
Still waiting for the first one. I'm not holding my breath - just like fuzzing found a lot of vulnerabilities in low-level software, I expect novel automated analysis approaches will yield some vulnerabilities - but that won't be a catastrophic event just like fuzzing wasn't.
- sqeaky 2y ago
  I hope it doesn't find a new class of bug. Find another thing like Spectre could be problematic. EDIT - I hope if that new class of bug exists that it is found. I hope that new class of bug doesn't exist.
- throwaway240403 2y ago
  Hope that's true. Really mucks up the world a bit if not.
- criddell 2y ago
  It's rumored that the NSA has 600 mathematicians working for them. If they are the ones finding the exploits you will probably never hear about them until they are independently discovered by someone who can publish.
- ComplexSystems 2y ago
  Why don't you think that AI models will, perhaps rather soon, surpass human capabilities in finding security vulnerabilities? Because an AI that's even equally competent would be a fairly catastrophic event.

nnarek 2y ago

"three days" does not say anything about how much computational power is used to solve problems, maybe they have used 10% of all GCP :)

vlovich123 2y ago
The thing is though, once we have a benchmark that we pass, it’s pretty typical to be able to bring down time required in short order through performance improvements and iterating on ideas. So if you knew you had GAI but it took 100% of all GCP for 3 years to give a result, within the next 5 years that would come down significantly (not least of which you’d build HW dedicated to accelerating the slow parts).
- tsimionescu 2y ago
  That's patently false for many classes of problems. We know exactly how to solve the traveling salesman problem, and have for decades, but we're nowhere close to solving a random 1000 city case (note: there are approximate methods that can find good, but not optimal, results on millions of cities). Edit: I should say 1,000,000 city problem, as there are some solutions for 30-60k cities from the 2000s. And there are good reasons to believe that theorem finding and proof generation are at least NP-hard problems.
  - rowanG077 2y ago
    The person said typical not always the case. Just because there are obviously cases where it didn't happen does mean it it's still not typically the case.
  - vlovich123 2y ago
    We're not talking about mathematical optimality here, both from the solution found and for the time taken. The point is whether this finds results more cheaply than a human can and right now it's better on some problems while others it's worse. Clearly if a human can do it, there is a way to solve it in a cheaper amount of time and it would be flawed reasoning to think that improving the amount of time would be asymptotically optimal already. While I agree that not all problems show this kind of acceleration in performance, that's typically only true if you've already spent so much time trying to solve it that you've asymptoted to the optimal solution. Right now we're nowhere near the asymptote for AI improvements. Additionally, there's so many research dollars flowing into AI precisely because the potential upside here is nowhere near realized and there's lots of research lines still left to be explored. George Hinton ended the AI winter.

wongarsu 2y ago

The problem solved "within minutes" is also interesting. I'd interpret that as somewhere between 2 and 59 minutes. Given the vagueness probably on the higher end, otherwise they'd celebrate it more. The students had 6 tasks in 9 hours, so on average 1.5h per task. If you add the time a student would take to (correctly!) translate the problems to their input format, their best-case runtime is probably about as fast as a silver-medalist would take to solve the problem on their own. But even if they aren't as fast as humans yet this is very valuable. Both as a stepping stone, and because at a certain scale compute is much easier to scale than skilled mathematicians.

gjm11 2y ago
They say "our systems" (presumably meaning AlphaProof and AlphaGeometry 2) solved one problem "within minutes", and later on the page they say that the geometry question (#4) was solved by AlphaGeometry in 19 seconds. So either (1) "within minutes" was underselling the abilities of the system, or (2) what they actually meant was that the geometry problem was solved in 19 seconds, one of the others "within minutes" (I'd guess #1 which is definitely easier than the other two they solved), and the others in unspecified times of which the longer was ~3 days. I'd guess it's the first of those. (Euclidean geometry has been a kinda-solved domain for some time; it's not super-surprising that they were able to solve that problem quickly.) As for the long solve times, I would guess they're related to this fascinating remark: > The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found.
- visarga 2y ago
  Euclidian Geometry still requires constructions to solve, and those are based in intuition.
  - gjm11 2y ago
    There are known algorithms that can solve _all_ problems in euclidean (ruler-and-compasses) geometry, no intuition required. The most effective algorithms of this type are quite inefficient, though, and (at least according to DeepMind) don't do as well as AlphaGeometry does at e.g. IMO geometry problems.

lolinder 2y ago

It feels pretty disingenuous to claim silver-medal status when your machine played by significantly different rules. The article is light on details, but it says they wired it up to a theorem prover, presumably with feedback sent back to the AI model for re-evaluation. How many cycles of guess-and-check did it take over the course of three days to get the right answer? If the IMO contestants were allowed to use theorem provers and were given 3 days (even factoring in sleep) would AlphaProof still have gotten silver? > let's be real I'd be okay waiting a month for the cure to cancer. I don't think these results suggest that we're on the brink of knowledge coming at a substantially faster rate than before. Humans have been using theorem provers to advance our understanding for decades. Now an LLM has been wired up to one too, but it still took 8x as long to solve the problems as our best humans did without any computer assistance.

ToucanLoucan 2y ago
I am so exhausted of the AI hype nonsense. LLMs are not fucking curing cancer. Not now, not in five years, not in a hundred years. That's not what they do. LLM/ML is fascinating tech that has a lot of legitimate applications, but it is not fucking intelligent, artificial or otherwise, and I am sick to death of people treating it like it is.
- apsec112 2y ago
  What observation, if you saw it, do you think would falsify that hypothesis?
  - necovek 2y ago
    It seems unlikely people will employ only ML models, especially LLM, to achieve great results: they will combine it with human insights (through direction and concrete algorithms). It's obvious that's happening with LLMs even today to ensure they don't spew out too much bullshit or harmful content. So let's get to a point where we can trust AI as-is first, and let's talk about what's needed to achieve the next milestone after and if we get there. And I love asking every new iteration of ChatGPT/Gemini something along the lines of "What day was yesterday if yesterday was a Thursday?" It just makes me giggle.

10100110 2y ago

Don't confuse interpolation with extrapolation. Curing cancer will require new ideas. IMO requires skill proficiency in tasks where the methods of solving are known.

trueismywork 2y ago
They are the same things
golol 2y ago
Mathematicians spend most of their time interpolating between known ideas and it would be extremely helpful to have computer assistance with that.
visarga 2y ago
Search is extrapolation. Learning is interpolation. Search+Learn is the formula used by AZ. Don't forget AZ taught us humans a thing or two about a game we had 2000 years head start in, and starting from scratch not from human supervision.
- xdavidliu 2y ago
  no, search is not extrapolation. Extrapolation means taking some data and projecting out beyond the limits of that data. For example, if my bank account had $10 today and $20 tomorrow, then I can extrapolate and say it might have $30 the day after tomorrow. Interpolation means taking some data and inferring the gaps of that data. For example, if I had $10 today and $30 the day after tomorrow, I can interpolate and say I probably had $20 tomorrow. Search is different from either of those things, it's when you have a target and a collection of other things, and are trying to find the target in that collection.
  - visarga 2y ago
    Search can go from a random init model to beating humans at Go. That is not interpolation. - Search allows exploration of the game tree, potentially finding novel strategies. - Learning compresses the insights gained from search into a more efficient policy. - This compressed policy then guides future searches more effectively. Evolution is also a form of search, and it is open-ended. AlphaProof solved IMO problems, those are chosen to be out of distribution, simple imitation can't solve them. Scientists do (re)search, they find novel insights nobody else discovered before. What I want to say is that search is on a whole different level than what neural nets do, they can only interpolate their training data, search pushes outside of the known data distribution. It's actually a combo of search+learning that is necessary, learning is just the little brother of search, it compresses novel insights into the model. You can think of training a neural net also as search - the best parameters that would fit the training set.