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

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

#131

Post by lacker » Thu, Jul 25, 2024, 5:21 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?

The training loop was also applied during the contest, reinforcing proofs of self-generated variations of the contest problems until a full solution could be found.

So they had three days to keep training the model, on synthetic variations of each IMO problem.

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

#132

Post by trotro » Thu, Jul 25, 2024, 5:23 PM UTC

petters wrote: post #6

The problems were first converted into a formal language. So they were partly solved by the AI

But formalization is the easy part for humans. I'm sure every mathematician would be be happy if the only thing required to prove a result was to formalize it in Lean and feed it to the AI to find the proof.

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

#133

Post by noud » Thu, Jul 25, 2024, 5:23 PM UTC

skywhopper wrote: post #97

Except it didn’t. The problem statements were hand-encoded into a formal language by human experts, and even then only one problem was actually solved within the time limit. So, claiming the work was “silver medal” quality is outright fraudulent.

I had exactly the same feeling when reading this blog. Sure, the techniques used to find the solutions are really interesting. But the claim more than they achieve. The problem statements are not available in Lean, and the time limit is 2 x 4.5 hours. Not 3 days.

The article claims they have another model that can work without formal languages, and that it looks very promising. But they don't mention how well that model performed. Would that model also perform at silver medal level?

Also note, that if the problems are provided in a formal language, you can always find the solution in finite amount of time (provided the solution exists). You can brute-force over all possible solutions until you find the solution that proofs the statement. This may take a very long time, but it will find the solutions eventually. You will always solve all the problems and win the IMO at gold medal level. Alphaproof seems to do something similar, but takes smarter decisions which possible solutions to try and which once to skip. What would be the reason they don't achieve gold?

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

#134

Post by visarga » Thu, Jul 25, 2024, 5:23 PM UTC

lolinder wrote: post #101

golol wrote: post #92

Earlier quoted context omitted.

"Solving IMO problems at Silver-Medal level" is pretty much equivalent to solving something like 4/6 problems. It is only a disingenious comparison if you want to read it as a comparison. I mean yea, many people will, but I don't care anout them. People who are technically interested in this know that the point is not to have a competition of AI with humans.

> but I don't care anout them It's great that you feel safe being so aloof, but I believe we have a responsibility in tech to turn down the AI hype valve. The NYT is currently running a piece with the headline "Move Over, Mathematicians, Here Comes AlphaProof". People see that, and people react, and we in tech are not helping matters by carelessly making false comparisons.

I think search-based AI is on a different level than imitation models like GPT. This is not a hallucinating model, and it could potentially discover things that are not written in any books.

Search is amazing. Protein folding searches for the lowest energy configuration. Evolution searches for ecological fit. Culture searches for progress, and science for understanding. Even placing a foot on the ground searches for dynamic equilibrium. Training a ML model searches for best parateters to fit a dataset. Search is universal. Supervised learning is just imitative, search is extrapolative.

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

#135

Post by Jun8 » Thu, Jul 25, 2024, 5:24 PM UTC

Tangentially: I found it fascinating to follow along the solution to Problem 6: https://youtu.be/7h3gJfWnDoc (aquaesulian is a node to ancient name of Bath). There’s no advanced math and each step is quite simple, I’d guess on a medium 8th grader level.

Note that the 6th question is generally the hardest (“final boss”) and many top performers couldn’t solve it.

I don’t know what Lean is or how see AI’s proofs but an AI system that can explain such a question on par with the YouTuber above would be fantastic!

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

#136

Post by jercos » Thu, Jul 25, 2024, 5:24 PM UTC

ToucanLoucan wrote: post #60

lolinder wrote: post #57

Earlier quoted context omitted.

It feels pretty disingenuous to claim silver-medal status when your machine played by significantly different rules. The article is light on details, but it says they wired it up to a theorem prover, presumably with feedback sent back to the AI model for re-evaluation. How many cycles of guess-and-check did it take over the course of three days to get the right answer? If the IMO contestants were allowed to use theor…

I am so exhausted of the AI hype nonsense. LLMs are not fucking curing cancer. Not now, not in five years, not in a hundred years. That's not what they do. LLM/ML is fascinating tech that has a lot of legitimate applications, but it is not fucking intelligent, artificial or otherwise, and I am sick to death of people treating it like it is.

A significant part of the problem is that a majority of people are unaware of just how simple what they consider "intelligence" really is. You don't need actual intelligence to replace the public-facing social role of a politician, or a talking head, or a reactive-only middle manager. You just need words strung together that fit a problem.

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

#137

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

amelius wrote: post #107

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.

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?

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

#138

Post by throwaway240403 » Thu, Jul 25, 2024, 5:26 PM UTC

poincaredisk wrote: post #46

ComplexSystems wrote: post #25

Earlier quoted context omitted.

Or the simultaneous discovery of thousands of cryptographic exploits...

Still waiting for the first one. I'm not holding my breath - just like fuzzing found a lot of vulnerabilities in low-level software, I expect novel automated analysis approaches will yield some vulnerabilities - but that won't be a catastrophic event just like fuzzing wasn't.

Hope that's true. Really mucks up the world a bit if not.

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

#139

Post by kurthr » Thu, Jul 25, 2024, 5:26 PM UTC

Smaug123 wrote: post #35

So I am extremely hyped about this, but it's not clear to me how much heavy lifting this sentence is doing: > First, the problems were manually translated into formal mathematical language for our systems to understand. The non-geometry problems which were solved were all of the form "Determine all X such that…", and the resulting theorem statements are all of the form "We show that the set of all X is {foo}". The do…

As is often the case, creating a well formed problem statement often takes as much knowledge (if not work) as finding the solution.

But seriously, if you can't ask the LLM to solve the right question, you can't really expect it to give you the right answer unless you're really lucky. "I'm sorry, but I think you meant to ask a different question. You might want to check the homework set again to be sure, but here's what I think you really want."

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

#140

Post by visarga » Thu, Jul 25, 2024, 5:27 PM UTC

StefanBatory wrote: post #79

Wow, that's absolutely impressive to hear! Also it's making me think that in 5-10 years almost all tasks involving computer scientists or mathematicians will be done in AI. Perhaps people going into trades had a point.

Everything that allows for cheap validation is going that way. Math, code, or things we can simulate precisely. LLM ideation + Validation is a powerful combination.