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

511–520 of 564 posts

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

#511

Post by humansareok1 »

EugeneOZ wrote: post #280
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…

No. It's like you are allowed to use search engines to find a solution, nothing more than that.

Through a search space often large enough to be completely intractable with a galaxy wide computer.

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

#512

Post by humansareok1 »

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?

If we can formally verify the proof then it doesn't matter. Often the implications on other problems is substantial just knowing the proof exists.

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

#513

Post by lupire »

smokel wrote: post #268
shkkmo wrote: post #260

Earlier quoted context omitted.

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?

Almost every "number" "in" N doesn't actually exist. In the search for numbers that exist, we will most likely only ever find a finite set of numbers before the Universe or humanity dies.

("Scare quotes")

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

#514

Post by lupire »

sebzim4500 wrote: post #240
gowld wrote: post #206

Earlier quoted context omitted.

What makes solving IMO problems hard is usually the limits of human memory, pattern-matching, and search, not creativity. After all, these are problems that are already solved, and it is expected that many people can solve the problems in about 1 hour's time. That makes it, in principle, similar or even easier than a champsionship-level chess move, which often take more than 1 hour for a professional human (with more…

Ok but if you read the actual solutions they aren't a bizarre mess of brute force. They look like what a human would write if they were trying to come up with a formal proof (albeit it does some steps in a weird order).

The solutions aren't a bizarre mess of brute force. The search for the solutions is.

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

#515

Post by seydor »

We need to up the ante: Getting human-like performance on any task is not impressive in itself, what matters is superhuman, orders of magnitude above. These comparisons with humans in order create impressive sounding titles are disguising the fact that we are still at the stone age of intelligence.

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

#516

Post by nopinsight »

Once Gemini, the LLM, integrates with AlphaProof and AlphaGeometry 2, it might be able to reliably perform logical reasoning. If that's the case, software development might be revolutionized.

"... We'll be bringing all the goodness of AlphaProof and AlphaGeometry 2 to our mainstream #Gemini models very soon. Watch this space!" -- Demis Hassabis, CEO of Google DeepMind. https://x.com/demishassabis/status/1816499055880437909

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

#518

Post by auggierose »

throwaway290 wrote: post #481
auggierose wrote: post #473

Earlier quoted context omitted.

Of course. That falls under "understanding why the proof is a proof".

Now we only need to find that human that never makes mistakes and we're golden...

Luckily, that is not necessary. You can make many mistakes, until you arrive at a logic you are happy with. Then you talk with other humans about it, and eventually you will all agree, that to the best of your knowledge, there is no mistake in the logic. If you pick first-order logic, that has already been done for you.

Then you need to implement that logic in software, and again, you can and will mistakes here. You will use the first version of that software, or another logic software, to verify that your informal thoughts why your logic implementation is correct, can be formalised and checked. You will find mistakes, and fix them, and check that your correctness proof still goes through. It is very unlikely that it won't, but if it doesn't, you fix your correctness proof. If you can indeed fix it, you are done, no mistakes remain. If you cannot, something must be wrong with your implementation, so rinse and repeat.

At the end of this, you have a logic, and a logic implementation, which doesn't contain any mistakes. Guaranteed.

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

#520

Post by sdenton4 »

_heimdall wrote: post #504
Thorrez wrote: post #428

Earlier quoted context omitted.

This quote from the article sounds like it learns from failed tests: >We trained AlphaProof for the IMO by proving or disproving millions of problems, covering a wide range of difficulties and mathematical topic areas over a period of weeks leading up to the competition. The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution…

Reading between the lines a bit, that does answer the question I had though don't think I I clarified very well. I read that to say the model's token weights are adjusted as it goes, so in an LLM sense it is kind of learning. It isn't reasoning through an answer in the way a human does though. Meaning, the model is still just statistically predicting what an answer may be and checking if it worked. I wouldn't chalk t…

Computers are good at arithmetic, not math...

There's definitely an aspect of this that is 'airplanes, not birds.' Just because the wings don't flap doesn't mean it can't fly, though.

Post reply on HN