Leading LLMs get <5% scores on USAMO (which selects participants for the IMO): https://arxiv.org/abs/2503.21934

@pietrokc Bear in mind that this market is not limited to LLMs

@JimHays Oh, for sure; and LLMs were never the most likely avenue for this to be achieved.

I just think there is a certain current of thought in the AI hypersphere (which includes a lot of Manifold) for which this result should be a big update.

@pietrokc leading LLMs scored 28 in IMO 2024, and Gold started at 29

@mathvc No, leading AI systems did, but not LLMs.

AlphaGeometry is a neuro-symbolic system made up of a neural language model and a symbolic deduction engine, which work together to find proofs for complex geometry theorems. Akin to the idea of “thinking, fast and slow”, one system provides fast, “intuitive” ideas, and the other, more deliberate, rational decision-making.

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.

So while these systems include language models, they are not themselves LLMs, it’s not the language models that are doing the heavy mathematical lifting.

@JimHays I don’t know who taught you all these words but AlphaProof is LLM with tree search on top. Tree search is literally sampling (i.e. one of many ways to use LLM)

There is nothing neurosymbolic in it. It’s just a fancy words used by people who don’t know Lean.

@mathvc Take it up with the creators of the models then. I’m quoting from their blog posts announcing the results. They say that their systems include, but are not limited to, language models.

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry/

@JimHays you confused AlphaProof with AlphaGeometry then. The quotes are about AlphaGeometry, it isn’t LLM. AlphaProof is nothing more than LLM

Wikipedia says:

AlphaProof is an AI model, which couples a pre-trained language model with the AlphaZero reinforcement learning algorithm.

AlphaZero (AZ) is a more generalized variant of the AlphaGo Zero (AGZ) algorithm, and is able to play shogi and chess as well as Go.

I’m not sure why you consider that to be nothing more than an LLM?

@JimHays yes i do because i understand what is “AlphaZero” and implemented it many times myself for combinatorial search.

It’s a sampling technique on top of LLM (or on top of any policy network in RL environment).

There are tons of ways to change sampling from LLM (eg change temperature, best of k, maximum likelihood, etc), it doesn’t turn it into non-LLM

You can bet more on NO instead of arguments

I mean, this conversation isn’t really related to the market, since this market is about AI generally, not LLMs. It doesn’t matter in this context how they are categorized.

@JimHays DeepSeek has paper that gives much more details on LLMs+TreeSearch https://arxiv.org/pdf/2408.08152

I keep coming back to this market and wanting to bet but ultimately deciding against it. IMO takes place in ~July, and as anyone who's been in that milieu knows, solutions go up on various websites pretty much the next day, including many superficial variants where the key idea is the same.

Therefore, the deadline of EoY 2025 is nuts. It's way too long, models available by then will definitely have seen the questions. So this market will come down to whether two random people think the eval was "fair", and there's no way to be >80% confident in that.

I believe this market is much closer to the spirit of "can AI do IMO?": https://manifold.markets/jack/will-an-ai-win-a-gold-medal-on-imo

Will an AI win a gold medal on International Math Olympiad (IMO) 2025?

77% chance. Will an AI score well enough on the 2025 International Mathematics Olympiad (IMO) to earn a gold medal score (top ~50 human performance)? Resolves YES if this result is reported no later than 1 month after IMO 2025 (currently scheduled for July 10-20). The AI must complete this task under the same time limits as human competitors. The AI may receive and output either informal or formal problems and proofs. More details below. Otherwise NO. This is related to https://imo-grand-challenge.github.io/ but with some different rules. Rules: The result must be achieved on the IMO 2025 problemset and be reported by reliable publications no later than 1 month after the end of the IMO contest dates (https://www.imo-official.org/organizers.aspx, so by end of August 20 2025, if the IMO does not reschedule its date. Local timezone at the contest site). The AI has only as much time as a human competitor (4.5 hours for each of the two sets of 3 problems), but there are no other limits on the computational resources it may use during that time. The AI may receive and output either informal (natural language) or formal (e.g. the Lean language) problems as input and proofs as output. The AI cannot query the Internet. The AI must not have access to the problems before being evaluated on them, e.g. the problems cannot be included in the training set. (The deadline of 1 month after the competition is intended to give enough time for results to be finalized and published, while minimizing the chances of any accidental inclusion of the IMO solutions in the training set.) If a gold medal score is achieved on IMO 2024 or an earlier IMO, that would not count for this market.

@pietrokc I don't think Yudkowsky and Christiano are "two random people"

To me, the biggest uncertainties (and the reason why I don't bet) are whether the IMO organizers will select anti-AI problems this year, and whether top AI orgs will invest a lot into this specific benchmark

@Lorenzo I don't know much about either of them so to me they're just random people.

I'm leaning pretty heavily NO on the substance of this question. The scenario I envision is that in Dec 2025 models will definitely be able to gold IMO 2025, because they will have been trained on it. Then, some AI company might allege they "filtered out" IMO 2025 from training (as if this was possible to do reliably). At that point, I don't know how Yudkowsky or Christiano will react. Even worse, this market is biased to resolve YES, because it only requires one of them to say YES.

I'm definitely not >20% sure they'll both give the correct answer of NO in the scenario I described above.

@pietrokc The difference between Eliezer's and Paul's statements is significant here, yeah. "For the 2022, 2023, 2024, or 2025 IMO an AI built before the IMO is able to solve the single hardest problem" is very different to "the technical capability existing by end of 2025".

Buuut, the market criteria outside of the quotes is much clearer, and only includes AIs built before the IMO:

"So I think we have Paul at <8%, Eliezer at >16% for AI made before the IMO is able to get a gold (under time controls etc. of grand challenge) in one of 2022-2025. Resolves to YES if either Eliezer or Paul acknowledge that an AI has succeeded at this task."

I'm assuming the market maker will only include Eliezer or Paul saying it achieved that statement, not them saying it achieved IMO by EOY. Still some wiggle room there though.

@pietrokc problem says "AI made before the IMO" which I think precludes the its-in-the-training-data condition

@JamesBaker3 @Grizzimo What you say is all fair but I think there is a lot of fuzziness around when an LLM was "made". It's a very long pipeline, and companies are incentivized to fudge things and claim models were finished earlier than they really were if you account for RLHF etc. Like, I think it's very possible that some large company may release a model in October that it claims "has training data cutoff May 2025" (say), and still it has seen the IMO questions somehow.

@Lorenzo what would an anti-AI problem selection look like?

@Odoacre I don't know, but I expect them to know. As one potential example, maybe less geometry and more game theory? I think AIs might currently do badly in IMO problems like: there's this contrived game between Alice and Bob, prove that Alice has a winning strategy iff the gameboard side is a power of two

@Odoacre Combinatorics instead of problems for AlphaGeom or AlphaProof?

Surely the AI must earn the gold medal under normal time constraints, right? Otherwise an "AI" that just enumerates theorems of ZFC will eventually solve all the problems.

The AlphaProof blog post (for which I'm unable to find a corresponding paper), which describes an AI system which solved 4 of 6 problems, claims it solved some problems in "minutes" and some in "up to three days".

https://garymarcus.substack.com/p/alphageometry2-impressive-accomplishment
Impressive indeed, however does this count for this market if the problem are translated before being solved by the AI, and the result is not clearly human readable.

@Zardoru Paul said that formal proofs count. https://manifold.markets/Austin/will-an-ai-get-gold-on-any-internat#QuXuluE8CGMjalzyqOx4

Why there is so much progress this year (and it is just the beginning): https://benjamintodd.substack.com/p/teaching-ai-to-reason-this-years