AI solves International Math Olympiad problems at silver medal level

Post by golol » Thu, Jul 25, 2024, 5:01 PM UTC

lolinder wrote: post #95

golol wrote: post #73

Earlier quoted context omitted.

I believe you are misreading this. First of all, this is not a sport and the point is not to compare AI to humans. The point is to compare AI to IMO-difficulty problems. Secondly, this is now some hacky trick where Brute force and some theorem prover magic are massaged to solve a select few problems and then you'll never hear about it again. They are building a general pipeline which turns informal natural lamguage m…

> First of all, this is not a sport and the point is not to compare AI to humans. The point is to compare AI to IMO-difficulty problems. If this were the case then the headline would be "AI solves 4/6 IMO 2024 problems", it wouldn't be claiming "silver-medal standard". Medals are generally awarded by comparison to other contestants, not to the challenges overcome. > This can become a real mathematical assistant that…

Post by golol » Thu, Jul 25, 2024, 5:02 PM UTC

lolinder wrote: post #101

golol wrote: post #92

Earlier quoted context omitted.

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

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

Post by visarga » Thu, Jul 25, 2024, 5:03 PM UTC

golol wrote: post #33

This is the real deal. AlphaGeometry solved a very limited set of problems with a lot of brute force search. This is a much broader method that I believe will have a great impact on the way we do mathematics. They are really implementing a self-feeding pipeling from natural language mathematics to formalized mathematics where they can train both formalization and proving. In principle this pipeline can also learn bas…

Post by riku_iki » Thu, Jul 25, 2024, 5:04 PM UTC

golol wrote: post #73

lolinder wrote: post #57

Earlier quoted context omitted.

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 theor…

I believe you are misreading this. First of all, this is not a sport and the point is not to compare AI to humans. The point is to compare AI to IMO-difficulty problems. Secondly, this is now some hacky trick where Brute force and some theorem prover magic are massaged to solve a select few problems and then you'll never hear about it again. They are building a general pipeline which turns informal natural lamguage m…

Post by riku_iki » Thu, Jul 25, 2024, 5:06 PM UTC

golol wrote: post #42

petters wrote: post #6

The problems were first converted into a formal language. So they were partly solved by the AI

Formalization is in principle just a translation process and should be a much simpler problem than the actual IMO problem. Besides, they also trained a Gemini model which formalizes natural language problems, and this is how they generated training data for AlphaProof. I would therefore expect that they could have also formalized the IMO problems with that model and just did it manually because the point is not to de…