A different angle on UDT

[So8res]

Instead of directly asking “what decision theory should an agent run,” consider the question, “given a description of an environment and a description of an agent, identify the best action available to that agent, regardless of its algorithm.”

These are pretty much the same question, with slightly different framings. (If you answer the latter, then the answer to the former is “approximate the latter thing on the world model.”) The latter question is more general, though, and it highlights different parts of the problem.

For example, it highlights questions about what counts as an agent, how the agent is identified in the environment, how the set of things the agent “could have done” is determined, how the agent’s “observations” are identified, and so on. These parts of the question are where decision theory intersects with naturalized induction.

This angle puts the spurious proof problem in a new light. Instead of considering UDT as an algorithm which computes what its best available strategy is, consider a “global” version of UDT which takes any description of an environment and an agent within that environment, and computes the best strategy available to that agent.

Assume away the naturalized problems and say that there is a sorted list of outcomes (best first) and a set of available strategies (observation-to-action mappings). Now we can define GlobalUDT(E, A) as a function which takes a description E of the environment, a description A of the agent, and computes the best strategy available to that agent:

(I don’t know how to use latex in code blocks, so braces are used as dequotes in strings: if x="ell" then "h{x}o" is the string "hello".)

def GlobalUDT(E, A):
  for o in outcomes:
    for s in strategies:
      if PA proves "{A}()={s} implies {E}()={o}":
        return s
  return default_strategy

For a given universe U, Vladimir’s proof-based UDT can be recovered by defining the following via quining:

UDT := GlobalUDT(quote(U), quote(UDT))

And, as it happens, GlobalUDT will always identify the actual best strategy available to UDT. (GlobalUDT never finds bad spurious proofs, because it iterates through outcomes in order; if there are any spurious proofs then they are spurious proofs that the best strategy is the best strategy.) But GlobalUDT does not identify the best strategy for agents in general!

Consider the following universe:

outcomes = [3, 2, 1]
strategies = {Hi, Med, Low}
A = lambda: Low
E = lambda: {Hi: 3, Med: 2, Low: 1}[A()]

That is, there are three options Hi, Med, Low corresponding to payoffs 3, 2, 1. The “agent” always selects the action Low. GlobalUDT("E", "A") either returns Hi or Med, whichever it considers first, because both A()=Hi and A()=Med are contradictory (and so imply E()=Hi).

This isn’t all that surprising (what does it mean to ask what would have happened if (lambda: Low)() == Hi?), but it does distill the problem with using logical implications as counterfactuals a bit.GlobalUDT only identifies the right strategy on UDT because it happens that UDT is something in the environment where knowing what it does requires knowing that PA is consistent, and GlobalUDT doesn’t know that.

(But a version of GlobalUDT using ZFC would prescribe bad strategies for a PA-based version of UDT in the environment.)

Moving beyond proof-based UDT requires a better theory of logical counterfactuals, and GlobalUDT provides a slightly different angle of approach than the one I’m used to. Intuitively, a satisfactory theory of logical counterfactuals should give us an algorithm that identifies Hi as the best strategy available to const Low. I’m actually not too convinced that such a thing is possible/​meaningful (at least, not without context and better answers to questions like “what’s an agent” and “what’s an embedding”), but this makes it a bit clearer that when we talk about wanting a full theory of logical counterfactuals we’re talking about defining a working version of GlobalUDT.

Food for thought.