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

141–150 of 564 posts

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

#141

Post by visarga »

kypro wrote: post #127
visarga wrote: post #106

Earlier quoted context omitted.

> a lot of brute force search Don't dismiss search, it might be brute force but it goes beyond human level in Go and silver at IMO. Search is also what powers evolution which created us, also by a lot of brute forcing, and is at the core of scientific method (re)search.

My old AI professor used to say that every problem is a search problem. The issue is that to find solutions for useful problems you're often searching through highly complex and often infinite solution spaces.

For some problems validation is expensive. Like the particle collider or space telescope, or testing the COVID vaccine. It's actually validation that is the bottleneck in search not ideation.

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

#143

Post by Smaug123 »

pclmulqdq wrote: post #123
Smaug123 wrote: post #78

Earlier quoted context omitted.

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

Comparing "turn photo into LaTeX" to "translate theorems into Lean" is like comparing a child's watercolor drawing to the Mona Lisa.

… no? After the LaTeX output, I told stock GPT4o that the answer was "all even integers", and asked for the statement in Lean. I had to make two changes to its output (both of which were compile-time errors, not misformalisations), and it gave me the formalisation of the difficult direction of the problem.

Both changes were trivial: it had one incorrect (but unnecessary) import, and it used the syntax from Lean 3 instead of Lean 4 in one lambda definition. A system that was trained harder on Lean would not make those mistakes.

The one actual error it made was in not proposing that the other direction of the "if and only if" is required. Again, I am quite confident that this formalisation failure mode is not hard to solve in a system that is, like, actually trained to do this.

Obviously formalising problems that a working mathematicican solves is dramatically harder than formalising IMO problems, and is presumably way ahead of the state of the art.

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

#144

Post by dooglius »

pclmulqdq wrote: post #118
dooglius wrote: post #52

Earlier quoted context omitted.

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

So if Lean was used to find the answers, where exactly is the AI? A thin wrapper around Lean?

Lean checks that the proof is valid, it didn't find the proof.

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

#145

Post by thomasahle »

summerlight wrote: post #100
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…

To speak generally, that translation part is much easier than the proof part. The problem with automated translation is that the translation result might be incorrect. This happens a lot when even people try formal methods by their hands, so I guess the researchers concluded that they'll have to audit every single translation regardless of using LLM or whatever tools.

You'd think that, but Timothy Gowers (the famous mathematician they worked with) wrote (https://x.com/wtgowers/status/1816509817382735986)

> However, LLMs are not able to autoformalize reliably, so they got them to autoformalize each problem many times. Some of the formalizations were correct, but even the incorrect ones were useful as training data, as often they were easier problems.

So didn't actually solve autoformalization, which is why they still needed humans to translate the input IMO 2024 problems.

The reason why formalization is harder than you think is that there is no way to know if you got it right. You can use Reinforcement Learning with proofs and have a clear signal from the proof checker. We don't have a way to verify formalizations the same way.

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

#146

Post by xrisk »

pclmulqdq wrote: post #118
dooglius wrote: post #52

Earlier quoted context omitted.

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

So if Lean was used to find the answers, where exactly is the AI? A thin wrapper around Lean?

Lean is just the language, Presumably to drive the AI towards the program (“the proof”)

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

#147

Post by Davidzheng »

ocfnash wrote: post #40
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 computer did find the answers itself. I.e., it found "even integers" for P1, "{1,1}" for P2, and "2" for P6. It then also provided provided a Lean proof in each case.

Can you elaborate on how it makes guesses like this? Does it do experiments before? Is it raw LLM? Is it feedback loop based on partial progress?

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

#148

Post by Davidzheng »

visarga wrote: post #106
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…

> a lot of brute force search Don't dismiss search, it might be brute force but it goes beyond human level in Go and silver at IMO. Search is also what powers evolution which created us, also by a lot of brute forcing, and is at the core of scientific method (re)search.

Yes and there's a lot of search here too. That's a key to the approach

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

#149

Post by criddell »

poincaredisk wrote: post #46
ComplexSystems wrote: post #25

Earlier quoted context omitted.

Or the simultaneous discovery of thousands of cryptographic exploits...

Still waiting for the first one. I'm not holding my breath - just like fuzzing found a lot of vulnerabilities in low-level software, I expect novel automated analysis approaches will yield some vulnerabilities - but that won't be a catastrophic event just like fuzzing wasn't.

It's rumored that the NSA has 600 mathematicians working for them. If they are the ones finding the exploits you will probably never hear about them until they are independently discovered by someone who can publish.

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

#150

Post by Davidzheng »

Smaug123 wrote: post #29
Ericson2314 wrote: post #23

The lede is a bit buried: they're using Lean! This is important for more than Math problems. Making ML models wrestle with proof systems is a good way to avoid bullshit in general. Hopefully more humans write types in Lean and similar systems as a much way of writing prompts.

And while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be constructing Gröbner bases in their head, but `polyrith` is just eight characters away. I saw AlphaProof used `nlinarith`.

Good. I want my AI to use all the advantages it has to reinvent the landscape of mathematics
Post reply on HN