Remember when people thought computers would never be able to beat a human Grand Master at chess? Ohhh, pre-2000 life, how I miss thee.
not to be pedantic, but Deep Blue beat Kasparov in 1997.
AI solves International Math Olympiad problems at silver medal level
381–390 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#382Earlier 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
I would expect that in their data which they train AlphaProof on they have some concept of a "vague problem" whoch could just look like {Formal description of the set in question} = ? And then Alphaproof has to find candidate descriptions of this set and prove a theorem that they are equal to the above. I doubt they would claim to solve the problem if they provided half of the answer.
> I doubt they would claim to solve the problem if they provided half of the answer.
This falls under extraordinary claims require extraordinary proof and we have seen nothing of the sort.
Re: AI solves International Math Olympiad problems at silver medal level
#383This is a fun result for AI, but a very disingenuous way to market it. IMO contestants aren't allowed to bring in paper tables, much less a whole theorem prover. They're given two 4.5 hour sessions (9 hours total) to solve all the problems with nothing but pencils, rulers, and compasses [0]. This model, meanwhile, was wired up to a theorem proover and took three solid days to solve the problems. The article is extrem…
I can tell you that as someone who could have gotten bronze (i was too weak for the team) and is now a math phd--I would not have scored as well as alphaproof in three days most likely. In most problems either you find an idea soon or it can be much much longer. It's just not a matter of working and constant progress.
Noting the difference in humility between someone that has made the cut to participate in the IMO (6 people per country) and the multitude of retrospect prophets that trivialize the DeepMind achievement.
Re: AI solves International Math Olympiad problems at silver medal level
#384Earlier quoted context omitted.
[flagged]
That wasn't very nice. Are you curious about anything? Happy to help. I'd proactively do it, but I don't want to guess at whats in your mind. My initial guess is you think I think that engaging with the public is an infinite loop. I don't!
[deleted]
Re: AI solves International Math Olympiad problems at silver medal level
#385Earlier quoted context omitted.
I don't believe anything was graded by the IMO, Google is just giving itself 7 for anything proved in Lean (which is reasonable IMO), so they can't really try for partial credit so much as choose not to report a higher self-graded number.
From the article: "Our solutions were scored according to the IMO’s point-awarding rules by prominent mathematicians Prof Sir Timothy Gowers, an IMO gold medalist and Fields Medal winner, and Dr Joseph Myers, a two-time IMO gold medalist and Chair of the IMO 2024 Problem Selection Committee."
Fair enough. Although I think the question is whether P3/P5 were given zero points vs not evaluated vs evaluated but not published. I don't think it is surprising that Lean-verified proofs get a 7.
Re: AI solves International Math Olympiad problems at silver medal level
#386Earlier quoted context omitted.
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?
[deleted]
Re: AI solves International Math Olympiad problems at silver medal level
#387Earlier quoted context omitted.
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…
AlphaGeometry is not an LLM
Re: AI solves International Math Olympiad problems at silver medal level
#388In 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…
The success in Go was very much not dumb search. Where dumb search had failed to achieve the level of even a very weak player, the neural net's "intuition" about good moves without any search was already very strong. Only the combination was superhuman, and that was anything but the dumb search that had been tried before. Today's announcement is also not about proving Lean theorems by "dumb search". The success is ab…
I think that was the op's point.
Re: AI solves International Math Olympiad problems at silver medal level
#389I'm seriously jealous of the people getting paid to work on this. Sounds great fun and must be incredibly satisfying to move the state of the art forward like that.
I don't know about that. A lot of the work that should have been very satisfying turned out to be boring as hell, if not toxic, while at the same time, some apparently mundane stuff turned out to be really exciting. I found the work environment to be more important than the subject when it comes to work satisfaction. If you are working on a world changing subject with a team of assholes, you are going to have a bad t…
Awesome work environment for one person can be not ideal for another.
Pretty much all the top AI labs are both intensely competitive and collaborative. They consist of many former IMO and IOI medalists. They don't believe in remote work, either. Even if you work at Google DeepMind, you really need to be in London for this project.
Re: AI solves International Math Olympiad problems at silver medal level
#390[dead]