IMO challenge bet with Eliezer

I bet the market down from 58% to 40% which seems like a steal on the merits. Seems like it will mostly lock up my money though given the long resolution timeline, unless people eventually settle down to a significantly lower consensus.

I'd be happy to do bet about fast growth prior to end of world. I'd say something like:

> 25% chance that there are 4 consecutive years before 2045 with >10% real economic growth per year, under an accounting scheme that feels plausible/real to Eliezer and Paul, and the fast growth sure feels to Paul and Eliezer like it's about automation rather than some weird thing like recovery from a pandemic.

You would win when the end of the world looks close enough that we can't get 4 years of progress (e.g. if we have 50% growth in one year with <10% progress in the year before, or if it becomes clear enough that we won't have time for rapid growth before the AI-R&D-AI gets us to a singularity). It's kind of unsatisfying not to pay out until right before the end with kind of arbitrary conditions (since it's so hard for you to actually win before 2045 unless the world ends).

I would give you higher probabilities if we relax 2045, but then it just gets even harder for you to win. Probably there is some better operationalization which I'm open to. Maybe a higher threshold than 10% growth for 4 years is better, but my probabilities will start to decline and I'd guess we get more expected info from disagreements about higher probability events.

(I don't know what kind of programmer Mike Blume is but don't expect to ever have many $10M+ programmers. Likewise, I don't think we have $10T spent training a single AI model until after we've already faced down alignment risk, and I assume that you also thinks that society will eventually use >>$10T of resources on training a single ML model. I would have thought we could also bet about softer versions of those things---I assume I also assign much higher probability than you do $1B training runs even if it's not worldview-falsifying, I don't think worldviews usually get falsified so much as modestly undermined.)

Yeah, this may well be right. I agree that IMO 2015 problem 3 can be solved by machine. I think both the geometry and 3 variable inequalities could be a very big problem (in that lots of instances are easy for machines and hard for humans). Some diophantine equations and functional equations are also very easy for machine. By 2022 my vague understanding is that the committee is much less likely to put that kind of question in the hardest slot since increasingly many contestants can basically do the machine-like proofs. But I maybe shouldn't count on that, since the big problem is that we are letting it win at any of 4 IMOs (2022, 2023, 2024, 2025).

I'd guess we have like a 2-3% chance of 3-variable inequality in hardest spot (hasn't happened in last 20 years and is getting  less likely, but not that confident).  By now I think it would be considered unreasonable to put a muirhead bashable problem as 3/6 (though even the other 3 variable inequalities will likely be much easier for machines than humans), even in 2005 I think that was probably considered a mistake. But still lots of these may be easy for machines, so you may easily be looking at like 10% chance of one of them being a 3-variable inequality and a 50% chance of solving it conditioned on a serious effort which would already be >4%.

Other candidate definitions would have been:

• Instead of just using the type of problem, try to explicitly flag constant-number-variables inequalities or diophantine equations or functional equations as special cases to be ranked lower.
• Have a stronger preference for combo, e.g. pick from amongst 3/6 (or even 2/3/5/6) with preference for combo then NT then algebra than geo. (But I'm scared of e.g. combo 2/5 that can be solved with easy monovariant or that kind of thing, I strongly suspect many of those are also automatically solvable without deep learning.)
• Actually ask someone who doesn't yet know the results of running a machine which problem seems hardest for machine.

I also agree that "special case of existing result" is plausible, but I think that's going to be <1% (and it's fairly likely to be missed by machines even so). Though that could get worse if many more formal proofs are added in the interim as part of increased investment in theorem proving which could drive that up, and that's very correlated with a serious effort that could effectively exploit such data.

If Eliezer wants to actually bet about the hardest problem claim I may want to argue for some kind of reformulation (even though I said I didn't want to change my predictions). If Eliezer doesn't want to bet about it, I think it's OK to ding me epistemically if the AI ends up getting a "hardest problem" that is a 3 variable inequality or bashable functional or diophantine equation, though I think it's a bit of a technicality / a general error in my forecasting rather than a claim about AI.

These numbers come from if each party were actually in a mixture of experts, or equivalently Kelly-betting their epistemic credit points on a prediction market. We might update less due to some combination of

• other evidence we have about Paul and Eliezer is not independent with this
• The bet is between Paul thinking for a few hours, and Eliezer thinking for a few hours. But what we really want to decide between is Paul's model being right vs Eliezer's model being right, and the bet is not perfect evidence of that.

I don't really think we have particularly careful views; it would be reasonable to not update very much.

ETA: I moved that text to a footnote since I basically agree that it's unreasonable as a prescription.

I believe most people who work in deep learning (but don't have inside evidence about particular theorem-proving efforts currently underway) are on Eliezer's side and would go even higher than 16%.

In the broader world I think probably it's more divided, and I'd guess that most academics in AI would be on my side though I'm not sure.

This is definitely a thing that makes me uneasy about the bet (I would have loved for Eliezer to be the one with the more contrarian take, and for my position to be closer to 50-50, but you get what you get).

I think this is quite plausible. Also see toner's comment [LW(p) · GW(p)] in the other direction though. Both probabilities are somewhat high because there are lots of easy IMO problems. Like you, I think "hardest problem" is quite a bit harder than a gold, though it seems you think the gap is larger (and most likely it sounds like you put a much higher probability on an IMO gold overall).

Overall I think that AI can solve most geometry problems and 3-variable inequalities for free, and many functional equations and diophantine equations seem easy. And I think the easiest problems are also likely to be soluble. In some years this might let it get a gold (e.g. 2015 is a good year), but typically I think it's still going to be left with problems that are out of reach.

I would put a lower probability for "hardest problem" if we were actually able to hand-pick a really hard problem; the main risk is that sometimes the hardest problem defined in this way will also be bashable for one reason or another.

Having posted this and emailed Eliezer, I'm now considering his prediction as 16% flat. So that's 1 bit of epistemic credit for him if it happens 1/8th of a bit for me if it doesn't.

I'm curious if you can explicate the thought process behind such a high estimate.