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

Gemini with Deep Think achieves gold-medal standard at the IMO

deepmind.google

Post reply on HN
Print view View original

151–160 of 254 posts

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#151

Post by daxfohl »

modeless wrote: post #45

> AlphaGeometry and AlphaProof required experts to first translate problems from natural language into domain-specific languages, such as Lean, and vice-versa for the proofs. It also took two to three days of computation. This year, our advanced Gemini model operated end-to-end in natural language, producing rigorous mathematical proofs directly from the official problem descriptions So, the problem wasn't translated…

I'd also be curious as to why not use Lean. Is it that Lean use at this point makes the problems too easy to brute force? Or is it that Lean at this point just gets in the way of things?

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#152

Post by alephnerd »

sanjitb wrote: post #146

Why do they brag about not using a theorem prover? To me, whatever tool helps the model perform, go for it. Besides, they still specialized Gemini for the IMO in other ways: > we additionally trained this version of Gemini on novel reinforcement learning techniques that can leverage more multi-step reasoning, problem-solving and theorem-proving data. We also provided Gemini with access to a curated corpus of high-qua…

> Why do they brag about not using a theorem prover

Because this highlights that Gemini actually reasoned independently of other tools. That is a massive quantum leap in AI/ML. Abstract reasoning is arguably the basis of cognition.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#153

Post by sweezyjeezy »

shiandow wrote: post #131
sweezyjeezy wrote: post #123

Earlier quoted context omitted.

Gemini is clearer but MY GOD is it verbose. e.g. look at problem 1, section 2. Analysis of the Core Problem - there's nothing at all deep here, but it seems the model wants to spell out every single tiny logical step. I wonder if this is a stylistic choice or something that actually helps the model get to the end.

Section 2 is a case by case analysis. Those are never pretty but perfectly normal given the problem. With OpenAI that part takes up about 2/3 if the proof even with its fragmented prose. I don't think it does much better.

It's not it being case by case that's my issue. I used do olympiads and e.g. for the k>=3 case I wouldn't write much more than:

"Since there are 3k - 3 points on the perimeter of the triangle to be covered, and any sunny line can pass through at most two of them, it follows that 3k − 3 ≤ 2k, i.e. k ≤ 3."

Gemini writes:

Let Tk be the convex hull of Pk. Tk is the triangle with vertices V1 = (1, 1), V2 = (1, k), V3 = (k, 1). The edges of Tk lie on the lines x = 1 (V), y = 1 (H), and x + y = k + 1 (D). These lines are shady.

Let Bk be the set of points in Pk lying on the boundary of Tk. Each edge contains k points. Since the vertices are distinct (as k ≥ 2), the total number of points on the boundary is |Bk| = 3k − 3.

Suppose Pk is covered by k sunny lines Lk. These lines must cover Bk. Let L ∈ Lk. Since L is sunny, it does not coincide with the lines containing the edges of Tk. A line that does not contain an edge of a convex polygon intersects the boundary of the polygon at most at two points. Thus, |L ∩ Bk| ≤ 2. The total coverage of Bk by Lk is at most 2k. We must have |Bk| ≤ 2k. 3k − 3 ≤ 2k, which implies k ≤ 3.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#154

Post by wbhart »

daxfohl wrote: post #151
modeless wrote: post #45

> AlphaGeometry and AlphaProof required experts to first translate problems from natural language into domain-specific languages, such as Lean, and vice-versa for the proofs. It also took two to three days of computation. This year, our advanced Gemini model operated end-to-end in natural language, producing rigorous mathematical proofs directly from the official problem descriptions So, the problem wasn't translated…

I'd also be curious as to why not use Lean. Is it that Lean use at this point makes the problems too easy to brute force? Or is it that Lean at this point just gets in the way of things?

Lean is an interactive prover, not an automated prover. Last year a lot of human effort was required to formalise the problems in Lean before the machines could get to work. This year you get natural language input and output, and much faster.

The advantage of Lean is that the system checks the solutions, so hallucination is impossible. Of course, one still relies on the problems and solutions being translated to natural language correctly.

Some people prefer difficult to read formally checked solutions over informal but readable solutions. The two approaches are just solving different problems.

But there is another important reason to want to do this reliably in natural language: you can't use Lean for other domains (with a few limited exceptions). They want to train their RL pipelines for general intelligence and make them reliable for long horizon problems. If a tool is needed as a crutch, then it more or less demonstrates that LLMs will not be enough in any domain, and we'll have to wait for traditional AI to catch up for every domain.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#155

Post by ars »

NitpickLawyer wrote: post #35
tornikeo wrote: post #31

I think we are having a Deep Blue vs. Kasparov moment in Competitive Math right now. This is a large progress from just a few years ago and yet I think we still are really far away from even a semi-respectable AI mathematician. What an exciting time to be alive!

Terrence Tao, in a recent podcast, said that he's very interested in "working along side these tools". He sees the best use in the near future as "explorers of human set vision" in a way. (i.e. set some ideas/parameters and let the LLMs explore and do parallel search / proof / etc) Your comparison with chess engines is pretty spot-on, that's how the best of the best chess players do prep nowadays. Gone are the multi…

Similar to https://en.wikipedia.org/wiki/Advanced_chess

The Wikipedia doesn't have much info on the results, but from other reading I got the impression that the combination produced results stronger than any individual human or computer player.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#156

Post by danie123 »

neom wrote: post #112

How much of a big deal is this stuff? I was blessed with dyscalculia so I can hardly add two numbers together, don't pay much attention to the mathematics word, but my reading indicates this is extremely difficult/humans cannot do this? What comes next for this particular exercise? Thank you.

Humans certainly can get gold at IMO: the threshold is chosen each year such that around 8% of students get it. So about 50 students (worldwide) per year are awarded it. Also note that the competition is only for students who are still in school.

Getting a gold is considered very impressive, but there are certainly plenty of humans in the world who can solve problems at that level, and even more so if you relax the time constraints of it being a competition environment. If you include people who are too old to be eligible for IMO, then there are maybe around 1,000-100,000 people in the world who could get a gold at IMO (the large range is because I think this quantity is quite hard to estimate).

Another important thing to bear in mind is that research mathematics is quite different to competition mathematics, so it is quite tricky to tell how good these AIs will be at research maths.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#157

Post by simonw »

jonahx wrote: post #137
simonw wrote: post #87

Earlier quoted context omitted.

I interpreted that bit as meaning they did not manually alter the problem statement before feeding it to the model - they gave it the exact problem text issued by IMO. It is not clear to me from that paragraph if the model was allowed to call tools on its own or not.

As a side question, do you think using tools like Lean will become a staple of these "deep reasoning" LLM flavors? It seems that LLMs excel (relative to other paradigms) in the kind of "loose" creative thinking humans do, but are also prone to the same kinds of mistakes humans make (hallucinations, etc). Just as Lean and other formal systems can help humans find subtle errors in their own thinking, they could do the…

I was surprised to see them not using tools for it, that feels like a more reliable way to get useful results for this kind of thing.

I get the impression not using tools is as part of the point though - to help demonstrate how much mathematical "reasoning" you can get out of just a model on its own.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#158

Post by npinsker »

NitpickLawyer wrote: post #130
pphysch wrote: post #73

Earlier quoted context omitted.

This reminds me of when OpenAI made a splash (ages ago now) by beating the world's best Dota 2 teams using a RL model. ...Except they had to substantially bend the rules of the game (limiting the hero pool, completely changing/omitting certain mechanics) to pull this off. So they ended up beating some human Dota pros at a psuedo-Dota custom game, which was still impressive, but a very much watered-down result beneath…

Limiting the hero pool was fair I'd say. If you can prove RL works on one hero, it's fairly certain it would work on other heroes. All of them at once? Maybe run into problems. But anyway you'd need orders of magnitude more compute so I'd say that was fair game.

It's not even close to the same game as Dota. Limiting the hero (and item) pool so drastically locks off many strategies and counters. It's a bit hard to explain if you haven't played, but full Dota has many more tools and much more creativity than the reduced version on display. The behavior does not evidently "scale up", in the same way that the current SotA of AI art and writing won't evidently replace top-level humans.

I'd never say it's impossible, but the job wasn't finished yet.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#159

Post by asdfologist »

ted_dunning wrote: post #147
vouaobrasil wrote: post #128

This is making mathematics too systematic and mechanical, and it kills the joy of it....

It didn't kill chess

It did partially, which is why top players are nowadays playing Freestyle (chess 960) more and more.

Re: Gemini with Deep Think achieves gold-medal standard at the IMO

#160

Post by erichocean »

square_usual wrote: post #86
erichocean wrote: post #57

Earlier quoted context omitted.

I regularly have the opposite experience: o3 is almost unusable, and Gemini 2.5 Pro is reliably great. Claude Opus 4 is a close second. o3 is so bad it makes me wonder if I'm being served a different model? My o3 responses are so truncated and simplified as to be useless. Maybe my problems aren't a good fit, but whatever it is: o3 output isn't useful.

Are you using o3 on the official ChatGPT app or via API? I use it on the app and it performs very well, it's my go-to model for general purpose LLM use.

official ChatGPT app
Post reply on HN