Agents that can predict their Newcomb predictor

[orthonormal]

There’s a certain type of problem where it appears that having more computing power hurts you. That problem is the “agent simulates predictor” Newcomb’s Dilemma.

As Gary Drescher put it:

There’s a version of Newcomb’s Problem that poses the same sort of challenge to UDT that comes up in some multi-agent/​game-theoretic scenarios.

Suppose:

• The predictor does not run a detailed simulation of the agent, but relies instead on a high-level understanding of the agent’s decision theory and computational power.

• The agent runs UDT, and has the ability to fully simulate the predictor.

Since the agent can deduce (by low-level simulation) what the predictor will do, the agent does not regard the prediction outcome as contingent on the agent’s computation. Instead, either predict-onebox or predict-twobox has a probability of 1 (since one or the other of those is deducible), and a probability of 1 remains the same regardless of what we condition on. The agent will then calculate greater utility for two-boxing than for one-boxing.

Meanwhile, the predictor, knowing that the the agent runs UDT and will fully simulate the predictor, can reason as in the preceding paragraph, and thus deduce that the agent will two-box. So the large box is left empty and the agent two-boxes (and the agent’s detailed simulation of the predictor correctly shows the predictor correctly predicting two-boxing).

The agent would be better off, though, running a different decision theory that does not two-box here, and that the predictor can deduce does not two-box.

EDITED 5/​19/​15: There’s a formal model of this due to Vladimir Slepnev where the agent and the predictor both have different types of predictive powers, such that in some sense they each know how the other will act in this universe. We’ll write this out along with another case where things work out properly.

(One algorithm has more computing power, but the other has stronger axioms: in particular, strong enough to prove that the other formal system is sound, as ZFC proves that PA is sound.)

In one of the following cases, proof-based UDT one-boxes for correct reasons; in the other case, it two-boxes analogously to the reasoning above.

---

In both cases, we’ll use the following lemma:

Lemma: Let $A\left(\right)$ be an algorithm that returns either 1 or 2, such that ZFC has a proof of length $\approx \log \left(N\right)$ of ”$A\left(\right)$ returns in $\le N$ steps”. Then ZFC has a proof of length $\approx \log \left(N\right)$ that ”$A\left(\right)=1$ if and only if PA proves that $A\left(\right)=1$.”

Proof: ZFC knows that PA is sound, so ZFC has a short proof that “if PA proves that $A\left(\right)=1$, then $A\left(\right)=1$”. The other direction follows from the fact that the algorithm is bounded, and PA can simply show the execution trace of $A$ in $\le CN$ steps.

Case 1: Success (Agent Trusts Predictor)

Omega looks through all proofs in PA; when it finds a proof that the agent one-boxes or a proof that the agent two-boxes, it stops looking and fills or empties the box accordingly. (If it fails to prove either, it empties the box.)

The agent looks several times through all proofs in ZFC of length $\le N$; it first looks for a proof that one of its actions leads to the payoff $1001000, then $1000000, then $1000, then $0. The first time it finds a proof that an action implies the outcome it’s looking for, it immediately takes that action. (If it fails to find any such proof, it two-boxes.)

I claim that for sufficiently large $N$, the agent one-boxes, and Omega fills the box.

Proof: We use the Lemma. ZFC proves in $\le N$ steps that $A\left(\right)=1\leftrightarrow {\square }_{PA}\left[A\right()=1]$. Since we (from outside the problem) assume ZFC is consistent, it will not be able to prove that two-boxing gets it $1001000, nor that one-boxing gets it $1001000, nor that two-boxing gets it $1000000, but it will be able to prove that one-boxing gets it $1000000. Thus it one-boxes. Since it runs in finite time, of course PA proves it one-boxes, and so Omega fills the box.

Case 2: Failure (Agent Simulates Predictor)

We’ll swap the deductive processes this time. Omega looks through all proofs in ZFC of length $\le N$; when it finds a proof that the agent one-boxes or a proof that the agent two-boxes, it stops looking and fills or empties the box accordingly. (If it fails to prove either, it empties the box.)

The agent looks several times through all proofs in PA; it first looks for a proof that one of its actions leads to the payoff $1001000, then $1000000, then $1000, then $0. The first time it finds a proof that an action implies the outcome it’s looking for, it immediately takes that action. (If it fails to find any such proof, it two-boxes.)

I claim that the agent two-boxes, and Omega leaves the box empty.

Proof: Again, by the lemma, ZFC proves that $\Omega \left(\right)=1\leftrightarrow {\square }_{PA}\left[\Omega \right()=1]$ (where $\Omega \left(\right)=1$ means “Omega predicts one-boxing and thus fills the box”). Now note that $\Omega \left(\right)=1$ implies that PA proves $A()=2 \to U=$1001000$ and does not prove that $A()=1 \to U=$1001000$, and thus in this case $A\left(\right)=2$; and similarly, $\Omega \left(\right)=2$ implies that PA proves $A()=2 \to U=$1000$ and does not prove any of the prior counterfactuals, so again $A\left(\right)=2$. All of these proofs are quick within ZFC, so $\Omega$ does prove that $A\left(\right)=2$, and thus $\Omega \left(\right)=2$.

[cousin_it]

Your second case seems really similar to my post about ASP from 2011: http://​​lesswrong.com/​​lw/​​5rq/​​example_decision_theory_problem_agent_simulates/​​

[orthonormal]

You’re absolutely right. I know I was in a hurry writing this post, but I don’t know how I managed to skip reading the second half of the post that I excerpted.

[Benya_Fallenstein]

The other direction follows from the fact that the algorithm is bounded, and PA can simply show the execution trace of $A$ in $\le CN$ steps.

Unimportant technical point: I think the length of the PA proof grows faster than this. (More precisely, the length in symbols, rather than the length in number of statements; we’re almost always interested in the former, since it determines how quickly a proof can be checked or be found by exhaustive search.) The obvious way of showing $A\left(\right)=1$ in PA is to successively show for higher and higher $t$ that “after $t$ ticks, the Turing machine computing $A\left(\right)$ is in the following state, and its tapes have the following content”. But even to write out the contents of the tape of a Turing machine that has run for $t$ ticks will in general take $t$ symbols. So the obvious way of doing the proof takes at least $O\left(t^2\right)$ symbols. Moreover, I’m not sure whether we can get from “at time $t$, the configuration is such-and-such” to “at time $t+1$, the configuration is such-and-such” in a constant number of proof steps. I suspect we don’t need more than $O\left(t^3\right)$ symbols overall, but I’m not extremely confident. (I’d be quite surprised if the time turned out not to be polynomial, though!)

[orthonormal]

Note that in both this and the other model of Agent Simulates Predictor, the agent’s formal system does not know that the predictor’s formal system is consistent. One could argue that in this case it’s right to two-box. However, it’s still worrisome that the agent’s formal system proves $A()=1 \to U()= $0$ and does not prove $A()=1 \to U()= $1000000$, rather than proving both counterfactuals (spuriously) or neither.