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

261–270 of 564 posts

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

#261

Post by Davidzheng »

thrance wrote: post #230

Theorem proving is a single-player game with an insanely big search space, I always thouht it would be solved long before AGI. IMHO, the largest contributors to AlphaProof were the people behind Lean and Mathlib, who took the daunting task of formalizing the entirety of mathematics to themselves. This lack of formalizing in math papers was what killed any attempt at automation, because AI researcher had to wrestle wi…

They didn't formalize the entirety of math. Good thing imo doesn't need the entirety. But they didn't even formalize enough for imo--this is probably why combo wasn't solved

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

#262

Post by Davidzheng »

thrance wrote: post #241
camjw wrote: post #235

Earlier quoted context omitted.

> Theorem proving is a single-player game with an insanely big search space, I always thouht it would be solved long before AGI. This seems so weird to me - AGI is undefined as a term imo but why would you expect "producing something generally intelligent" (i.e. median human level intelligence) to be significantly harder than "this thing is better than Terrence Tao at maths"?

My intuition tells me we humans are generally very bad at math. Proving a theorem, in an ideal way, mostly involves going from point A to point B in the space of all proofs, using previous results as stepping stones. This isn't particularly a "hard" problem for computers which are able to navigate search spaces for various games much more efficiently than us (chess, go...). On the other hand, navigating the real worl…

I also think humans are bad at math. And that we are probably better at IRL but maybe IRL has more data anyway

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

#263

Post by raincole »

mupuff1234 wrote: post #22

Can it / did it solve problems that weren't solved yet?

Techinically yes. And it's easy. You can probably do it with your PC's computational power.

The thing is that most math "problems" are not solved not becasue they're hard, but because they're not interesting enough to even be discovered by humans.

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

#264

Post by klysm »

dan_mctree wrote: post #251

I'm curious if we'll see a world where computers could solve math problems so easily, that we'll be overwhelmed by all the results and stop caring. The role of humans might change to asking the computer interesting questions that we care about.

I'm not sure what stop caring really means - like stop caring about the result, or the implications?

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

#265

Post by summerlight »

thrdbndndn wrote: post #180
thomasahle wrote: post #145

Earlier quoted context omitted.

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

> 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. A small detail wasn't clear to me: for these incorrectly formalized problems, how do they get the correct answer as ground truth for training? Have a human to manually so…

> A small detail wasn't clear to me: for these incorrectly formalized problems, how do they get the correct answer as ground truth for training? Have a human to manually solve them?

Formal proofs can be mechanically checked if it's correct or not. We just don't know what's the answer. Think it as an extremely rigorous type system that typically requires really long type annotations, like annotation itself is a complex program. So if AlphaProof happens to generate a proof that passes this checker, we know that it's correct.

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

#266

Post by im3w1l »

10100110 wrote: post #83
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…

Don't confuse interpolation with extrapolation. Curing cancer will require new ideas. IMO requires skill proficiency in tasks where the methods of solving are known.

I think this is kinda false actually on the cancer side. We have reached a point where we have known approaches that work. It's "just" a matter of putting them into practice which will of course require solving many little details, which is very important and time-consuming work, but it doesn't require super-human genius level of lateral thinking, just a few millions man years of grinding away at it.

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

#267

Post by thrance »

tim-kt wrote: post #252
thrance wrote: post #241

Earlier quoted context omitted.

My intuition tells me we humans are generally very bad at math. Proving a theorem, in an ideal way, mostly involves going from point A to point B in the space of all proofs, using previous results as stepping stones. This isn't particularly a "hard" problem for computers which are able to navigate search spaces for various games much more efficiently than us (chess, go...). On the other hand, navigating the real worl…

I don't think that computers have an advantage because they can navigate search spaces efficiently. The search space for difficult theorems is gigantic. Proving them often relies on a combination of experience with rigorous mathematics and very good intuition [1] as well as many, many steps. One example is the classification of all finite simple groups [2], which took about 200 years and a lot of small steps. I guess…

Oh for sure, when I say "soon" it's only relative to AGI.

What I meant to convey, is that theorem proving at least is a well-defined problem, and computers have had some successes in similar-ish search problems before.

Also I don't think pure brute-force was ever used to solve any kind of interesting problem.

Chess engines make use of alpha-beta pruning plus some empirical heuristics people came up with over the years. Go engines use Monte-Carlo Tree Search with straight deep learning models node evaluation. Theorem proving, when it is solved, will certainly use some kind of neural network.

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

#268

Post by smokel »

shkkmo wrote: post #260
kypro wrote: post #127

Earlier quoted context omitted.

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.

I would argue that no actually searchable solution space is really infinite (if only because infinite turing machines can't exist). Finite solution spaces can get more than large enough to be intractable.

What about ℕ? Seems pretty infinite to me, unless with "actually" you mean finite in time and space, which would make your argument a tautology. Or am I missing something?

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

#270

Post by Davidzheng »

nybsjytm wrote: post #218

To what extent is the training and structure of AlphaProof tailored specifically to IMO-type problems, which typically have short solutions using combinations of a small handful of specific techniques? (It's not my main point, but it's always worth remembering - even aside from any AI context - that many top mathematicians can't do IMO-type problems, and many top IMO medalists turn out to be unable to solve actual pr…

The last statement is largely correct (though idk what the imo medalists that are unable to solve actual problems most mathematicians can't solve most open problems). But i kind of disagree with the assessment of imo problems--the search space is huge if it were as you say it would be easy to search.
Post reply on HN