Problem 14: An explicit bound
Blogger Gwern has recently posted about Lean. In honor of this, here is some analysis this other post of his about the fourteenth problem from a list of quant interview questions.
You have 52 playing cards (26 red, 26 black). You draw cards one by one. A red card pays you a dollar. A black one fines you a dollar. You can stop any time you want. Cards are not returned to the deck after being drawn. What is the optimal stopping rule in terms of maximizing expected payoff?
Also, what is the expected payoff following this optimal rule?
I am particularly interested in this comment from Gwern’s post:
If you look at the spreadsheet solution, the whole bottom left of the spreadsheet is simple: if you know you should stop when there are x good cards and y bad cards remaining, you don’t need to do all the calculations to know you should stop when there x good cards and >y bad cards remaining---it can only be worse, never better. This skipping of most of the bottom triangle cuts off almost half the state space (because it’s the lower triangle) and thus, skips half the computations, and since we are compute-bound, almost doubles speed:
This is very nice, but what I would prefer is a proven simple bound on the number of bad cards where this happens. This makes it possible1 to avoid recursion altogether and simply return “stop” for some of these values2.
To make some Questions explicit: What upper/lower bounds can we give on the number of red/black cards that will result in a zero/nonzero expected score…
…given a number of black/red cards?
…given a total # of cards?
…given a fixed difference in the number of cards?
Conjecture
Gwern notes that the score for a balanced deck roughly goes up with the square root of the number of cards. One can informally justify this observation by observing that an unbiased random walk in one dimension for n steps will have a maximum value around ~√n. By the same token, one could conjecture that the cutoff for where it becomes suboptimal to continue is when the bad cards outnumber the good cards by ~k√n, where n is the number of cards in the deck. From this, I conjectured that there should be some 0 < k such that when b > r + k√r, it’s optimal to stop.
My proof attempts
I tried for a few years to prove this, but it’s tricky. We would like to have some upper bound on the equity, perhaps proven inductively. But this upper bound has to have a weird shape: It’s zero when b > r + k√r, but when b ≪ r, then it should be around ~ (r − b), because it’s likely that around that point we will have drawn the whole deck.
AI enters the picture
These days I work for an AI nonprofit, and I have been testing our Fuse application for developing formal proofs. The conjecture above isn’t too hard to formalize, so I stuck it in and asked Fuse to come up with a proof strategy.
After a false start and getting it to come up with some basic definitions, Fuse came up with the approach of interpolating between the zero region and the linear region quadratically and trying to prove that as an upper bound on the equity. It used the term “supersolution”, which I had never heard before, but which seems to just be a fancy term for “upper bound” when you have a differential/difference equation.
A closer look at the algebra
AI can bash lots of algebra to solve a problem, so it makes sense that the solution it came up with is along these lines.
The proof idea is that, if our supersolution is given as this piecewise formula defined as zero / quadratic / linear for the high / medium / low values of b, then checking that this formula gives an upper bound can be done by proving it remains consistent with the main recursion. And if we relax the inputs to be nonnegative real numbers, is just a matter of proving some polynomial inequalities hold for each of the cases within and on the border of the regions.
Because the region boundaries are defined using only square roots and arithmetic, the relaxation of this to the reals is a decidable algebraic problem. In theory, solving this decision problem might take a long time, but in practice, the AI can verify that the solution is right by programmatically checking a bunch of numbers, and then play with algebraic manipulations for the different regions over multiple turns.
Positivstellensatz
Fuse was able to handle all of the cases except for the curved border, which it pointed out should be solvable by “Sum-of-squares” (SOS) / Positivestellensatz techniques. I passed that instruction to an external model with Python support and it was able to find a solution, thereby proving the theorem. Hooray!
At this point the proof was looking very gnarly, but the appearance of SOS made me optimistic because there is actually a Lean tactic for that. I was able to use this to golf the proof somewhat (although I couldn’t get it to close the main goal, the tactic is unfortunately a bit buggy and/or slow). After bit more tweaking I got the constant down to k = 4.
Conclusions
The equity of the Problem 14 game with b black cards and r red cards is at most
0 for r + 4√r ≤ b
(r + 4√r − b)² / (6√r) for r ≤ b < r + 4√r
(r − b) + (8/3)√r for b < r
This seems useful for efficiently computing large values of e(r, b), and certainly for computing which cases you should stop in and which you should continue. You should obviously continue when there are more red cards than black, so there are now only 4√r many black-card-counts for which we have to do any computation at all (beyond the computation of the square root itself).
Probably it is possible to go further by handing edge cases near zero and using a more powerful sum of squares solver. I’d be interested in hearing about any progress made on this.
Here is a nice chart to show the gap between theory and reality:
And here is a link to the Lean code.
with a larger number of cards, say
ignoring the expected value part of the problem, which wouldn’t be practical in reality anyway