Intelligent Agent Foundations Forumsign up / log in
An implementation of modal UDT
post by Benja Fallenstein 591 days ago | Jessica Taylor, Luke Muehlhauser, Nate Soares and Patrick LaVictoire like this | discuss

One of the great advantages of working with Gödel-Löb provability logic is that it’s possible to implement an evaluator which efficiently checks whether a sentence in the language of GL is true. Mihaly and Marcello used this to write a program that checks whether two modal agents cooperate or defect against each other. Today, Nate and I extended this with an implementation of modal UDT, which allows us to check what UDT does on different decision problems—see Program.hs in the Github repository. No guarantees for correctness, since this was written rather quickly; if anybody is able to take the time to check the code, that would be very much appreciated!


The implementation of UDT is rather pleasing, I think. Here’s the informal definition of modal UDT, using PA + \(\ell\):

  • For every possible outcome \(j\), from best to worst:
    • For every possible action \(i\), in order:
      • If it’s provable in PA + \(\ell\) that “UDT takes action \(i\)” implies “the universe returns outcome \(j\)”, then take action \(i\).
  • If you’re still here, return a default action.

Here is the corresponding Haskell code:

udt :: (Enum a,Ord b,Show b,Enum b)
    => Int -> ModalProgram b a -> b -> ModalProgram b b
udt level univ dflt = modalProgram dflt $
  mFor $ \a ->
    mFor $ \b ->
      mIf (boxk level (Var b %> univ a)) (mReturn b)

Being able to write modal UDT like this makes it very easy to implement and try small variations on the code.


We used this code to check what modal UDT would do in a version of Newcomb’s problem where Omega uses proofs in PA (rather than simulations) to decide whether to put the money in the box; that is, it will put a million dollars in the first box if and only if it can prove that you will one-box. If our code is correct, it turns out that in this case, modal UDT will do whatever its default action was.

Earlier, we thought we had proved a different result on the whiteboard, but after the code disagreed with us, we went over it again and found a bug in our proof. After fixing that bug, we now have a manual proof that UDT will end up taking its default action in this scenario (which I’ll write about some other time). So looks like this can be a useful tool for figuring out this sort of thing!



NEW LINKS

NEW POSTS

NEW DISCUSSION POSTS

RECENT COMMENTS

I strongly predict that if
by Jessica Taylor on Heroin model: AI "manipulates" "unmanipulatable" r... | 0 likes

Wireheading the human is the
by Stuart Armstrong on Heroin model: AI "manipulates" "unmanipulatable" r... | 0 likes

Re 1: There are cases where
by Jessica Taylor on Heroin model: AI "manipulates" "unmanipulatable" r... | 0 likes

1. I don't really see the
by Stuart Armstrong on Heroin model: AI "manipulates" "unmanipulatable" r... | 0 likes

If we could model humans as
by Wei Dai on (C)IRL is not solely a learning process | 0 likes

1. Can we agree that this is
by Jessica Taylor on Heroin model: AI "manipulates" "unmanipulatable" r... | 0 likes

This was initially setup in
by Stuart Armstrong on Heroin model: AI "manipulates" "unmanipulatable" r... | 0 likes

This significantly clarifies
by Jessica Taylor on Heroin model: AI "manipulates" "unmanipulatable" r... | 0 likes

What kind of object is $Q$?
by Paul Christiano on (C)IRL is not solely a learning process | 0 likes

The model $P$ is simply a
by Stuart Armstrong on (C)IRL is not solely a learning process | 0 likes

>For example, if you assume
by Stuart Armstrong on (C)IRL is not solely a learning process | 0 likes

Do you think that we can
by Paul Christiano on (C)IRL is not solely a learning process | 0 likes

(I saw your comment several
by Wei Dai on (C)IRL is not solely a learning process | 0 likes

>Most value learning
by Paul Christiano on Learning values versus learning knowledge | 0 likes

Having separate models $P$
by Paul Christiano on (C)IRL is not solely a learning process | 1 like

RSS

Privacy & Terms (NEW 04/01/15)