MIRI’s publications seem to exclusively refer to TDT
Why do you say that? If I do a search for “UDT” or “TDT” on intelligence.org, I seem to get about an equal number of results.
people here on LW seem to refer pretty much exclusively to UDT in serious discussion
This seems accurate to me. I think what has happened is that UDT has attracted a greater “mindshare” on LW, to the extent that it’s much easier to get a discussion about UDT going than about TDT. Within MIRI it’s probably more equal between the two.
that UDT is just an uninteresting variant of TDT so as to hardly merit its own name
As I recall, Eliezer was actually the one who named UDT. (Here’s the comment where he called it “updateless”, which everyone else then picked up. In my original post I never gave it a name but just referred to “this decision theory”.)
Has either one been fully specified/formalized?
There has been a number of attempts to formalize UDT, which you can find by searching for variations on “formal UDT” on LW. I’m not aware of a similar attempt to formalize TDT, although this paper gives some hints about how it might be done. It’s not really possible to “fully” specify either one at this time because both need to interface with a to-be-discovered solution to the problem of logical uncertainty, and at this point we don’t even know the type signature of such a solution. In the attempts to formalize UDT, people either make a guess as to what the type signature is, or side-step the problem by assuming that all relevant logical facts can be deduced by the agent.
Thanks! This is exactly the kind of answer I was hoping for. A lot of it was what I had sort of deduced from looking at MIRI docs and stuff, but having it laid out explicitly seems to have clicked the missing elements into place and I feel like I understand it much better now.
Why do you say that? If I do a search for “UDT” or “TDT” on intelligence.org, I seem to get about an equal number of results.
This seems accurate to me. I think what has happened is that UDT has attracted a greater “mindshare” on LW, to the extent that it’s much easier to get a discussion about UDT going than about TDT. Within MIRI it’s probably more equal between the two.
As I recall, Eliezer was actually the one who named UDT. (Here’s the comment where he called it “updateless”, which everyone else then picked up. In my original post I never gave it a name but just referred to “this decision theory”.)
There has been a number of attempts to formalize UDT, which you can find by searching for variations on “formal UDT” on LW. I’m not aware of a similar attempt to formalize TDT, although this paper gives some hints about how it might be done. It’s not really possible to “fully” specify either one at this time because both need to interface with a to-be-discovered solution to the problem of logical uncertainty, and at this point we don’t even know the type signature of such a solution. In the attempts to formalize UDT, people either make a guess as to what the type signature is, or side-step the problem by assuming that all relevant logical facts can be deduced by the agent.
Thanks! This is exactly the kind of answer I was hoping for. A lot of it was what I had sort of deduced from looking at MIRI docs and stuff, but having it laid out explicitly seems to have clicked the missing elements into place and I feel like I understand it much better now.
You might also find this honor’s thesis by Daniel Hintze handy.