bets

I'm generally against recreational gambling, but interested in bets as a tool for collective epistemics. I've avoided manifold.markets for confidentiality and attention-conservation reasons, but I'm fairly active on a private play-money prediction market at work. Long Bets are also pretty cool.

This page records some public bets I've made, in the spirit that a bet is a tax on bullshit:

Against feasibility of Guaranteed Safe AI projects

I offered several open bets related to the feasibility of proposals in the Provably Safe AI: Worldview and Projects post, including:

• That proposal (3), involving a semantic library for probabilistic programming and machine learning, won't happen with nontrivial bounds due to difficulties in modeling nondeterministic GPUs and varying floating-point formats.
• That proposal (8), involving a provably unpickable mechanical lock, won't be attempted or will fail at some combination of design, manufacture, or just being pickable.
• On a mutually agreed operationalization against the success of other listed ideas with a physical component.

Ben Goldhaber accepted the bet on the provably unpickable mechanical lock. To summarize the terms:

• I win if, by end of 2026, there's no formally-verified design, or it doesn't verify unpickability, or fewer than three physical instances are made.
• Ben wins if, by end of 2027, there have been credible failed expert attempts to pick such a lock (e.g., at Defcon).
• I win if there's a successful picking attempt.
• The lock should have at least a thousand distinct, non-pickable keys, with the design available in advance to potential pickers.

Against formal verification on large language models

This comment lays out my belief that formal verification of large models is infeasible. As well as offering open bets, I announced a $1,000 prize for solving the following problem before 2023:

Take an EfficientNet model with ≥99% accuracy on MNIST digit classification. What is the largest possible change in the probability assigned to some class between two images, which differ only in the least significant bit of a single pixel? Prove your answer.

The proof must not include executing the model or equivalent computations (e.g. concolic execution). Participants may train a custom model and/or directly set model weights, as long as it uses a standard EfficientNet architecture and reaches 99% accuracy. I'd award half the prize for a non-trivial bound.

Buck and Maxwell each proposed some ideas for how a proof might work, but ultimately the prize went unclaimed and nobody took me up on the offer to bet.

This challenge aims to demonstrate the difficulty of rigorously proving even trivial global bounds on the behavior of large learned models. I believe this is and will remain infeasible for reasons discussed in that comment thread, and that even if we could prove such bounds this would be unlikely to help with the alignment problem or other AI risks.

Against massive Fortune 500 market cap decline

lukehmiles predicted that "almost all [investors'] investments go to zero except for a few corps lead by absolute sharks." We operationalized this as: the inflation-adjusted market cap of the bottom 50% of the Fortune 500 (as of Jan 1st 2024) will decline by 80% or more by Jan 1st 2034.

I'm betting against this outcome. If I win, lukehmiles will donate $50 to GiveWell's all-grants fund. If I lose, I'll pay $50 to lukehmiles or their charity of choice.

Against value of Ethicophysics to Yudkowsky

MadHatter bet that Eliezer Yudkowsky will find their work on ethicophysics valuable by December 1st, 2024. Resolution criteria are to ask EY "which of Zac or MadHatter won this bet?", with no payment if he declines to respond.

back to homepage.