For anyone wanting to harness AI models to create formally verified proofs for theoretical alignment, it looks like last call for formalizing question statements.

Game theory is almost completely absent from mathlib4. I found some scattered attempts at formalization in Lean online but nothing comprehensive. This feels like a massive oversight to me -- if o12345 were released tomorrow with perfect reasoning ability then I'd have no framework with which to check its proofs of any of my current research questions.

So I've been thinking a little more about the real-world-incentives problem, and I still suspect that there are situations in which rules won't solve this. Suppose there's a prediction market question with a real-world outcome tied to the resulting market probability (i.e. a relevant actor says "I will do XYZ if the prediction market says ABC"). Let's say the prediction market participants' objective functions are of the form play_money_reward + real_world_outcome_reward. If there are just a couple people for whom real_world_outcome_reward is at least as significant as play_money_reward and if you can reliably identify those people (i.e. if you can reliably identify the people with a meaningful conflict of interest), then you can create rules preventing those people from betting on the prediction market.

However, I think that there are some questions where the number of people with real-world incentives is large and/or it's difficult to identify those people with rules. For example, suppose a sports team is trying to determine whether to hire a star player and they create a prediction market for whether the star athlete will achieve X performance if hired. There could be millions of fans of that athlete all over the world who would be willing to waste a little prediction market money to see that player get hired. It's difficult to predict who those people are without massive privacy violations -- in particular, they have no publicly verifiable connection to the entities named in the prediction market. 

Awesome post!

I have absolutely no experience with prediction markets, but I’m instinctively nervous about incentives here. Maybe the real-world incentives of market participants could be greater than the play-money incentives? For example, if you’re trying to select people to represent your country at an international competition and the potential competitors have invested their lives into being on that international team and those potential competitors can sign up as market participants (maybe anonymously), then I could very easily imagine those people sabotaging their competitors’ markets and boosting their own with no regard for their post-selection in-market prediction winnings.

For personal stuff (friendship / dating), I have some additional concerns. Suppose person A is open for dating and person B really wants to date them. By punting the decision-making process to the public, person A restricts themselves to working with publicly available information about person B and simultaneously person B is put under pressure to publicly reveal all relevant information. I can imagine a lot of Goodharting on the part of person B. Also, if it was revealed that person C bet against A and B dating and person B found out, I can imagine some … uh … lasting negative emotions between B and C. That possibility could also mess with person C’s incentives. In other words, the market participants with the closest knowledge of A and B also have the most to lose by A and B being upset with their bets and thus face the most misaligned incentives. (Note: I also dislike dating apps and lots of people use those so I’m probably biased here.)

Finally, I can imagine circumstances where publicly revealing probabilities of things can cause negative externalities, especially on mental health. For example, colleges often don’t reveal students’ exact percentage scores on classes even if employers would be interested — the amount of stress that would induce on the student body could result in worse learning outcomes overall. In an example you listed, with therapists/patients, I feel like it might not be great to have someone suffering from anxiety watch their percentage chance of getting an appointment go up and down.

But for circumstances with low stakes (so play money incentives beat real-world incentives) and small negative externalities, such as gym partners, I could imagine this kind of system working really well! Super cool!

I like these observations! As for your last point about ranges and bounds, I'm actually moving towards relaxing those in future posts: basically I want to look at the tree case where you have more than one variable feeding into each node and I want to argue that even if the conditional probabilities are all 0's and 1's (so we don't get any hard bounds with arguments like the one I present here) there can still be strong concentration towards one answer.

Wow, this is exactly what I was looking for! Thank you so much!

I also suspect that the evaluation mechanism is going to be very important. I can think of philosophical debates whose resolution could change the impact of an "artifact" by many orders of magnitude. If possible I think it could be good to have several different metrics (corresponding to different objective functions) by which to grade these artifacts. That way you can give donors different scores depending on which metrics you want to look at. For example, you might want different scores for x-risk minimization, s-risk minimization, etc. That still leaves the "[optimize for (early, reliable) evidence of impact] != [optimize for impact]" issue open, of course. 

I really like this perspective! Great first post!

Okay that paper doesn't seem like what I was thinking of either but it references this paper which does seem to be on-topic: https://research.rug.nl/en/publications/justification-by-an-infinity-of-conditional-probabilities 

Thanks for the response! I took a look at the paper you linked to; I'm pretty sure I'm not talking about combinatorial explosion. Combinatorial explosion seems to be an issue when solving problems that are mathematically well-defined but computationally intractable in practice; in my case it's not even clear that these objects are mathematically well-defined to begin with.

The paper https://www.researchgate.net/publication/335525907_The_infinite_epistemic_regress_problem_has_no_unique_solution initially looks related to what I'm thinking, but I haven't looked at it in depth yet.

Hmmm, I’m still thinking about this. I’m kinda unconvinced that you even need an algorithm-heavy approach here. Let’s say that you want to apply logit, add some small amount of noise, apply logistic, then score. Consider the function on R^n defined as (score function) composed with (coordinate-wise logistic function). We care about the expected value of this function with respect to the probability measure induced by our noise. For very small noise, you can approximate this function by its power series expansion. For example, if we’re adding iid Gaussian noise, then look at the second order approximation. Then in the limit as the standard deviation of the noise goes to zero, the expected value of the change is some constant (something something Gaussian integral) times the Laplacian of our function on R^n times the square of the standard deviation. Thus the Laplacian is very related to this precision we care about (it basically determines it for small noise). For most reasonable scoring functions, the Laplacian should have a closed-form solution. I think that gets you out of having to simulate anything. Let me know if I messed anything up! Cheers!