The FairBot from the MIRI prisoner's dilemma tournament is defined by a theorem of Peano arithmetic (PA) that holds for each opponent: where is "the FairBot cooperates" and is "the opponent cooperates". As a source for FairBot, the paper cites Vladimir Slepnev, aka cousin_it. Though this isn't what's cited in...
One model of rational agency is a proof-based agent, and one fun exercise with proof-based agents is to play them against each other in prisoner's dilemmas. The players are computer programs that exchange source code and try to decide whether to cooperate or defect by writing formal proofs. In this...
A logical decision theory recommends that you choose as if deciding the output of your decision algorithm. The main difficulty in formulating a logical decision theory is how to define statements like: "If my algorithm outputs this, the result will be that". These look like counterfactual implications, but counterfactuals describe...
MIRI's proof-based prisoner's dilemma tournament defined agents encoded as formulas of Peano arithmetic (PA) with one free variable. means the agent cooperates in a match against the agent , and is constructed by plugging the Gödel number of the formula defining into the formula defining . The simplest interesting agent...
Recently I’ve been thinking a lot about a certain model of a rational agent: a proof-based agent which is triggered to act when it finds certain proofs in Peano arithmetic (PA). Back when MIRI had an agent foundations team, they found they could derive what these agents would do using...
In his original paper on what we now call the "many-worlds" interpretation, Everett motivated it with quantum cosmology, since there's nowhere outside the universe for a Copenhagen-style observer to stand. Eliezer Yudkowsky said something similar to motivate timeless decision theory: > I hold it a virtue of any decision theory...