3 ms·

This is a fun result for AI, but a very disingenuous way to market it. IMO contestants aren't allowed to bring in paper tables, much less a whole theorem prove

This is a fun result for AI, but a very disingenuous way to market it. IMO contestants aren't allowed to bring in paper tables, much less a whole theorem prover. They're given two 4.5 hour sessions (9 hours total) to solve all the problems with nothing but pencils, rulers, and compasses [0]. This model, meanwhile, was wired up to a theorem proover and took three solid days to solve the problems. The article is extremely light on details, but I'm assuming that most of that time was guess-and-check: feed the theorem prover a possible answer, get feedback, adjust accordingly. If the IMO contestants were given a theorem prover and three days (even counting breaks for sleeping and eating!), how would AlphaProof have ranked? Don't get me wrong, this is a fun project and an exciting result, but their comparison to silver medalists at the IMO is just feeding into the excessive hype around AI, not accurately representing its current state relative to humanity. [0] 5.1 and 5.4 in the regulations: https://www.imo-official.org/documents/RegulationsIMO.pdf https://www.imo-official.org/documents/RegulationsIMO.pdf

gjm11 2y ago
Working mathematicians mostly don't use theorem provers in their work, and find that when they do they go significantly more slowly (with of course the compensating advantage of guaranteeing no mistakes in the final result). A theorem prover is probably more useful for the typical IMO problem than for the typical real research problem, but even so I'd guess that even with a reasonable amount of training most IMO contestants would not do much better for having access to a theorem prover. Having three days would be a bigger deal, for sure. (But from "computers can't do this" to "computers can do this, but it takes days" is generally a much bigger step than from "computers can do this, but it takes days" to "computers can do this in seconds".)
golol 2y ago
The point is not to compare AI and humans, it is to compare AI and IMO-level math problems. It's not for sport.
- lolinder 2y ago
  They're literally comparing AI to human IMO contestants. "DeepProof solves 4/6 IMO problems correctly" would be the non-comparison version of this press release and would give a better sense for how it's actually doing.
  - golol 2y ago
    "Solving IMO problems at Silver-Medal level" is pretty much equivalent to solving something like 4/6 problems. It is only a disingenious comparison if you want to read it as a comparison. I mean yea, many people will, but I don't care anout them. People who are technically interested in this know that the point is not to have a competition of AI with humans.
    - lolinder 2y ago
      > but I don't care anout them It's great that you feel safe being so aloof, but I believe we have a responsibility in tech to turn down the AI hype valve. The NYT is currently running a piece with the headline "Move Over, Mathematicians, Here Comes AlphaProof". People see that, and people react, and we in tech are not helping matters by carelessly making false comparisons.
      - golol 2y ago
        Why? Why is hype bad? What actual harm does it cause? Also the headline is fair, as I do believe that AlphaProof demonstrates an approach to mathematics that will indeed invade mathematicians workspaces. And I say that as a mathemstician.
        Davidzheng 2y ago
        For sure. I feel like mathematicians are not paying attention (maybe deliberately) we have a real shot of solving some incredibly hard open problem in the next few years.
      - visarga 2y ago
        I think search-based AI is on a different level than imitation models like GPT. This is not a hallucinating model, and it could potentially discover things that are not written in any books. Search is amazing. Protein folding searches for the lowest energy configuration. Evolution searches for ecological fit. Culture searches for progress, and science for understanding. Even placing a foot on the ground searches for dynamic equilibrium. Training a ML model searches for best parateters to fit a dataset. Search is universal. Supervised learning is just imitative, search is extrapolative.
- kenjackson 2y ago
  Exactly. The point is what can we eventually get AI to solve problems which we as humans can’t. Not if we can win the IMO with a computer.
blackbear_ 2y ago
And why aren't you complaining that human participants could train and study for thousands of hours before attempting the problems? And that the training materials they used was itself created and perfected by hundreds of other people, after having themselves spend countless hours studying?
- lolinder 2y ago
  Because so did the AI?
  - blackbear_ 2y ago
    That's exactly my point? Both had to learn?
Davidzheng 2y ago
I can tell you that as someone who could have gotten bronze (i was too weak for the team) and is now a math phd--I would not have scored as well as alphaproof in three days most likely. In most problems either you find an idea soon or it can be much much longer. It's just not a matter of working and constant progress.
- knotthebest 2y ago
  Skill issue tbh
  - Davidzheng 2y ago
    Agreed :'(
- utopcell 2y ago
  Noting the difference in humility between someone that has made the cut to participate in the IMO (6 people per country) and the multitude of retrospect prophets that trivialize the DeepMind achievement.
deleted 2y ago
[deleted]

gjm11 2y ago

Working mathematicians mostly don't use theorem provers in their work, and find that when they do they go significantly more slowly (with of course the compensating advantage of guaranteeing no mistakes in the final result). A theorem prover is probably more useful for the typical IMO problem than for the typical real research problem, but even so I'd guess that even with a reasonable amount of training most IMO contestants would not do much better for having access to a theorem prover. Having three days would be a bigger deal, for sure. (But from "computers can't do this" to "computers can do this, but it takes days" is generally a much bigger step than from "computers can do this, but it takes days" to "computers can do this in seconds".)

golol 2y ago

The point is not to compare AI and humans, it is to compare AI and IMO-level math problems. It's not for sport.

lolinder 2y ago
They're literally comparing AI to human IMO contestants. "DeepProof solves 4/6 IMO problems correctly" would be the non-comparison version of this press release and would give a better sense for how it's actually doing.
- golol 2y ago
  "Solving IMO problems at Silver-Medal level" is pretty much equivalent to solving something like 4/6 problems. It is only a disingenious comparison if you want to read it as a comparison. I mean yea, many people will, but I don't care anout them. People who are technically interested in this know that the point is not to have a competition of AI with humans.
  - lolinder 2y ago
    > but I don't care anout them It's great that you feel safe being so aloof, but I believe we have a responsibility in tech to turn down the AI hype valve. The NYT is currently running a piece with the headline "Move Over, Mathematicians, Here Comes AlphaProof". People see that, and people react, and we in tech are not helping matters by carelessly making false comparisons.
    - golol 2y ago
      Why? Why is hype bad? What actual harm does it cause? Also the headline is fair, as I do believe that AlphaProof demonstrates an approach to mathematics that will indeed invade mathematicians workspaces. And I say that as a mathemstician.
      - Davidzheng 2y ago
        For sure. I feel like mathematicians are not paying attention (maybe deliberately) we have a real shot of solving some incredibly hard open problem in the next few years.
    - visarga 2y ago
      I think search-based AI is on a different level than imitation models like GPT. This is not a hallucinating model, and it could potentially discover things that are not written in any books. Search is amazing. Protein folding searches for the lowest energy configuration. Evolution searches for ecological fit. Culture searches for progress, and science for understanding. Even placing a foot on the ground searches for dynamic equilibrium. Training a ML model searches for best parateters to fit a dataset. Search is universal. Supervised learning is just imitative, search is extrapolative.
kenjackson 2y ago
Exactly. The point is what can we eventually get AI to solve problems which we as humans can’t. Not if we can win the IMO with a computer.

blackbear_ 2y ago

And why aren't you complaining that human participants could train and study for thousands of hours before attempting the problems? And that the training materials they used was itself created and perfected by hundreds of other people, after having themselves spend countless hours studying?

lolinder 2y ago
Because so did the AI?
- blackbear_ 2y ago
  That's exactly my point? Both had to learn?

Davidzheng 2y ago

I can tell you that as someone who could have gotten bronze (i was too weak for the team) and is now a math phd--I would not have scored as well as alphaproof in three days most likely. In most problems either you find an idea soon or it can be much much longer. It's just not a matter of working and constant progress.

knotthebest 2y ago
Skill issue tbh
- Davidzheng 2y ago
  Agreed :'(
utopcell 2y ago
Noting the difference in humility between someone that has made the cut to participate in the IMO (6 people per country) and the multitude of retrospect prophets that trivialize the DeepMind achievement.

deleted 2y ago

[deleted]