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

221–230 of 564 posts

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

#221

Post by queuebert »

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.

That's amazing. I was just about to comment that hooking this up to Lean [1] would be killer. This must be the way forward for higher math, as proofs are getting so complicated that almost no one understands all pieces of major proofs.

1. https://lean-lang.org/

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

#222

Post by riku_iki »

golol wrote: post #112
riku_iki wrote: post #108

Earlier quoted context omitted.

> They are building a general pipeline which turns informal natural lamguage mathematics but this part currently sucks, because they didn't trust it and formalized problems manually.

Yea that's fair, but I don't think it will keep sucking forever as formalization is in principle just a translation process.

and we don't have 100% accuracy in translation in ambiguous texts, because system often need some domain knowledge, context etc. And math has 0% tolerance to mistakes.

I also expect that math formalized by machine will be readable by machine and hardly understandable by humans.

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

#223

Post by creer »

cs702 wrote: post #177

In 1997, machines defeated a World Chess Champion for the first time, using brute-force "dumb search." Critics noted that while "dumb search" worked for chess, it might not necessarily be a general strategy applicable to other cognitive tasks.[a] In 2016, machines defeated a World Go Champion for the first time, using a clever form of "dumb search" that leverages compute, DNNs, reinforcement learning (RL), and self-p…

If one of the lessons of LLMs was that much of "common sense" is covered in the written language corpus - that is, perhaps, basic human intelligence is covered by language.

Then, should we expect less with mathematics where written language is the normal way knowledge is propagated, and where formal proofs are wanted? An important distinction here is the coupling of search (not LLM for this one), a formal math language, and theorem proving. Math intelligence may not be merely the math written corpus, but adding the formal language and theorem proving sounds pretty powerful.

All this still lacks self-directed goals. An intention. For now that's taken care of by the human asking questions.

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

#224

Post by gowld »

This shows a major gap in AI.

The proofs of these problems aren't interesting. They were already known before the AI started work.

What's interesting is how the AI found the proof. The only answer we have is "slurped data into a neural network, matched patterns, and did some brute search".

What were the ideas it brainstormed? What were the dead-end paths? What were the "activations" where the problem seemed similar to a certain piece of input, which led to a guess of a step in the solution?

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

#225

Post by cs702 »

tux3 wrote: post #217
cs702 wrote: post #213

Earlier quoted context omitted.

That's in fact precisely my point: Clever forms of "dumb search" that leverage compute, DNNs, RL, self-play, and/or formal languages are not dumb at all. I put the words "dumb search" in quotes precisely because I think critics who dismiss AI progress as such are missing the point. We're not in disagreement :-)

>Clever forms of "dumb search" that leverage compute, DNNs, RL, self-play, and formal languages are not dumb at all Right. My point is that you're attacking a position that no real critic holds. Of course we're in agreement then! "Clever forms of dumb search are not dumb" feels a little like kicking down open doors. We were always going to agree.

> My point is that you're attacking a position that no real critic holds

I'm not so sure. I wrote my comment after seeing quite a few comments on other threads here that read like fancy versions of "this is just brute-force search over cleverly pruned trees." Search the other threads here, and you'll see what I mean.

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

#227

Post by oXman038 »

quirino wrote: post #80

I honestly expected the IOI (International Olympiad of Informatics) to be "beaten" much earlier than the IMO. There's AlphaCode, of course, but on the latest update I don't think it was quite on "silver medal" level. And available LLM's are probably not even on "honourable mention" level. I wonder if some class of problems will emerge that human competitors are able to solve but are particularly tricky for machines.…

IOI problems are more close to IMO combinatoric problems than other IMO problem types. That might be the reason for that delay. I personally like only combinatoric problems in IMO. Thats why I drop math track and went IOI instead.

I feel why combinatoric is harder for AI models is the same reason why LLM's are not great at reasoning anything out of distribution. LLM's are good pattern recognizers and fascinating at this point. But simple tasks like counting intersections at the Venn diagrams requires more strategy and less pattern recognition. Pure NN based models seem won't be enough to solve these problems. AI agents and RL are promising.

I don't know anything about lean but I am curious that proof of combinatorial problems can be as well represented as number theory or algebra. If combinatorial problem solutions are always closer to natural language, the failure of LLMs are expected. Or, at least we can assume it might take more time to make it better. I am making assumption in here that solutions of combinatorial problems in IMO are more human language oriented and relies on more common sense/informal logic when it compared to geometry or number theory problems.

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

#228

Post by [deleted] »

cs702 wrote: post #177

In 1997, machines defeated a World Chess Champion for the first time, using brute-force "dumb search." Critics noted that while "dumb search" worked for chess, it might not necessarily be a general strategy applicable to other cognitive tasks.[a] In 2016, machines defeated a World Go Champion for the first time, using a clever form of "dumb search" that leverages compute, DNNs, reinforcement learning (RL), and self-p…

[deleted]

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

#229

Post by Xelynega »

Smaug123 wrote: post #81
nnarek wrote: post #53

Earlier quoted context omitted.

formal definition of first theorem already contain answer of the problem "{α : ℝ | ∃ k : ℤ, Even k ∧ α = k}" (which mean set of even real numbers).if they say that they have translated first problem into formal definition then it is very interesting how they initially formalized problem without including answer in it

(You're talking to one of the people who was part of the project, which is why I took @ocfnash's answer as authoritative: they did not cheat.)

If they're talking to the people who are part of the project I'd hope the answer would contain detail and not expect to be taken as authoritative.

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

#230

Post by thrance »

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 with the human element of figuring out the author's own notations, implicit knowledge, skipped proof steps...

Post reply on HN