This is kind of an ideal use-case for AI, because we can say with absolute certainty whether their solution is correct, completely eliminating the problem of hallucination.
AI solves International Math Olympiad problems at silver medal level
171–180 of 564 posts
Re: AI solves International Math Olympiad problems at silver medal level
#172Earlier quoted context omitted.
> 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.
Why? Why is hype bad? What actual harm does it cause? Also the headline is fair, as I do believe that AlphaProof demonstrates an approach to mathematics that will indeed invade mathematicians workspaces. And I say that as a mathemstician.
For sure. I feel like mathematicians are not paying attention (maybe deliberately) we have a real shot of solving some incredibly hard open problem in the next few years.
Re: AI solves International Math Olympiad problems at silver medal level
#173Earlier quoted context omitted.
Compared to all of the humans who compete at this level and their inputs and outputs for the trailing 5 years.
And? The result is (likely) net energy consumption, resulting in (likely) net CO2 emissions. So, what was did it cost us for this achievement in AI? EDIT TO ADD: It's fair to think that such a presser should not include answers to my questions. But, it's also fair to want that level of transparency given we are dealing with climate change.
You're not wrong and in general the conclusion is that AI emits less CO2 than a human performing the same task. Whether that's true for this specific task is worth asking, as is the question of how efficient such a process can be made.
Re: AI solves International Math Olympiad problems at silver medal level
#174This 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…
And why aren't you complaining that human participants could train and study for thousands of hours before attempting the problems? And that the training materials they used was itself created and perfected by hundreds of other people, after having themselves spend countless hours studying?
Because so did the AI?
Re: AI solves International Math Olympiad problems at silver medal level
#175Earlier 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?
"AlphaProof is a system that trains itself to prove mathematical statements in the formal language Lean. It couples a pre-trained language model with the AlphaZero reinforcement learning algorithm, which previously taught itself how to master the games of chess, shogi and Go."
Re: AI solves International Math Olympiad problems at silver medal level
#176Earlier 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`.
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?
nlinarith is a proof automation that attempts to finish a proof using the simplex method to find a linear combination of hypotheses and things that have already been proven, as well as some quadratic terms of them.
Docs: https://leanprover-community.github.io/mathlib4_docs/Mathlib...
Re: AI solves International Math Olympiad problems at silver medal level
#177In 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-play. Critics noted that while this fancy form of "dumb search" worked for Go, it might not necessarily be a general strategy applicable to other cognitive tasks.[a]
In 2024, machines solved insanely hard math problems at the Silver Medal level in an International Math Olympiad for the first time, using a clever form of "dumb search" that leverages compute, DNNs, RL, and a formal language. Perhaps "dumb search" over cleverly pruned spaces isn't as dumb as the critics would like it to be?
---
[a] http://www.incompleteideas.net/IncIdeas/BitterLesson.html
Re: AI solves International Math Olympiad problems at silver medal level
#178Earlier 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?
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.
Re: AI solves International Math Olympiad problems at silver medal level
#179> First, the problems were manually translated into formal mathematical language
That is more than half the work of solving them. Headline should read "AI solves the simple part of each IMA problem at silver medal level"
Re: AI solves International Math Olympiad problems at silver medal level
#180Earlier quoted context omitted.
To speak generally, that translation part is much easier than the proof part. The problem with automated translation is that the translation result might be incorrect. This happens a lot when even people try formal methods by their hands, so I guess the researchers concluded that they'll have to audit every single translation regardless of using LLM or whatever tools.
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 solve them?
(In contrast to problems actually from "a huge database of IMO-type problems", they do have answers for these already).