$10M AI Mathematical Olympiad Prize

by jasondavies • 3 years ago

281 225 3 years ago

gregdoesit• 3 years ago

I was recently in Palo Alto, and bumped into a newly founded startup (I don't remember the name unfortunately) who set themselves the grand the vision of exactly this: winning a gold medal on the international Olympiad using AI. Their plan was to build mostly on LLMs as a start, and iterate as they go. In their barebones office space, they had a poster with a countdown of the number of weeks till the event: it was 36 at the time.

It sounded interesting to wonder how far they could go with this kind of approach. I thought they were aiming for the moon: but also respected the boldness and determination. They had the funding to operate for at least a year, and were very focused to get there.

Seems like this prize will supr hundreds (or thousands) of teams competing in exactly this space. Perhaps it will have a similar effect like the $1M Netflix Prize in 2009 for recommendations algorithms!

anonylizard6• 3 years ago

Well math solving is exactly what the rumored Q* is aiming towards too. I don't think it'll take more than 2 years before some LLM + RL system can take the gold medal.

I think companies like OpenAI are aiming for something far more ambitious, like solving a millennium prize problem (even with human assistance). That's the kind of news release that'll add another $100 billion to your market cap.

dimask3• 3 years ago

Their current ambition is to be able to solve school math, which is quite far away from solving unsolved conjectures or math olympiads. I really doubt that any of this is within LLM/transformer scope, except maybe in some auxiliary sense to other, much different architectures.

antoinexp• 3 years ago

Might depend on the terms you have in mind, but current consensus seems to be more like 4-5 years as we speak on https://www.metaculus.com/questions/6728/ai-wins-imo-gold-me...

eddtries8• 3 years ago

I have a couple friends who did the Math tripos at Cambridge (so a pretty high level!) who work in tech and have unanimously said they have 0% expectations of an LLM doing a millennium problem anytime soon

auggierose5• 3 years ago

I don't think anything came out of the Netflix prize, did it?

anonylizard6• 3 years ago

I don't think the actual winning algorithm itself was used, because real world systems have more constraints/requirements than what the recommender was trained on. But that was in 2009, pre deep-learning/AI summer, and $1 mil clearly helped stimulate interest in that area.

Today we see multiple billion dollar recommender systems, like Tiktok. Netflix ironically benefits the least from recommenders due to the nature of its dataset (Very expensive, low sample size).

lern_too_spel• 3 years ago

Matrix factorization was popular in industrial recommender systems for years afterwards, and its ideas are still useful today. https://sifter.org/~simon/journal/20061211.html

rcpt2• 3 years ago

Netflix got enormous amounts of R and D for dirt cheap

dist-epoch• 3 years ago

What's his plan on being allowed to compete?

Or will he be doing it after the fact, when the questions are published.

lupire8• 3 years ago

After the fact.

jasfi• 3 years ago

I'm not sure if such a system would qualify, the prize specifically mentions a model that could solve specific types of problems.

I'm building something myself that I hope will be able to work similarly: https://aiconstrux.com

alecco3• 3 years ago

I wish there was a serious study of Dunning-Kruger effect in Silicon Valley.

larodi2• 3 years ago

your sense of humor is much appreciated. couldn't have said it better. hah :) basically i would suggest the study to expand to everyone doing anything titled AI at this moment.

eddtries8• 3 years ago

And HN!

queuebert3• 3 years ago

While I get your point and agree, there apparently is no Dunning-Kruger effect. It was determined to be yet another case of faulty data analysis in behavioral psych.[1]

1. https://economicsfromthetopdown.com/2022/04/08/the-dunning-k...

c7b• 3 years ago

I'm sure lots of people have been thinking/working along that direction. I think the idea of combining LLMs with formal verification/proof assistant tools (Lean, Coq, Isabelle,...) is particularly interesting. Anyone is aware of any major groups working on open source solutions for this?

tomatoadventure• 3 years ago

That sounds really cool, but I am having trouble finding any information about them to get in touch :(

mlengineerio• 3 years ago

Can you share the name of the startup? I'm also in Palo Alto and tinkering LLM for Match competition too (math.llmlab.io).

arcza• 3 years ago

Of course XTX is sponsoring this

rvz• 3 years ago

Great, a worthy competition which being first and correctness completely matter and may the best AI model win. Hopefully DeepMind doesn’t enter otherwise they would smoke everyone else other than OpenAI.

Speaking of which, I’ll give you a 1% chance of winning with this paper from OpenAI: [0] with the MATH dataset: [1]

EDIT: Why the downvotes? I'm trying to help you here and give you a starting point to win the competition? What's wrong with helping others?

[0] https://arxiv.org/abs/2305.20050

[1] https://github.com/hendrycks/math

daoboy2• 3 years ago

Anything you can do with a calculator is obviously trivial.

Is there a clear point of departure when AI can no longer handle mathematical reasoning?

edf132• 3 years ago

The IMO are a bit more involved...

e.g. IMO 2023:

Problem 1. Determine all composite integers n > 1 that satisfy the following property: if d1, d2, . . . , dk are all the positive divisors of n with 1 = d1 < d2 < · · · < dk = n, then di divides di+1 + di+2 for every 1 ⩽ i ⩽ k − 2

Although ChatGPT 4 makes a pretty decent start on this already:

To determine all composite integers $ n > 1 $ that satisfy the given property, we need to closely examine the condition set forth: for a composite number $ n $ with its divisors $ d_1, d_2, \ldots, d_k $ where $ 1 = d_1 < d_2 < \cdots < d_k = n $, the property $ d_i $ divides $ d_{i+1} + d_{i+2} $ must hold for every $ 1 \leq i \leq k - 2 $.

Let's break down the problem:

1. *Composite Number Requirement*: We are looking for composite numbers, which are integers greater than 1 that are not prime. These numbers have more than two distinct positive divisors.

2. *Divisor Property*: The property $ d_i | (d_{i+1} + d_{i+2}) $ means that $ d_{i+1} + d_{i+2} $ is a multiple of $ d_i $.

3. *Systematic Examination*: We will analyze this property systematically for composite numbers starting from the smallest composite number (4) and going upwards.

Let's start the analysis:

- For $ n = 4 $, the divisors are $ 1, 2, 4 $. Here, $ 1 | (2 + 4) $, so 4 satisfies the condition. - For $ n = 6 $, the divisors are $ 1, 2, 3, 6 $. Here, $ 1 | (2 + 3) $ and $ 2 | (3 + 6) $, so 6 satisfies the condition. - For $ n = 8 $, the divisors are $ 1, 2, 4, 8 $. Here, $ 1 | (2 + 4) $, but $ 2 \nmid (4 + 8) $, so 8 does not satisfy the condition.

Let's implement a systematic method to identify such composite numbers up to a reasonable limit (let's say up to 100 for a start) and check if they satisfy the given condition.

The composite integers greater than 1 and up to 100 that satisfy the given property are: 4, 8, 9, 16, 25, 27, 32, 49, 64, and 81.

Each of these numbers has the characteristic that for all their positive divisors $ d_1, d_2, \ldots, d_k $ (where $ 1 = d_1 < d_2 < \cdots < d_k = n $), the condition $ d_i $ divides $ d_{i+1} + d_{i+2} $ is true for every $ 1 \leq i \leq k - 2 $.

singularity20013• 3 years ago

Tangential is there a list of Unicode characters allowed on hacker news?

﷽!

magnio• 3 years ago

That's 300 words for saying "in order for n to satisfy the requirements, it must satisfy the requirements."

I tried an easier problem, extending Rolle's theorem to the multidimensional case with Poe.com:

Prompt: Let U be an open subset of R^n with compact closure K. Suppose f: K → R is continuous on K, differentiable on U, and satisfies f(x) = 0, for all x in K \ U. Show that there exists a in U with grad f (a) = 0.

Poe: To prove that there exists a point a in U such that grad f(a) = 0, we will utilize the concept of connectedness and the Mean Value Theorem.

Since U is an open subset of R^n with compact closure K, we know that K is a closed and bounded subset of R^n. Furthermore, since K is a compact set, it is also a connected set.

Now, let's define a new function g: K → R^n such that g(x) = (f(x), f(x), ..., f(x)) for all x in K. In other words, each component of g is equal to f(x) for all x in K.

Since f is continuous on K and differentiable on U (which is an open subset containing K), it follows that g is continuous on K and differentiable on U.

Consider the function h: K → R defined as h(x) = ||g(x)||^2 = f(x)^2 + f(x)^2 + ... + f(x)^2 = nf(x)^2.

Note that h is continuous on K since g is continuous on K and ||.||^2 is a continuous function.

Now, let's consider the set S = {x in K : f(x) = 0}. Since f(x) = 0 for all x in K \ U, we have K \ U ⊆ S. Therefore, the set S is closed.

...

Stochastic parrot indeed.

spi3• 3 years ago

A decent start? It says absolutely nothing about how to solve it, except repeating the question. The part where it tries out the few first numbers is entirely wrong, given that 6 does _not_ satisfy the condition (2 does not divide 3+6=9) and 8 _does_ (2 does divide 4+8=12).

Amusingly, the list of the integers <= 100 satisfying the property is correct, and it contradicts itself from the previous paragraph. Maybe if GPT wasn't a one-directional autoregressive model but allowed itself to go back and edit the past, it would have caught up that discrepancy and fixed it - but no such architecture currently exists that would run in decent amount of time.

Given that GPT4 is not a model but a full product, behind the scenes it probably coded up and ran a small python code that translated the problem into code, executed it and got its solution for the first few integers. Which would be a good thing to do to start solving a problem like this, except you're not allowed to do that at the IMO, obviously.

Looking at the output of this program, it suggests that powers of primes could be a class of solution (or maybe even the only solutions? I guess that's all the problem was _really_ asking to prove, but having never qualified for the IMO myself, I can't be sure). In fact, for n = p^k, the divisors are [1, p, p^2, ..., p^{k-1}, p^k], and clearly always p^i divides p^{i+1} + p^{i+2} = p^i (p + p^2). I guess this small remark would have gained me a point at the IMO, only 41 to go ;-)

But the other side of the coin is that having those numbers written down in front of you and not even making a conjecture about powers of prime being the answer would really denote poor mathematical reasoning by GPT4. It's only really proving that it can understand what it's being asked, which, I admit, places it in a better position than maybe 90% of the human population, but unfortunately for GPT4 mathematics is the least democratic science of them all - it's always only the top-1 result that matters in the end.

P.S. Being a former mathematician currently working on deep learning, having (or building!) a model that can solve mathematical questions has always been my dream. I'm not even talking about something that can _prove_ things, even just that can understand and rephrase them in different settings (which in mathematics is very, very hard, even for a human). Or spot weaknesses in already stated down proofs. As a graduate student, having something I could chat about to ask silly question while studying a paper would have been a real game changer. Even for best-of-world professionals it would be useful: when the wrong proof about the ABC conjecture came out, it took months of work from the best minds of our world to read through it and disprove it. If Mochizuki had had some tool for automatically checking his proof (and a smaller ego, I guess) he could have caught that early on, saved everybody a lot of work and the whole world some useless drama.

And while we're closer than ever to reaching that, I think GPT4 is still quite a far way from it. But with the pace we've seen recently in AI evolution, who knows...

Davidzheng14• 3 years ago

GPT-4+code is surprisingly good. https://chat.openai.com/share/ad42d09a-b366-4b21-b701-782fc8... "This observation leads to a hypothesis: only the powers of prime numbers satisfy the given condition. To verify this hypothesis, we need to consider why powers of primes might uniquely satisfy the divisibility condition and then prove or disprove it."

devit2• 3 years ago

In my first attempt at the problem it made this mistake:

"The condition fails for i=1 since 1 does not divide p+q unless p+q is a multiple of n, which is not generally true" (1 divides everything)

In the second it gives up:

"However, this conclusion is based on heuristic reasoning and examples"

Third attempt it makes this mistake:

"If the immediate next divisor, di+1 , is not a multiple of p (for instance, it could be q or a product involving q), then p does not divide di+1. Hence, p will not divide the sum di+1+di+2 in such a case, violating the condition." (the fact that p does not divide d_i+1 does not imply that it does not divide d_i+1, d_i+2)

Then it gives up again: "However, this conclusion is based on heuristic reasoning and examples"

Then it makes this basic logic mistake: "However, since p and q are distinct primes, p does not divide q, and it's not guaranteed that p divides q+d_i+2 , especially if d_i+2 is not a multiple of p. Therefore, for such n, the condition fails." (the fact that "it's not guaranteed" doesn't imply that it's false)

Overall it proves that prime powers have the property, conjures that non-prime-powers don't, proves that p*q doesn't have it, but completely fails at coming up with a proof strategy that proves that non-prime-powers don't have the property.

devit2• 3 years ago

It's problem solving (i.e. finding a proof of a statement or finding one or more mathematical objects that have some given properties and proving they have them and possibly that no other objects do), not computation.

daoboy2• 3 years ago

That distinction seems really obvious now that you said it. Thank you.

criddell• 3 years ago

Is there a clear point of departure when AI can no longer handle mathematical reasoning?

I'm more interested in the point where AIs are presenting proofs far beyond human capability. I'm imagining a day when an AI says it has solved some interesting problem and when we ask for the proof it spits out a 4 million page document. What are we supposed to do with that? What's the role of humans in that world?

lupire8• 3 years ago

Yet AI "models" ar terrible at calculation.

singularity20013• 3 years ago

Maybe the recently announced 1T Parameter Scientific AI will be trained on mathematical papers as well and picks up reasoning on the fly: https://news.ycombinator.com/item?id=38391923

Or at least maybe it will be a good foundation model to be fine-tuned for reasoning?

machiaweliczny• 3 years ago

Picks up reasoning on the fly seems like wishful thinking. On the other hand in nature there also is split into people who get math and those who don’t so maybe there are 2 different ways of bootstrapping brain to be functional and luck is all we need. Anyone knows more on this?

haltist6• 3 years ago

It's just a matter of scale because when you add more floating point numbers magical things happen. The magic is called emergence, as in if you have a big enough computer then it can do anything if you prompt it the right way. As a techno-optimist I believe that thinking is simply very complicated arithmetic and by adding enough numbers we can solve any problem.

73737373734• 3 years ago

It would be cool to have a Patreon-like system for math proofs. But to reward solvers appropriately and at scale, the award conditions and evaluation would have to be very formalized and specific.

This seems to be one potential, actually useful application of blockchains which support general purpose computing - if you can port a proof verifier onto them, you give anyone the ability to commit to (and claim) proof bounties.

Now, precisely formalizing specific conjectures and ensuring the proof system is expressive enough but doesn't allow for the introduction of any new assumptions is another problem...

xavxav• 3 years ago

A blockchain provides nothing of value here, what you need is a mechanized proof, and once you have that the blockchain in no way contributes to the trust.

The trust in a Coq proof comes down to "do you believe that the 8kloc kernel faithfully implements CiC+extensions and is this metatheory a sound type system?". As it is today, anyone could claim or commit a proof bounty by posting a Coq / Lean file / project online, all that's required is an email.

73737373734• 3 years ago

Sure, any centralized group, ideally a non-profit could run it just as well, and do so without potential complications arising from computation limits.

But they'd have to be entrusted with all the funds, and the financial side may be more difficult to implement. What could be a contract call would involve more real life logistics.

Not to imply that the points or whatever would have to represent anything more than kudos/bragging rights.

It would be interesting to see which problems have the most professional interest, say if every math PhD got 1 million points to commit.

eddtries8• 3 years ago

First person to submit a mechanised proof gets the payout to the address that submits the code? People can pool money into a pot? No one manages the funds individually and on a set date funds return to senders?

colesantiago2• 3 years ago

This seems to be one potential, actually useful application of blockchain...

No.

Blockchain and anything crypto has absolutely no use case at all other than speculation, please stop suggesting this solution in search of a problem.

pixel8account• 3 years ago

One: anonymous[1] method of payment online. Maybe this is not a problem you like, but your statement is trivially false.

[1] pseudonymous (in case of BTC) if we're being pedantic.

cottonseed• 3 years ago

I actually prototyped a system like this, mostly as an exercise to learn about crypto. You can't feasibly host or verify proofs on-chain, so you need external trusted verifiers (e.g. oracles). Making sure the oracles can't front-run proof submission is a challenge. Standard formal proof system (like Lean) are sufficiently expressive, although they weren't built for this and need to be modified to make sure a proof hasn't introduced any additional axioms, as you note. The proof system also becomes a point of attack, so you'd probably want multiple, independent verifiers (which themselves have been formally proved correct). I believe these exist for some proof systems, although I'm not sure about Lean's kernel.

Ultimately, I don't think this is really practical, and investing in AI proof agents is the way to go.

73737373734• 3 years ago

You can't feasibly host or verify proofs on-chain

I came to the same conclusion with existing systems, full on-chain verification would not be economically feasible.

But perhaps a special-purpose chain specifically made for this may not have the same limitations. Or Truebit-like oracle systems may be possible, where external verifiers can dispute other external verifier's assertions of correctness by running only the (potentially) wrong steps on-chain.

The frontrunning may be avoided by submitting hash(accountid | secret large random number | proof) first, then once that's finalized the full proof with the random number. The random number so the proof can't be brute forced from the hash. Payouts have some reasonable delay so if someone tries to frontrun the second step by intercepting the full proof and submits both steps (possibly with a varied proof) before the second step of the first person is finalized, the first person can still prove with a reference to their first step and their working proof that they were first. This still requires some thought regarding (forced) congestion in relation to the transaction cost and bounty size.

Metamath has the same problem of the system accepting new axioms anywhere, and the same $a statement being used for definitions. I have some hopes for Metamath Zero (https://github.com/digama0/mm0), which is a related system which may be able to fix this.

I think this idea is rather synergistic with proof agents. I think more people would consider developing these if enough bounties were credibly committed. It might speed up and greatly increase the number of formalized proofs.

kalverra• 3 years ago

Chainlink has solved this. Worth taking a look if you're still interested in this sort of thing.

baq• 3 years ago

I don't think you need the blockchain to post a verifiable, cryptographically signed proof of any theorem. A simple email is good enough for that.

Blockchains are append-only databases, sometimes (usually?) with 'slow' thrown in somewhere.

eddtries8• 3 years ago

That’s an app on top of the append only DB with some logic that either requires IRL groups to manage it, or a blockchain contract. I prefer the latter tbh!

byteware• 3 years ago

talking as someone who is building such a system, why would an avarage participant of the network give their own money, i dont think they would for the same reason i'm not running a bounty program with my dollars, the only use of having it on the blockchain is rewards without using your own money (so it's economics depends on the eventual value of the coin), for that it has to be bound to the minting process, but a purely algorithmic system for determining who gets how much based on their proofs seems elusive (think of the infinite possible proofs 1+2=3, 1+3=4...), we are going for having a central authority doing the minting for proofs (as voting based on money would hardly reflect mathematical experties)

73737373734• 3 years ago

I'd like to personally put 5-10 bucks toward the solution of the Collatz conjecture, just for fun (and to see machine learning people grind their GPU-teeth on it).

No idea about the minting process, there seems to be an infinitude of possibilities.

andyjohnson03• 3 years ago

As the parent of a young adult currently half way through their maths undergrad, this kind of fills me with foreboding.

I know that proof assistants etc have existed for quite a while now, but what with this and the murmours about OAI's Q* model, I do wonder what will happen to maths as a human endeavour - and as a enabling skill for jobs that can financially support people like my child.

adhocmobility• 3 years ago

I think its pretty clear that in the coming decade intelligence and cognitive labor is going to become very cheap. So your kid should develop some skills outside of that to stay competitive in the job market.

nickfromseattle• 3 years ago

Any suggestions?

RugnirViking• 3 years ago

general intelligence will become cheap? and so your suggestion is to develop skills outside of skills?

Davidzheng14• 3 years ago

Personally i think markets will be so different from now that this question of where you'll have skills for jobs is less important than asking what will a job mean in 2040. But ok, maybe this is still a minority opinion.

skepticATX• 3 years ago

I think it's pretty clear that cognitive labor will become even higher value in the future, as our tools get better and allow us to become more productive.

Der_Einzige4• 3 years ago

You speak the truth but people here will hate you for it.

auggierose5• 3 years ago

I wouldn't worry. What this means is that mathematics as a skill is going to be back big time, because now you can actually use it everywhere.

Mathematics departments have been closing down for a while now, I think. I think this trend will reverse now. Mathematics itself will change in the process, but for the better.

anonylizard6• 3 years ago

This. Math proofs are useless in 99.99% of situations because they are far too expensive to actually use in production. Only something like AWS would use formal proofs to verify some system property for reliability.

With some super-math Q* bot, a mathematician could presumably create actual proofs/simplifications for complex real world problems/systems at very affordable time and costs (in weeks not years).

The mathematician in this case is far less skilled than the bot, but that doesn't detract from their market value. Most programmers are way less skilled/smart than the library authors that they rely on, that doesn't stop them from earning $$$, because they are useful.

Davidzheng14• 3 years ago

I don't think it's true that "math departments have been closing for a while now"

slibhb• 3 years ago

I wouldn't worry about it. We're going to need humans with specialized mathematical training in the loop.

Besides, these things have a way of surprising us. Before compilers, people wrote machine code by hand. It would have been reasonable to think that compilers would reduce the demand for programmers, but the opposite happened.

Davidzheng14• 3 years ago

It's highly unclear to me what will happen. Probably learning math will be more accessible. But it's unclear how many humans will be involved at the forefront of math research. For example you can imagine a situation where in some parts of math large communities work in a direction guided by a few "visionaries". This sort of thing will not really happen after the commodization of theorem provers. Like instead of an advisor telling a PhD student a problem, they can just plug it in. On the other hand, in some sense the advisor and the student will be equal in the fact that the only thing you will need to do is ask questions?(last part is also speculative)

margorczynski• 3 years ago

Besides, these things have a way of surprising us. Before compilers, people wrote machine code by hand. It would have been reasonable to think that compilers would reduce the demand for programmers, but the opposite happened.

I see this reasoning a lot but for me it kinda screams "correlation is not causation". As time passed and technology advanced it was simply more widely used, both on a consumer and business level. Very well may be that if we had to write machine code by hand we would need 10x more developers and a salary of $1kk/year would be average at best.

Do you really think if we get some AI agent that can write a wholly working application based on natural language specification that wouldn't significantly reduce the need for human devs?

pixl972• 3 years ago

There isn’t a rule of economics that says better technology makes more, better jobs for horses. It sounds shockingly dumb to even say that out loud, but swap horses for humans and suddenly people think it sounds about right.

andyjohnson03• 3 years ago

Before compilers, people wrote machine code by hand. It would have been reasonable to think that compilers would reduce the demand for programmers, but the opposite happened.

That analogy occurred to me too. But I'm not sure what the corresponding higher-level domain is that mathematicians might have to migrate to - in the way that assembly programmers started using high level languages. Writing prompts for maths LLMs, or wrangling teams of them, is hardly going to be well paid enough to facilitate a decent life in this era of late capitalism, or even pay uni fees.

And even if there are such higher-level domains, its not certain that they are compatable with available human cognitive ability or limits.

Lots of maths grads currently go into tech/finance/lifescience/whatever. I'm a dev and I can see those fields being eaten alive by this stuff. I don't want my kid to end up as a 2030-equivalent of a fully qualified assembly language programmer.

tomp• 3 years ago

You do realize that we still learn (and not unnecessarily) addition despite having had calculators for 50+ years?

Math shapes your mind, that’s why we learn it.

daxfohl3• 3 years ago

In a way, all math proofs already exist. Humans just have to determine what is worth looking for and uncover them. AI will help us do the latter. But we still have to do the former ourselves.

It will still require sound mathematical knowledge and understanding, to know what are the interesting questions to ask. Even if AI knows all the answers, it doesn't change anything because the answers already exist anyway.

andyjohnson03• 3 years ago

That kind of Platonism also implies that all possible computer programs already exist: because any program is merely a very large natural number, the set of which has infinite cardinality. I'm not sure how helpful this is for the practice of humans doing mathematics or software development though.

BeetleB2• 3 years ago

I hate to break it to you but most people with math degrees aren't doing math jobs today. The demand for such skills is low. While such an AI may displace some of the few jobs that do involve heavy math, it's likely your child will not be in that category.

I wouldn't worry too much.

dxbydt2• 3 years ago

Perhaps this might cheer you up - https://statmodeling.stat.columbia.edu/2015/03/17/1980-math-...

Or perhaps not. In that blog, Gelman speaks of Gregg, who ended up as a GS VP, and says -

math olympiad = high school basketball star

pro mathematician = NBA player

Goldman Sachs VP = sports hustler

I actually worked with Gregg in fixed income at that time :) Gelman's blogpost received sufficient notoriety, atleast within GS & the IB community.

EVa5I7bHFq9mnYK5• 3 years ago

Yet GS VPs salary is closer to NBA player's salary, while math pro's salary is closer to sports hustlers' ...

svat2• 3 years ago

How does this relate to the "IMO Grand Challenge" https://imo-grand-challenge.github.io/ ? Is this a new name / formalization, with prize money attached, or is it entirely independent? (E.g. I see Kevin Buzzard and Leonardo de Moura listed on both that page and at https://aimoprize.com/supporters)

dwrensha4• 3 years ago

The IMO Grand Challenge is "formal to formal" -- a solver is given the problem specified in the Lean programming language, and must produce a solution in Lean. To see more concretely what this setup might look like, check out https://github.com/dwrensha/compfiles.

The AI MO prize is "informal to informal" -- a solver is given a problem in natural language and must produce a solution in natural language.

My belief is that the best way to get to "informal to informal" is to first solve "formal to formal", but not everyone thinks so.

lupire8• 3 years ago

"Informal to formal" is harder than "formal to formal". These puzzle problems are quite simple (for computers) if you have a formalization.

"Informal to informal" is so far snake oil.

svat2• 3 years ago

Answering my own question: Alex Gerko (who's behind the $10M prize here) says:

"It came about as me checking on the status of IMO Grand Challenge (which was launched in 2019 https://imo-grand-challenge.github.io) and deciding that it's time to give this idea a boost"

https://twitter.com/AlexanderGerko/status/172920793662562733...

dwrensha4• 3 years ago

$5mn will be awarded to the first publicly-shared AI model

Thank for you the emphasis on openness!

haltist6• 3 years ago

We will solve math with math and this project will succeed as foretold by prophets of techno-optimism like Marc Andreesen, Elon Musk, and Bill Gates. All we need is the right architecture, aka mathematical formula for giving all of math a smooth manifold structure. How this works for discrete structures like integers is left as an exercise for the reader and future AI which will figure out how to improve themselves and deal with discrete and non-smooth mathematical problems.

I can win this challenge by the way for $80B. I already know what architecture is required to solve math with math but I need the money to buy the GPUs. You might think such a recursive application of math is logically circular but it is not and all I need is $80B to prove it (pun intended).

Claude did not like this comment at all, ironically: I do not have enough context to fully evaluate those claims or determine if that approach would work. Solving all of mathematics is an extraordinarily ambitious goal that would require fundamental theoretical advances we do not yet possess. While future AI systems may someday make significant progress on longstanding mathematical problems, making definitive claims about solutions requires rigorous mathematical proof and analysis beyond optimistic speculation. I'd encourage focusing discussion on specific mathematical questions or areas of research rather than making broad, unsupported assertions about solving all of mathematics.

WhitneyLand5• 3 years ago

Winning a gold medal here will really be a leap forward for AI creativity and deep insight into problem solving.

AI already is already contributing in substantial ways to research.

What’s tantalizing here is this next level would take a huge step toward accelerating the pace of advancements in many fields.

It will be a milestone in moving past AI being a mere tool in scientific progress to something much greater.

haltist6• 3 years ago

I sense you are a techno-optimist.

WhitneyLand5• 3 years ago

Maybe somewhat, but is anything I said that much of a leap?

Do you consider AI to have already considered substantially to the advancement of science?

For example AlphaFold, Weather forecasting, Algorithm optimization, etc

Der_Einzige4• 3 years ago

Techno optimism is good and should be the default. I wish a16z didn’t ruin that phrase. Techno optimism should evoke Star Trek, not Silicon Valley vibes

Yhippa2• 3 years ago

I'm asking this question out of ignorance: if you were able to do this, why would you make it public for $10MM instead of keeping it private and exploiting it. Say, in algorithmic trading models?

nathanfig• 3 years ago

Some private enterprises would undoubtedly ignore this prize, but a lot of academic researchers (including students) would be more than motivated by this prize.

falcor846• 3 years ago

I'm answering this out of naivete: some people want to benefit humankind over their personal interests.

thomastjeffery• 3 years ago

In that case, why would you be motivated by a $10m prize?

BeetleB2• 3 years ago

I see no reason to believe such a machine would be helpful for algorithmic trading. Why should it?

How well do current gold medalists do in trading?

eddtries8• 3 years ago

Alameda Research had some gold medalists iirc!

Yhippa2• 3 years ago

I was curious as to why an algorithmic trading firm is sponsoring this. What's in it for them?

fooker• 3 years ago

Two reasons: (1) These are two different problems. Human mathematicians tend to be good at both, but there's no reason to believe (yet) that this generalization can be achieved with software.

(2) Trading has second order effects, no matter how good your algorithm is, if you apply it at any kind of scale the market reacts to it and you are left with something that doesn't work or cause large losses in the worst case.

logicchains• 3 years ago

Say, in algorithmic trading models

Higher level math is nothing like the math used in trading algorithms. It wouldn't be any more useful than a top tier PHD graduate.

WhitneyLand5• 3 years ago

Before gold at the math Olympiad, it would be nice if GPT 4 could merely evaluate an expression like this into an exact solution :

3 + 1 / (3 + 1 / (3 + 1/3))

dmd3• 3 years ago

Works for me... https://cloud.typingmind.com/share/29d28743-b6a7-4716-b1aa-a...

WhitneyLand5• 3 years ago

That’s helpful thank you.

Would you mind trying it 4 times and tell how many succeed?

I see it work occasionally but seems <= 50% success rate.

See here: https://chat.openai.com/share/6da22a7b-b8f8-4611-b5f7-38048f...

seafoam• 3 years ago

Is XTX good for the $10M ?

There are a lot of people who got burnt by FTX grants and prizes ...

eb2• 3 years ago

Yes, Alex Gerko is the UKs biggest tax payer and regularly donates to schools/universities math departments

alecco3• 3 years ago

Very cool of XTX. They are a solid company with very smart people.

But wouldn't a model capable of doing this be currently worth hundreds of millions? A billion?

ackbar03• 3 years ago

That's why they only offer 10 million.

If you want, you can offer 100mio, I'll join your competition instead

daxfohl3• 3 years ago

I'd still call this fancy autocomplete. I imagine the jump from this, to "come up with an interesting new branch of math to explore", is a long way off.

ak_111• 3 years ago

I totally disagree. I think it is more likely we will have quantum chips running your iphone before this prize gets cashed (and I am a bit of a quantum computing sceptic).

For comparison, even field medalists sometime struggle with getting gold medal in the time allocated or identify the trick needed in solving an IMO question.

The difficulty difference between solving an IMO level 6 problem and solving an open math problem is much smaller than most imagine.

killerstorm• 3 years ago

By that definition 99.99% people are also fancy autocomplete.

How many people you know who came up with an interesting new branch of math?

daxfohl3• 3 years ago

Yeah I don't disagree with this. But such people do exist. My expectation is that IMO gold is a couple years off. But inventing new math and explaining why it's interesting and useful is much much farther away.

I can't decide whether I hope I'm wrong or not.

esafak• 3 years ago

Fancy autocomplete is made possible by understanding.

Can you imagine correctly autocompleting a proof to a Millennium Prize problem any other way?

dooglius• 3 years ago

Seems better to go by AIME-style scoring (explicit 3-digit number answer) otherwise there's the question of whether an AI really solved the problem or just bullshitted enough relevant keywords to get partial credit.

quirino2• 3 years ago

IMO is competitive enough you can't bullshit your way to a gold medal

openquery• 3 years ago

Can automated theorem provers solve mathematical olympiad problems in a reasonable time given enough compute?

LLMs are quite good at generating semantically correct language. I remember reading a paper about extending the planning capabilities of GPT-4 by using a Planning Domain Definition Language [0]. By that same logic could an LLM not translate the olympiad problem into a form suitable for a theorem prover?

[0] https://arxiv.org/pdf/2305.11014.pdf

lacker2• 3 years ago

No, IMO problems are much too hard for the current generation of theorem provers.

govg2• 3 years ago

https://imo-grand-challenge.github.io/

This is a similar contest where the plan is exactly as you describe - to develop a way to solve formal descriptions in Lean of IMO problem.

amai2• 3 years ago

Just combine GPT-4 and Wolfram Alpha?

queuebert3• 3 years ago

Wow, that website has an extremely irritating background animation. Any time your mouse is inside a circle, the circle lights up, stealing your mental focus from the text.

Reminds me of the really dumb new Glassdoor design, where it flickers in the background as if it's loading something (but it's not) while you're trying to fill out the sign up form.

What is going on with web development these days? Is it some kind of Javascript animation version of the IOCCC?

lupire8• 3 years ago

This is an embarrassing overreach.

We don't even have models that can win the far easier AMC, let alone AIME, USAMO, and then IMO.

mathteddybear• 3 years ago

They don't need to win IMO, they need to get a gold medal. I got a gold medal at IMO solving 4 out of 6 problems

I don't want to speculate, but it's not inconceivable that this will be achieved by AI within the future lifetime of XTX

nojvek• 3 years ago

What is AMC AIME, USAMO ?

supernewton• 3 years ago

They're the feeder contests in the U.S. that determine who gets to represent the U.S. in the IMO.

AMC = multiple choice test, open to all grade school students.

AIME = open response test, all answers are numerical, open to students who score high enough on AMC only.

USAMO = USA Math Olympiad. IMO-style proof problems. Open only to top N scorers on AMC and AIME.

lacker2• 3 years ago

Well there's a $1m prize for the Riemann hypothesis. Now this is bigger. Which do you think will fall first?

oglop• 3 years ago

That’s, interesting I think. I’m not sure wha true domain of problems are in that arena. I’ve found great success using LLMs for teaching abstract algebra but have noticed when I switch to analysis or topology things get more wonky.

My advice, and I have zero understanding or care why the above happens, is to lean into algebra and train less on analysis. You’ll get there faster it seems.

shannifin• 3 years ago

Assuming one succeeded, would it be more financially lucrative to claim the prize or form a startup with it?

userforcomment• 3 years ago

Great marketing stunt, nice work by XTX HR!

amai2• 3 years ago

Just combine GPT-4 and Wolfram Alpha?

See https://arxiv.org/abs/2308.05713

EVa5I7bHFq9mnYK5• 3 years ago

Such a system would have a market value on $10billions++, nice try trying to get it for 1/1000 the price.

Imnimo• 3 years ago

It feels like 10M is a fraction of what it would cost to train such a model. Even if we assume an eventual winner would be willing to release the model and forgo potential profits, does this prize really motivate development if it doesn't even cover costs?

supergirl• 3 years ago

not sure there is much point to this. currently no model is even at the level of primary school math. it will take decades until it can win a gold medal in maths. it won't happen overnight. it will happen slowly. will they still give out the prize in 20 years from now, when it won't seem like such a breakthrough?

up2isomorphism• 3 years ago

What is fundamentally different about solving IMO compared to solve any other math problems in AI sense?

$10M AI Mathematical Olympiad Prize

Related Stories