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

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

#241

Post by thrance » Thu, Jul 25, 2024, 7:32 PM UTC

camjw wrote: post #235

thrance wrote: post #230

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 wi…

> 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"?

My intuition tells me we humans are generally very bad at math. Proving a theorem, in an ideal way, mostly involves going from point A to point B in the space of all proofs, using previous results as stepping stones. This isn't particularly a "hard" problem for computers which are able to navigate search spaces for various games much more efficiently than us (chess, go...).

On the other hand, navigating the real world mostly consists in employing a ton of heuristics we are still kind of clueless about.

At the end of the day, we won't know before we get there, but I think my reasons are compelling enough to think what I think.

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

#242

Post by raincole » Thu, Jul 25, 2024, 7:32 PM UTC

thrdbndndn wrote: post #180

thomasahle wrote: post #145

Earlier quoted context omitted.

You'd think that, but Timothy Gowers (the famous mathematician they worked with) wrote ( https://x.com/wtgowers/status/1816509817382735986 ) > However, LLMs are not able to autoformalize reliably, so they got them to autoformalize each problem many times. Some of the formalizations were correct, but even the incorrect ones were useful as training data, as often they were easier problems. So didn't actually solve auto…

> However, LLMs are not able to autoformalize reliably, so they got them to autoformalize each problem many times. Some of the formalizations were correct, but even the incorrect ones were useful as training data, as often they were easier problems. A small detail wasn't clear to me: for these incorrectly formalized problems, how do they get the correct answer as ground truth for training? Have a human to manually so…

They said the incorrectly formalized ones are usually easier, so I assume they just hire humans to solve them in the old way until the AI is smart enough to solve these easier problems.

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

#243

Post by sebzim4500 » Thu, Jul 25, 2024, 7:33 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`.

The uses of `nlinarith` are very straight forward manipulations of inequalities, they would be one or two steps for a human too.

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

#244

Post by piombisallow » Thu, Jul 25, 2024, 7:39 PM UTC

osti wrote: post #19

piombisallow wrote: post #5

IMO problems aren't fundamentally different from chess or other games, in that the answer is already known.

But the answer is probably not known by you, in particular.

Yes, sure, but this doesn't mean that this generalizes to open math research problems, which would be the useful real-world application of this. Otherwise this is just playing known games with known rules, granted better/faster than humans.

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

#245

Post by vlovich123 » Thu, Jul 25, 2024, 7:39 PM UTC

visarga wrote: post #119

vlovich123 wrote: post #91

Earlier quoted context omitted.

We're not talking about mathematical optimality here, both from the solution found and for the time taken. The point is whether this finds results more cheaply than a human can and right now it's better on some problems while others it's worse. Clearly if a human can do it, there is a way to solve it in a cheaper amount of time and it would be flawed reasoning to think that improving the amount of time would be asymp…

> The point is whether this finds results more cheaply than a human can If you need to solve 1000 problems in 3 days you wouldn't find the humans that can do it. So it would not be cheaper if it's not possible.

Well if it takes 10% of all of Google’s servers 3 days to solve, you may find it difficult to scale out to solving 1000 problems in 3 days as well.

As for humans, 100 countries send 6 students to solve these problems. It also doesn’t mean that these problems aren’t solvable by anyone else. These are just the “best 6” where best = can solve and solve most quickly. Given a three day budget, 1000 problems could reasonably be solvable and you know exactly who to tap to try to solve them. Also, while the IMO is difficult and winners tend to win other awards like Field Medals, there’s many professional mathematicians who never even bother because that type of competition isn’t interesting to them. It’s not unreasonable to expect that professional mathematicians are able to solve these problems as well if they wanted to spend 3 days on it.

But in terms of energy per solve, humans are definitely cheaper. As you note the harder part is scaling it out but so far the AI isn’t solving problems that are impossible for humans, just that given enough time it managed to perform the same task. That’s a very promising result but supremacy is slightly a ways off for now (this AI can’t win the competition for now)

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

#246

Post by sebzim4500 » Thu, Jul 25, 2024, 7:39 PM UTC

gowld wrote: post #212

JKCalhoun wrote: post #196

Earlier quoted context omitted.

Yeah I am not clear the degree to which this system and LLMs are related. Are they related? Or is AlphaProof a complete tangent to CHatGPT and its ilk?

It's not an English LLM (Large Language Model). It's a math Language Model. Not even sure it's a Large Language Model. (Maybe shares a foundational model with an English LLM; I don't know) It learns mathematical statements, and generates new mathematical statements, then uses search techniques to continue. Similar to Alpha Go's neural network, what makes it new and interesting is how the NN/LLM part makes smart guess…

My reading of it is that it uses the same architecture as one of the Gemini models but does not share any weights with it. (i.e it's not just a finetune)

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

#247

Post by raincole » Thu, Jul 25, 2024, 7:41 PM UTC

camjw wrote: post #235

thrance wrote: post #230

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 wi…

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

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

#248

Post by balls187 » Thu, Jul 25, 2024, 7:45 PM UTC

password54321 wrote: post #202

balls187 wrote: post #67

Earlier quoted context omitted.

The point isn't IMO rules. It's that we are living in a period of time where there are very real consequences of nearly a century of unchecked CO2 due to human industry. And AI (like crypto before it) requires considerable energy consumption. Because of which, I believe we (people who believe in AI) need to hold companies accountable by very transparently disclosing those energy costs.

> need to hold companies accountable by very transparently disclosing those energy costs. And if they do, then what? If it is "too high" do we delay research because we need to keep the world how it is for you? What about all the other problems others face that could be solved by doubling down on compute for AI research?

> And if they do, then what? If it is "too high" do we delay research because we need to keep the world how it is for you?

First, it's keeping the world how it is for all of us, not just me.

Second, to answer you question, I think that is a decision for all of us to weigh in on, but before we can do that, we must be informed as best as we can.

Do sacrifices have to be made for the greater good? Absolutely. Do for-profit mega corporations get to make those decisions without consent from the public? No.

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

#249

Post by balls187 » Thu, Jul 25, 2024, 7:47 PM UTC

ks2048 wrote: post #178

amelius wrote: post #107

Earlier quoted context omitted.

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

I know this is not an uncommon opinion in tech circles, but I believe an insane thing to hang humanities hopes on. There's no reason to think AI will be omnipotent.

There is not, but there is plenty of historical evidence that scientific and technological progress has routinely addressed humanities crisis du jour.

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

#250

Post by awahab92 » Thu, Jul 25, 2024, 7:47 PM UTC

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.

magnus carlsen basically quit because computers ruined chess. As did kasparov.

Fischer was probably the last great player who was unassisted by tools.