I still feel that logical uncertainty has to be tackled head on, rather than kept unspecified behind diagrams. But you bring up an interesting point. In the transparent Newcomb’s problem as originally formulated by Gary, the simulated agent sees both boxes as filled. That way both the agent and the predictor can be deterministic, and the agent can’t cause a paradox by doing the opposite of what was predicted. Maybe we should reformulate ASP in the same way.
Yes, logical uncertainty clearly needs to be dealt with, although I’d be interested in seeing a proper statement of the problem in its general form. Diagrams like this are a useful tool because you can give an uncontroversial correct answer to “what is the optimal strategy for diagram X?” but they don’t answer the underlying questions unless you also have a theory that says the diagram should be drawn THIS way and not THAT way.
I think the diagrams I made are valid; the ASP one in particular is justified pretty well by the exact same reasoning that goes into Eliezer’s TDT. The LCM one relies pretty heavily on being able to assign a prior probability of 0.5 to both possibilities, but without justification for something else I see little other choice than to go for a 50⁄50 split.
Also, yes; I do think that ASP in its standard form is underspecified, unlike Gary’s transparent Newcomb’s problem.
In terms of the proof-searching formalism you bring up in your post on ASP, you have these issues: 1) If proofs of one-boxing and two-boxing are both valid, which one gets found first? 2) If no proof can be found at all, what does the predictor do?
I think the straightforward way to resolve this issue with ASP is to state that the predictor only searches for proofs up to length N that the agent one-boxes, and fills both boxes if and only if it finds such a proof. This resolves the issue in the exact same way that “FairBot” does in the “Robust Cooperation” paper, right? Also, it’s essentially analogous to Gary’s transparent Newcomb’s, because searching for a proof that the agent one-boxes is pretty much the same idea as simulating what they would do if both boxes were filled.
Of course, it’s sufficiently well-specified in your original ASP post because you also specified an algorithm for the agent; in this case the agent happens to find a proof that two-boxing leads to $1000 and a “spurious” proof that one-boxing leads to $0, both of which do indeed turn out to be true because that agent ends up two-boxing.
If proofs of one-boxing and two-boxing are both valid, which one gets found first?
They can’t be both valid, because only one of the two statements is true. We assume that the predictor’s formal theory is sound (doesn’t prove false statements).
If no proof can be found at all, what does the predictor do?
Right, that’s the underspecified part. I guess the predictor should fill only one box in this case.
I think the straightforward way to resolve this issue with ASP is to state that the predictor only searches for proofs up to length N that the agent one-boxes, and fills both boxes if and only if it finds such a proof. This resolves the issue in the exact same way that “FairBot” does in the “Robust Cooperation” paper, right?
I think the UDT agent will still two-box in that case, for the same reason as before. To have FairBot-style cooperation, the agent must also search for one-sided proofs only.
Also, it’s essentially analogous to Gary’s transparent Newcomb’s, because searching for a proof that the agent one-boxes is pretty much the same idea as simulating what they would do if both boxes were filled.
Why? If an agent one-boxes when both boxes are filled, that doesn’t necessarily mean the agent one-boxes unconditionally.
They can’t be both valid, because only one of the two statements is true. We assume that the predictor’s formal theory is sound (doesn’t prove false statements).
True, but still underspecified. They can’t both be valid at the same time, but the point is that a priori it’s possible that either one could be valid, and you don’t know which one without knowing additional details. If the agent one-boxes whenever the predictor predicts it one-boxes, and two-boxes whenever the predictor predicts it two-boxes, the predictor’s actual prediction is arbitrary—it will depend on the specific details of the predictor’s proof-searching algorithm. I’m guessing this means that the proof itself would have to involve those details in some way.
I think the UDT agent will still two-box in that case, for the same reason as before. To have FairBot-style cooperation, the agent must also search for one-sided proofs only.
That would depend on the details of the UDT agent, wouldn’t it? It’s hard to say without those details. If you’re assuming the proof-searching model then yes, but that’s the same old spurious proof problem isn’t it?
Why? If an agent one-boxes when both boxes are filled, that doesn’t necessarily mean the agent one-boxes unconditionally.
If an agent one-boxes when both boxes are filled then the predictor will predict that the agent one-boxes when both boxes are filled, and so both boxes will be filed, and so the agent one-boxes unconditionally.
If you’re assuming the proof-searching model then yes, but that’s the same old spurious proof problem isn’t it?
Yeah.
If an agent one-boxes when both boxes are filled then the predictor will predict that the agent one-boxes when both boxes are filled, and so both boxes will be filed, and so the agent one-boxes unconditionally.
I’m confused, which implementation of the predictor are you assuming in that sentence? I don’t think that every predictor will be able to figure out every true statement about the agent...
Yeah, a predictor won’t necessarily figure out every true statement, but my original point was about the transparent Newcomb’s, in which case if Omega finds that the agent one-boxes whenever Omega fills both boxes, then Omega will fill both and the agent will one-box.
In the case of the proof-searching model things aren’t quite as nice, but you can still get pretty far. If the predictor has a sufficiently high proof limit and knows that it fills both boxes whenever it finds a proof of one-boxing, then a short enough proof that the agent one-boxes whenever both boxes are filled should be sufficient (I’m quite sure a Löbian argument holds here).
So yes, from the predictor’s point of view, a proof that the agent one-boxes whenever both boxes are filled should be sufficient. Now you just need the agent to not be stupid...
I still feel that logical uncertainty has to be tackled head on, rather than kept unspecified behind diagrams. But you bring up an interesting point. In the transparent Newcomb’s problem as originally formulated by Gary, the simulated agent sees both boxes as filled. That way both the agent and the predictor can be deterministic, and the agent can’t cause a paradox by doing the opposite of what was predicted. Maybe we should reformulate ASP in the same way.
Yes, logical uncertainty clearly needs to be dealt with, although I’d be interested in seeing a proper statement of the problem in its general form. Diagrams like this are a useful tool because you can give an uncontroversial correct answer to “what is the optimal strategy for diagram X?” but they don’t answer the underlying questions unless you also have a theory that says the diagram should be drawn THIS way and not THAT way.
I think the diagrams I made are valid; the ASP one in particular is justified pretty well by the exact same reasoning that goes into Eliezer’s TDT. The LCM one relies pretty heavily on being able to assign a prior probability of 0.5 to both possibilities, but without justification for something else I see little other choice than to go for a 50⁄50 split.
Also, yes; I do think that ASP in its standard form is underspecified, unlike Gary’s transparent Newcomb’s problem.
In terms of the proof-searching formalism you bring up in your post on ASP, you have these issues:
1) If proofs of one-boxing and two-boxing are both valid, which one gets found first?
2) If no proof can be found at all, what does the predictor do?
I think the straightforward way to resolve this issue with ASP is to state that the predictor only searches for proofs up to length N that the agent one-boxes, and fills both boxes if and only if it finds such a proof. This resolves the issue in the exact same way that “FairBot” does in the “Robust Cooperation” paper, right? Also, it’s essentially analogous to Gary’s transparent Newcomb’s, because searching for a proof that the agent one-boxes is pretty much the same idea as simulating what they would do if both boxes were filled.
Of course, it’s sufficiently well-specified in your original ASP post because you also specified an algorithm for the agent; in this case the agent happens to find a proof that two-boxing leads to $1000 and a “spurious” proof that one-boxing leads to $0, both of which do indeed turn out to be true because that agent ends up two-boxing.
They can’t be both valid, because only one of the two statements is true. We assume that the predictor’s formal theory is sound (doesn’t prove false statements).
Right, that’s the underspecified part. I guess the predictor should fill only one box in this case.
I think the UDT agent will still two-box in that case, for the same reason as before. To have FairBot-style cooperation, the agent must also search for one-sided proofs only.
Why? If an agent one-boxes when both boxes are filled, that doesn’t necessarily mean the agent one-boxes unconditionally.
True, but still underspecified. They can’t both be valid at the same time, but the point is that a priori it’s possible that either one could be valid, and you don’t know which one without knowing additional details. If the agent one-boxes whenever the predictor predicts it one-boxes, and two-boxes whenever the predictor predicts it two-boxes, the predictor’s actual prediction is arbitrary—it will depend on the specific details of the predictor’s proof-searching algorithm. I’m guessing this means that the proof itself would have to involve those details in some way.
That would depend on the details of the UDT agent, wouldn’t it? It’s hard to say without those details. If you’re assuming the proof-searching model then yes, but that’s the same old spurious proof problem isn’t it?
If an agent one-boxes when both boxes are filled then the predictor will predict that the agent one-boxes when both boxes are filled, and so both boxes will be filed, and so the agent one-boxes unconditionally.
Yeah.
I’m confused, which implementation of the predictor are you assuming in that sentence? I don’t think that every predictor will be able to figure out every true statement about the agent...
Yeah, a predictor won’t necessarily figure out every true statement, but my original point was about the transparent Newcomb’s, in which case if Omega finds that the agent one-boxes whenever Omega fills both boxes, then Omega will fill both and the agent will one-box.
In the case of the proof-searching model things aren’t quite as nice, but you can still get pretty far. If the predictor has a sufficiently high proof limit and knows that it fills both boxes whenever it finds a proof of one-boxing, then a short enough proof that the agent one-boxes whenever both boxes are filled should be sufficient (I’m quite sure a Löbian argument holds here).
So yes, from the predictor’s point of view, a proof that the agent one-boxes whenever both boxes are filled should be sufficient. Now you just need the agent to not be stupid...