Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

$10M AI Mathematical Olympiad Prize

aimoprize.com

Post reply on HN
Print view View original

141–150 of 231 posts

Re: $10M AI Mathematical Olympiad Prize

#141

Post by lupire »

dist-epoch wrote: post #31
gregdoesit wrote: post #2

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…

What's his plan on being allowed to compete? Or will he be doing it after the fact, when the questions are published.

After the fact.

Re: $10M AI Mathematical Olympiad Prize

#142

Post by jacobr1 »

anonylizard wrote: post #30
auggierose wrote: post #26

Earlier quoted context omitted.

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

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 o…

My understanding was that their research on what drove engagement shifted quite a bit. Things like social proof, and product patterns like auto-loading the next episode to binge drove engagement metrics. Recently there were some articles about their team custom-identifying which cuts of a video to show as a trailer maximized engagement on a personal level. In some sense that is a recommendation, but it is a broader problem space.

Re: $10M AI Mathematical Olympiad Prize

#143

Post by lupire »

queuebert wrote: post #139
alecco wrote: post #86

Earlier quoted context omitted.

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

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

That paper was thoroughly rebutted when posted to HN.

But Gwern has written about some earlier debunkings of the D-K effect, ad furthermore D-K was never about the popular misconception of D-K ("incompetent people think they are more competent than competent people").

Re: $10M AI Mathematical Olympiad Prize

#144

Post by queuebert »

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?

Re: $10M AI Mathematical Olympiad Prize

#145

Post by lupire »

dwrensha wrote: post #45
svat wrote: post #21

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 )

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…

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

Re: $10M AI Mathematical Olympiad Prize

#146

Post by lupire »

eddtries wrote: post #131
BeetleB wrote: post #109

Earlier quoted context omitted.

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?

Alameda Research had some gold medalists iirc!

Yes, but they stopped doing math puzzles when they started trading. Math puzzles aren't how they trade.

Re: $10M AI Mathematical Olympiad Prize

#147

Post by dwrensha »

lupire wrote: post #145
dwrensha wrote: post #45

Earlier quoted context omitted.

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…

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

> These puzzle problems are quite simple (for computers) if you have a formalization.

That may be true someday, but it's not yet! That's exactly what the IMO Grand Challenge is about, and nobody has gotten close to solving it.

Re: $10M AI Mathematical Olympiad Prize

#149

Post by 7373737373 »

byteware wrote: post #119
7373737373 wrote: post #11

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 bou…

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 p…

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.

Re: $10M AI Mathematical Olympiad Prize

#150

Post by Der_Einzige »

larodi wrote: post #91
anonylizard wrote: post #59

Earlier quoted context omitted.

Fingers are already mostly solved. The latest models draw hands better than most human artists. I think artists would disagree with your assessment of 'approximate pattern recognition'. Its more like： 1. Given a set of words describing what the user wants. 2. Arrange pixels in a grid 3. That maximizes the user rating On one hand it is tolerant of small errors. On the other hand its an extremely broad problem. Also to…

Well this thing about fingers, etc in drawings. Lets put it this way - for us mere mortals the generative images look very much okay. To artists and people who actually draw something, well ... they very often spot inconsistencies in the whole production, including how fingers, arms, overall body posture, etc is presented. So it is exactly what we can expect - good enough on average, but actually a mediocre result of…

Using controlnet fixes all of these problems and makes it where even real artists won’t be able to tell AI art apart from real art.
Post reply on HN