@youzicha Replied to your post “from yudkowsky's 2009 post Timeless Decision...”:
What do you think is the point of the proof model? What would be a better way to formulate decisions?
So I've got to say that proof systems have a natural appeal as a model of a rational agent because it seems like a model of reasoning on paper: making a pros cons list to compare two job offers, calculating the expected yield of a bunch of different oil wells, whatever. But I saw people working on it and running into all this weird godel shit and it just seemed like they were getting distracted. I didn't think there was anything interesting to say at this crazy level of generality, like consider an arbitrary decision problem that you address with mathematical reasoning. I thought once you talk about any specific problem all this metamathematics wouldn't come up.
So that's how I was thinking years ago, so let's forget about proof based agents for now.
Let's think about the broad idea of conceiving of your thought and action as the result of some algorithm. Instead of thinking of logical decision theory as a tool for getting the right answer in both smoking lesion and newcomb's problem (a tool for what job?), let's think of those problems as ways of exposing the weirdness of this idea of your action as the result of an algorithm. Like, what do you do when there's another implementation of that algorithm in the environment?
But really all a newcomblike problem does is make unavoidable what's always there, that you're thinking about a world that contains some implementation of your decision algorithm, namely you. Which is the classic determinism vs free will paradox, like can you make choices in a deterministic world.
Taking a Yudkowsky "what does the algorithm feel like from the inside" perspective on that... what kind of deterministic algorithm feels like it has volition, experiences this paradox? And I think the answer is any that's making choices using a world model that explicitly includes a description of itself. Such an agent can model stuff like "if this force vector were applied to this egg, it would fall off the counter and crack on the floor", but if it tries to ask "will the robot standing at the counter push the egg", it ends up in an infinite loop, an infinite mirror tunnel. Well let me just boot up a simulation of the whole kitchen, including the robot, well I see the robot booting up a simulation...
It's a point so simple you would think nobody could miss it but they do: you can't actually simulate yourself making the decision, as part of making the decision. You don't feel, to yourself, deterministic in the same way as your environment, because you can't actually use the mapping from your initial state to your decision, at least not when you're making your decision.
Okay that's great but I don't really like this perspective of imagining the execution of the program. Well if the RobotDecide function calls the RobotDecide function we loop forever so the execution path must be something else.
And that brings us back to the proof system model. All of this "dynamic" stuff about imagining the robot simulating itself has "static" analogues as metamathematical statements. That there's some fundamental difference between the robot simulating itself versus simulating its environment excluding itself is just the familiar metamathematical phenomenon of incompleteness as a result of self-reference. Which suggests an intriguing answer to "what kind of proof-based agent feels like it has volition"? One where its proof system is incomplete by not proving statements about the result of its decision. The agent is deterministic in the sense that it's some computer program, but not in the sense that its actions are logical consequences of the code (in whatever proof system it's using to decide).
Now I don't feel like the godel stuff is a distraction anymore, see? What I'm interested in, this inability to "predict" your own decision as part of the process of making it, is showing up as metamathematics stuff.
Or... you could imagine it could work out that way, based on conceptual associations. Like, there's self reference, so there's incompleteness; if we anthropomorphize the agent we could imagine incompleteness about its decisions as a feeling of volition... But does it actually work out like this? I mean, we could have incompleteness where the agent's proof system can't prove what its decisions are, but do we? Exactly what statements are we talking about proving?
So now getting to the other half of your question: what's a decision. And my answer is: a proof-based agent searches for proofs of a "report", which is a conjunction of implications like "if i take this action, the state of the environment will be that". For a concrete example, think of the prisoner's dilemma, where the "state of the environment" is the other player's action. Finding a report triggers an action in the obvious way (actions and states jointly determine consequences, there's a preference ordering on consequences).
This is different from the standard MIRI setup with fallback options (if i find a proof of the statement, do this; otherwise do that). To see the difference, imagine that the proof system is inconsistent. In the MIRI setup, that means we necessarily find the proof we're looking for. Inconsistency implies FairBot cooperates. In my setup, it means that the agent's action depends on which report it finds first, since every report has a proof. So instead of inconsistency determining the agent's action, it means the agent's action is nondeterministic.
Nondeterministic? Is the agent deterministic or not? So, here's where I realized this whole setup is a sort of cheat or dodge regarding the free will question. Suppose the agent searches proofs pseudorandomly. It has some seed for its random number generator, so which report it finds (assuming inconsistency) depends on the seed. What I want is for the agent's proof system to always be trying to prove what would happen regardless of the seed, so whenever the outcome depends on the seed, we have incompleteness. It's like the agent is pretending it doesn't know the full specification of its code, in which case it's not surprising that we have what looks like a violation of determinism. I think this cheat is benign, just like when we use probability theory to compute the expected time it will take for our bitcoin mining rig to add a block; I'm comfortable doing that calculation even if I already have the block on my computer so the answer is determined.
The reason what I'm describing isn't a fully specified decision theory is because I haven't told you what "the agent takes action A" means in the implications "if the agent takes action A, the state of the environment is S". I guess it has to be the statement that the agent proves a report in which the optimal decision is A. That seems like it should work. One appealing feature is there's no proof or disproof of "the agent takes action A", because the proof system can't prove its consistency, so it can't prove that there's one unique report that must come out of a proof search. So we don't have those FDT issues with counterpossibles.
Still, it's just a sketch at this point. I'll believe this really works when I can write down these report strings for the prisoner's dilemma and derive what the agent does.
