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

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

#321

Post by visarga » Thu, Jul 25, 2024, 9:33 PM UTC

xdavidliu wrote: post #256

visarga wrote: post #113

Earlier quoted context omitted.

Search is extrapolation. Learning is interpolation. Search+Learn is the formula used by AZ. Don't forget AZ taught us humans a thing or two about a game we had 2000 years head start in, and starting from scratch not from human supervision.

no, search is not extrapolation. Extrapolation means taking some data and projecting out beyond the limits of that data. For example, if my bank account had $10 today and $20 tomorrow, then I can extrapolate and say it might have $30 the day after tomorrow. Interpolation means taking some data and inferring the gaps of that data. For example, if I had $10 today and $30 the day after tomorrow, I can interpolate and sa…

Search can go from a random init model to beating humans at Go. That is not interpolation.

- Search allows exploration of the game tree, potentially finding novel strategies.

- Learning compresses the insights gained from search into a more efficient policy.

- This compressed policy then guides future searches more effectively.

Evolution is also a form of search, and it is open-ended. AlphaProof solved IMO problems, those are chosen to be out of distribution, simple imitation can't solve them. Scientists do (re)search, they find novel insights nobody else discovered before. What I want to say is that search is on a whole different level than what neural nets do, they can only interpolate their training data, search pushes outside of the known data distribution.

It's actually a combo of search+learning that is necessary, learning is just the little brother of search, it compresses novel insights into the model. You can think of training a neural net also as search - the best parameters that would fit the training set.

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

#322

Post by cynicalpeace » Thu, Jul 25, 2024, 9:36 PM UTC

ertgbnm wrote: post #308

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.

I'm sure humans will always enjoy chess and art regardless of how much better AI is at it. In the same way, there will probably always be mathematic hobbyist who study math for fun. But I seriously doubt that in the near future there will be mathematicians who will be publishing new advancements that aren't mostly or entirely discovered by AI. A human might get credit for a proof for asking the initial question, but…

My point was where does the concept of "meaningful" come from?

The proof will only have value if it's meaningful to us.

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

#323

Post by christianqchung » Thu, Jul 25, 2024, 9:37 PM UTC

cynicalpeace wrote: post #298

christianqchung wrote: post #254

Earlier quoted context omitted.

> This principle is broadly extensible to work and art Nah, as a consumer it makes no difference to me if a meat packing factory or Amazon warehouse employs 5000 or 5 people. To art, this principle is totally real, but for work, it only applies to some/most of it.

Read the next sentence: "We only care about machines insofar as it serves us." Imagine a machine doing "work" that only serves itself and other machines that does no service to humanity. It would have no economic value. In fact the whole concept of "work" only makes sense if it is assigned economic value by humans.

Then we agree, but your chess example made it sound like if a machine could automatically pack meat with little human intervention, people wouldn't want it. That's also not the next sentence. How is it broadly applicable to work?

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

#324

Post by ComplexSystems » Thu, Jul 25, 2024, 9:38 PM UTC

Ericson2314 wrote: post #99

Smaug123 wrote: post #29

Earlier quoted context omitted.

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

Hehe, well, we'll need to have a tool-assited international math Olympiad then.

This is the greatest idea ever. Why doesn't this exist?

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

#325

Post by data_maan » Thu, Jul 25, 2024, 9:38 PM UTC

It's bullshit. AlphaGeometry can't even solve Pythagoras theorem.

Not opensourcing anything.

This is a dead end on which no further research can be built.

It violates pretty much every principle of incremental improvement on which science is based. It's here just for hype, and the 300+ comments prove it.

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

#326

Post by cynicalpeace » Thu, Jul 25, 2024, 9:40 PM UTC

fanatic2pope wrote: post #318

hyperbovine wrote: post #275

Earlier quoted context omitted.

What if the proof were incomprehensible to humans?

If it cannot explain how it was proven, was it actually proven?

No. Funny how these discussions too often devolve into semantics lol.

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

#327

Post by data_maan » Thu, Jul 25, 2024, 9:40 PM UTC

falcor84 wrote: post #54

nnarek wrote: post #37

Earlier quoted context omitted.

"three days" does not say anything about how much computational power is used to solve problems, maybe they have used 10% of all GCP :)

And say they did use 10% of all GCP? Would it be less impressive? This is a result that was considered by experts to be far beyond the state of the art; it's absolutely ok if it's not very efficient yet. Also, for what it's worth, I'm pretty sure that I wouldn't have been able to solve it myself in three days, even if I had access to all of GCP, Azure and AWS (except if I could mine crypto to then pay actual IMO-leve…

Which experts said that?

I don't think that's the case at all. The writing was already on the wall.

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

#328

Post by ComplexSystems » Thu, Jul 25, 2024, 9:40 PM UTC

lumb63 wrote: post #312

Can someone explain why proving and math problem solving is not a far easier problem for computers? Why does it require any “artificial intelligence” at all? For example, suppose a computer is asked to prove the sum of two even numbers is an even number. It could pull up its list of “things it knows about even numbers”, namely that an even number modulo 2 is 0. Assuming the first number is “a” and the second is “b”,…

What you're missing is that this kind of thing has arbitrarily been declared "artificial intelligence" territory. Once the ability of computers to do has been established, it will no longer be artificial intelligence territory; at that point it'll just be another algorithm.

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

#329

Post by booleandilemma » Thu, Jul 25, 2024, 9:41 PM UTC

lumb63 wrote: post #312

Can someone explain why proving and math problem solving is not a far easier problem for computers? Why does it require any “artificial intelligence” at all? For example, suppose a computer is asked to prove the sum of two even numbers is an even number. It could pull up its list of “things it knows about even numbers”, namely that an even number modulo 2 is 0. Assuming the first number is “a” and the second is “b”,…

Proofs require a certain ingenuity that computers just don't have, imo. A computer would never be able to come up with something like Cantor's diagonalization proof on its own.

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

#330

Post by randcraw » Thu, Jul 25, 2024, 9:42 PM UTC

thomasahle wrote: post #158

visarga wrote: post #106

Earlier quoted context omitted.

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

And I understand the upper time limit for each question was 4.5 hours. So it solved one question almost immediately, two well over the allotted time (60 hrs), and two not at all. No medal for you, Grasshopper.