Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

AI solves International Math Olympiad problems at silver medal level

deepmind.google

Post reply on HN
Print view View original

71–80 of 564 posts

Re: AI solves International Math Olympiad problems at silver medal level

#71

Post by lolinder »

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

Re: AI solves International Math Olympiad problems at silver medal level

#72

Post by gjm11 »

wongarsu wrote: post #49
adverbly wrote: post #2

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

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…

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.

Re: AI solves International Math Olympiad problems at silver medal level

#73

Post by golol »

lolinder wrote: post #57
adverbly wrote: post #2

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

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 mathematics (of which we have ungodly amounts available) into formalized mathematics, and in addition trains a model to prove such kinds of mathematics. This can also work for theory building. This can become a real mathematical assistant that can help a mathematician test an argument, play with variations of a definition, try 100 combinations of some estimates, apply a classic but lengthy technique etc. etc.

Re: AI solves International Math Olympiad problems at silver medal level

#74

Post by diffeomorphism »

almostgotcaught wrote: post #24
piombisallow wrote: post #5

IMO problems aren't fundamentally different from chess or other games, in that the answer is already known.

> in that the answer is already known. you realize this holds true for all of math right? outside of godel incompleteness potholes every proof/theorem is a permutation of ZFC. And you can fix the potholes by just filling them in with more Cs.

That seems shallow and not really useful. Like sorting is easy, just take all permutations and look at each one to see whether is sorted.... it just might you take longer than the heat death of the universe to actually do that.

Re: AI solves International Math Olympiad problems at silver medal level

#75

Post by tsoj »

ZenMikey wrote: post #8
adverbly wrote: post #2

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

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?

This is NOT the paper, but probably a very similar solution: https://arxiv.org/abs/2009.03393

Re: AI solves International Math Olympiad problems at silver medal level

#76

Post by gjm11 »

lolinder wrote: post #71

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

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

Re: AI solves International Math Olympiad problems at silver medal level

#77

Post by Smaug123 »

diffeomorphism wrote: post #63
Smaug123 wrote: post #9

Earlier quoted context omitted.

I really don't understand what you mean by this. 1) it's not known whether chess is a win for White or not. 2) IMO problems, such as 2024 problem 1 which the system solved, are often phrased as "Determine all X such that…".

You are attacking a straw man and the point made is pretty good. Competition problems are designed to be actually solvable by contestants. In particular, the problems should be solvable using a reasonable collection of techniques and many "prep courses" will teach you many techniques, tools and algorithms and a good starting point is to throw that stuff at any given problem. So just like chess openings putting in lot…

I'm attacking nobody! I literally couldn't understand the point, so I said so: as stated, its premises are simply clearly false!

Your point, however, is certainly a good one: IMO problems are an extremely narrow subset of the space of mathematical problems, which is itself not necessarily even 50% of the space of the work of a mathematician.

Re: AI solves International Math Olympiad problems at silver medal level

#78

Post by Smaug123 »

dooglius wrote: post #52
Smaug123 wrote: post #35

So I am extremely hyped about this, but it's not clear to me how much heavy lifting this sentence is doing: > First, the problems were manually translated into formal mathematical language for our systems to understand. The non-geometry problems which were solved were all of the form "Determine all X such that…", and the resulting theorem statements are all of the form "We show that the set of all X is {foo}". The do…

The linked page says > While the problem statements were formalized into Lean by hand, the answers within the problem statements were generated and formalized by the agent. However, it's unclear what initial format was given to the agents that allowed this step

FWIW, GPT-4o transcribed a screenshot of problem 1 perfectly into LaTeX, so I don't think "munge the problem into machine-readable form" is per se a difficult part of it these days even if they did somehow take shortcuts (which it sounds like they didn't).

Re: AI solves International Math Olympiad problems at silver medal level

#80

Post by quirino »

I honestly expected the IOI (International Olympiad of Informatics) to be "beaten" much earlier than the IMO. There's AlphaCode, of course, but on the latest update I don't think it was quite on "silver medal" level. And available LLM's are probably not even on "honourable mention" level.

I wonder if some class of problems will emerge that human competitors are able to solve but are particularly tricky for machines. And which characteristics these problems will have (e.g. they'll require some sort of intuition or visualization that is not easily formalized).

Given how much of a dent LLM's are already making on beginner competitions (AtCoder recently banned using them on ABC rounds [1]), I can't help but think that soon these competitions will be very different.

[1] https://info.atcoder.jp/entry/llm-abc-rules-en

Post reply on HN