AI solves International Math Olympiad problems at silver medal level • Hacker News Board

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

#151

Post by pishpash » Thu, Jul 25, 2024, 5:39 PM UTC

pclmulqdq wrote: post #118

dooglius wrote: post #52

Earlier quoted context omitted.

The linked page says > While the problem statements were formalized into Lean by hand, the answers within the problem statements were generated and formalized by the agent. However, it's unclear what initial format was given to the agents that allowed this step

So if Lean was used to find the answers, where exactly is the AI? A thin wrapper around Lean?

The AI is the "solver network", which is the (directed) search over solutions generated by Lean. The AI is in doing an efficient search, I suppose.

I'm also waiting for my answer on the role of the Gemini formalizer, but reading between the lines, it looks like it was only used during training the "solver network", but not used in solving the IMO problems. If so then the hyping is greatly premature, as the hybrid formalizer/solver is the whole novelty of this, but it's not good enough to use end-to-end?

You cannot say AlphaProof learned enough to solve problems if formalization made them easier to solve in the first place! You can say that the "solver network" part learned enough to solve formalized problems better than prior training methods.

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

#152

Post by Davidzheng » Thu, Jul 25, 2024, 5:39 PM UTC

Smaug123 wrote: post #51

nwoli wrote: post #45

Earlier quoted context omitted.

Guessing the context here is that the RH was recently translated into Lean. Would be very cool if they threw their compute on that

I think you might be thinking of the recent project to start Fermat's Last Theorem? The Riemann hypothesis has been easy to state (given what's in Mathlib) for years.

Yeah lol i don't think either is hard to formalize in lean

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

#153

Post by Davidzheng » Thu, Jul 25, 2024, 5:40 PM UTC

majikaja wrote: post #115

cygaril wrote: post #89

Earlier quoted context omitted.

Proofs are here: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...

I found those, I just would have appreciated if the content of the mathematics wasn't sidelined to a separate download as if it's not important. I felt the explanation on the page was shallow, as if they just want people to accept it's a black box. All I've learnt from this is that they used an unstated amount of computational resources just to basically brute force what a human already is capable of doing in far les…

Very few humans can after years of training. Please don't trivialize.

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

#154

Post by pmcf » Thu, Jul 25, 2024, 5:41 PM UTC

I read this as “In My Opinion” and really thought this about AI dealing with opinionated people. Nope. HN is still safe. For now…

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

#155

Post by xrisk » Thu, Jul 25, 2024, 5:44 PM UTC

Smaug123 wrote: post #29

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.

And while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be constructing Gröbner bases in their head, but `polyrith` is just eight characters away. I saw AlphaProof used `nlinarith`.

Can you give some context on how using Lean benefits?

In my understanding, proofs are usually harder to transcribe into Lean which is nobody _writes_ proofs using Lean.

What is a nlinarith?

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

#156

Post by dsign » Thu, Jul 25, 2024, 5:45 PM UTC

visarga wrote: post #111

ZenMikey wrote: post #8

Earlier quoted context omitted.

I haven't read TFA as I'm at work, but I would be very interested to know what the system was doing in those three days. Were there failed branches it explored? Was it just fumbling its way around until it guessed correctly? What did the feedback loop look like?

> just fumbling its way around until it guessed correctly As opposed to 0.999999% of the human population who can't do it even if their life depends on it?

I was going to come here to say that. I remember being a teenager and giving up in frustration at IMO problems. And I was competing at IPhO.

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

#157

Post by empath75 » Thu, Jul 25, 2024, 5:45 PM UTC

Smaug123 wrote: post #29

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.

And while AlphaProof is clearly extremely impressive, it does give the computer an advantage that a human doesn't have in the IMO: nobody's going to be constructing Gröbner bases in their head, but `polyrith` is just eight characters away. I saw AlphaProof used `nlinarith`.

Don't think of lean as a tool that the ai is using (ie, cheating), think of lean plus AlphaProof as a single system. There's no reason to draw artificial boundaries around where the AI is and where the tools that the AI is using are. Lean itself is a traditional symbolic artificial intelligence system.

People want always knock generative AIs for not being able to reason, and we've had automated systems that reason perfectly well for decades, but for some reason that doesn't count as AI to people.

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

#158

Post by thomasahle » Thu, Jul 25, 2024, 5:46 PM UTC

visarga wrote: post #106

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…

> a lot of brute force search Don't dismiss search, it might be brute force but it goes beyond human level in Go and silver at IMO. Search is also what powers evolution which created us, also by a lot of brute forcing, and is at the core of scientific method (re)search.

Also AlphaProof had to search for 60 hours for one of the IMO problems it solved.

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

#159

Post by sensanaty » Thu, Jul 25, 2024, 5:47 PM UTC

Sivart13 wrote: post #137

amelius wrote: post #107

Earlier quoted context omitted.

What if at some point AI figures out a solution to climate change?

Why would we be any more likely to implement it, relative to the solutions that humans have already figured out for climate change?

Well we can be confident in the knowledge that techbros might finally take the issue seriously if an AI tells them to!

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

#160

Post by thomasahle » Thu, Jul 25, 2024, 5:49 PM UTC

ZenMikey wrote: post #8

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…

I haven't read TFA as I'm at work, but I would be very interested to know what the system was doing in those three days. Were there failed branches it explored? Was it just fumbling its way around until it guessed correctly? What did the feedback loop look like?

They just write "it's like alpha zero". So presumably they used a version of MCTS where each terminal node is scored by LEAN as either correct or incorrect.

Then they can train a network to evaluate intermediate positions (score network) and one to suggest things to try next (policy network).