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

121–130 of 254 posts

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

#121

Post by getnormality »

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…

We're told that formal verification tools like Lean are not used to solve the actual IMO problems, but are they used in training the model to solve the problems?

We know from Google's 2024 IMO work that they have a way to translate natural language proofs to formally verifiable ones. It seems like a natural next step would be to leverage this for RLVR in training/fine-tuning. During training, any piece of reasoning generated by the math LLM could be translated, verified, and assigned an appropriate reward, making the reward signal much denser.

Reward for a fully correct proof of a given IMO problem would still be hard to come by, but you could at least discourage the model from doing wrong or indecipherable things. That plus tons of compute might be enough to solve IMO problems.

In fact it probably would be, right? We already know from AlphaProof that by translating LLM output back and forth between formal Lean proofs, you can search the space of reasoning moves efficiently enough to solve IMO-class problems. Maybe you can cut out the middleman by teaching the LLM via RLVR to mimic formal reasoning, and that gets you roughly the same efficiency and ability to solve hard problems.

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

#122

Post by kevinventullo »

modeless wrote: post #110
kevinventullo wrote: post #91

This year, our advanced Gemini model operated end-to-end in natural language, producing rigorous mathematical proofs directly from the official problem descriptions I think I have a minority opinion here, but I’m a bit disappointed they seem to be moving away from formal techniques. I think if you ever want to truly “automate” math or do it at machine scale, e.g. creating proofs that would amount to thousands of page…

These problems are designed to be solvable by humans without tools. No reason we can't give tools to the models when they go after harder problems. I think it's good to at least reproduce human-level skill without tools first.

Oh so to be clear, I view formal methods as less of a useful tool, and more as enforcing a higher standard of proof. E.g. it’s not clear to me that having access to Lean would actually help a human in the IMO; certainly most professional mathematicians are not yet getting a positive ROI from formalization. But I’m sort of an armchair expert here; I could be wrong!

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

#123

Post by sweezyjeezy »

cubefox wrote: post #97
shiandow wrote: post #59

Comparing the answers between Openai and Gemini the writing style of Gemini is a lot clearer. It could be presented a bit better but it's easy enough to follow the proof. This also makes it a lot shorter than the answer given by OpenAI and it uses proper prose.

I found the proofs you were referring to: Google https://storage.googleapis.com/deepmind-media/gemini/IMO_202... OpenAI https://github.com/aw31/openai-imo-2025-proofs/

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.

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

#124

Post by drexlspivey »

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!

More like Deep Blue vs Child prodigy. In the IMO the contestants are high school students not the greatest mathematicians in the world.

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

#125

Post by sweezyjeezy »

gyrovagueGeist wrote: post #115

Useful and interesting but likely still dangerous in production without connecting to formal verification tools. I know o3 is far from state of the art these days but it's great at finding relevant literature and suggesting inequalities to consider but in actual proofs it can produce convincing looking statements that are false if you follow the details, or even just the algebra, carefully. Subtle errors like these m…

100% o3 has a strong bias towards "write something that looks like a formal argument that appears to answer the question" over writing something sound.

I gave it a bunch of recent, answered MathOverflow questions - graduate level maths queries. Sometimes it would get demonstrably the wrong answer, but it not be easy to see where it had gone wrong (e.g. some mistake in a morass of algebra). A wrong but convincing argument is the last thing you want!

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

#126

Post by 7373737373 »

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…

He created a Youtube channel showcasing working alongside these tools: https://youtube.com/@TerenceTao27

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

#127

Post by modeless »

getnormality wrote: post #121
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…

We're told that formal verification tools like Lean are not used to solve the actual IMO problems, but are they used in training the model to solve the problems? We know from Google's 2024 IMO work that they have a way to translate natural language proofs to formally verifiable ones. It seems like a natural next step would be to leverage this for RLVR in training/fine-tuning. During training, any piece of reasoning g…

It seems very likely from the description in the link that formal verification tools for mathematical proofs were used in part of the RL training for this model. On the other hand, OpenAI claims "We reach this capability level not via narrow, task-specific methodology, but by breaking new ground in general-purpose reinforcement learning and test-time compute scaling." Which might suggest that they don't specifically use e.g. Lean in their training process. But it's not explicitly stated. All we can really do is speculate unless they publish more detail.

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

#129

Post by NitpickLawyer »

SirMaster wrote: post #81
nashashmi wrote: post #54

Earlier quoted context omitted.

There are only so many words in the modern English language to hint at "next upgrade": pro, plus, ultra, new, advanced, magna, X, Z, and Ultimate. Even fewer words to explain miniaturized: mini, lite, and zero. And marketers are trying to seesaw on known words without creating new ones to explain new tech. This is why we have Bard and Gemini and Chat and Copilot. Taking a step back, it is overused exaggeration to the…

Good thing we have a system called numbers that can easily designate an infinite range of greater and greater things.

Heh, you'd still get confusing stuff. Wait, is gemini 2.5.3.1 the math one or the erotica lit one?

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

#130

Post by NitpickLawyer »

pphysch wrote: post #73
ekojs wrote: post #25

> Btw as an aside, we didn’t announce on Friday because we respected the IMO Board's original request that all AI labs share their results only after the official results had been verified by independent experts & the students had rightly received the acclamation they deserved > We've now been given permission to share our results and are pleased to have been part of the inaugural cohort to have our model results off…

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.
Post reply on HN