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

291–300 of 564 posts

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

#291

Post by cubefox »

fmap wrote: post #272
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…

Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them. By contrast, this kind of open ended formalization is something where progress used to be extremely slow and incremental. I worked in an adjacent field 5 years ago and I cannot stress enough that these results ar…

> Agreed, this is a big step forward. Geometry problems are in a different class, since you can translate them into systems of polynomial equations and use well known computer algebra algorithms to solve them.

The blog post indicates the opposite. The geometry problem in the IMO problem set was solved by AlphaGeometry 2, which is an LLM based on Google's Gemini. LLMs are considered relatively general systems. But the other three solved problems were proved by AlphaProof, which is a narrow RL system that is literally based on AlphaZero, the Go and Chess AI. Only its initial (bootstrapping) human training data (proofs) were formalized and augmented by an LLM (Gemini).

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

#292

Post by camjw »

hyperbovine wrote: post #275
camjw wrote: post #234

Earlier quoted context omitted.

Sure but if an AI can prove e.g the Goldbach conjecture then that is a bfd.

What if the proof were incomprehensible to humans?

I think that is unlikely to be the case - the classic example of a proof that human's "can't understand" is the Four Colour Theorem, but thats because the proof is a reduction to like 100000 special cases which are checked by computer.

To what extent is the proof of Fermat's Last Theorem "incomprehensible to humans" because only like a dozen people on the planet could truly understand it - I don't know.

The point of new proofs is really to learn new things about mathematics, and I'm sure we would learn something from a proof of Goldbach's conjecture.

Finally if it's not peer reviewed then its not a real proof eh.

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

#293

Post by camjw »

raincole wrote: post #247
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"?

Because "Generally Intelligent" is a very broad and vague term. "Better than Terrence Tao at solving certain formalized problems" (not necessarily equal to "Better that Terrence Tao at maths) isn't.

Seems fair - I strongly think that "certain formalized problems" is very very far away from doing actual maths! And that actual maths is sometimes much less about solving known conjectures and much more about developing new theories.

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

#294

Post by pishpash »

fngjdflmdflg wrote: post #277
pishpash wrote: post #166

Earlier quoted context omitted.

Yet the facts at hand are the opposite of what you say. Reliable formalizer was the more difficult problem than solving formalized IMO problems, because they have not produced one.

That does not necessarily follow from the facts at hand. For example they may have prioritized work on the proof solver itself as they may feel that that is the more important result. Alternatively if their goal is to build a proof solver then building the formalizer would be useless if they could not build the actual proof solver.

A proof solver existed. They were improving the proof solver explicitly by making the formalizer a part of the training. Formalizer reliability is the key novelty. It turns out it was only reliable enough for training. So unless they made the problem statement at the outset that "we'll only make the formalizer strong enough to train but not use", I disagree with that assessment.

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

#296

Post by hulitu »

> AI solves International Math Olympiad problems at silver medal level

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

Why not compare with students who are given 3 days to submit an answer ? /s

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

#297

Post by gjm11 »

visarga wrote: post #117
gjm11 wrote: post #72

Earlier quoted context omitted.

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…

Euclidian Geometry still requires constructions to solve, and those are based in intuition.

There are known algorithms that can solve _all_ problems in euclidean (ruler-and-compasses) geometry, no intuition required. The most effective algorithms of this type are quite inefficient, though, and (at least according to DeepMind) don't do as well as AlphaGeometry does at e.g. IMO geometry problems.

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

#298

Post by cynicalpeace »

christianqchung wrote: post #254
cynicalpeace wrote: post #232

Machines have been better than humans at chess for decades. Yet no one cares. Everyone's busy watching Magnus Carlsen. We are human. This means we care about what other humans do. We only care about machines insofar as it serves us. This principle is broadly extensible to work and art. Humans will always have a place in these realms as long as humans are around.

> This principle is broadly extensible to work and art Nah, as a consumer it makes no difference to me if a meat packing factory or Amazon warehouse employs 5000 or 5 people. To art, this principle is totally real, but for work, it only applies to some/most of it.

Read the next sentence: "We only care about machines insofar as it serves us."

Imagine a machine doing "work" that only serves itself and other machines that does no service to humanity. It would have no economic value. In fact the whole concept of "work" only makes sense if it is assigned economic value by humans.

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

#300

Post by mupuff1234 »

raincole wrote: post #263
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.

Yeah, I mean "interesting" problems (perhaps not fields medal interesting, but interesting enough)
Post reply on HN