## Posts

Optimization Concepts in the Game of Life 2021-10-16T20:51:35.821Z
Intelligence or Evolution? 2021-10-09T17:14:40.951Z
Draft papers for REALab and Decoupled Approval on tampering 2020-10-28T16:01:12.968Z
Modeling AGI Safety Frameworks with Causal Influence Diagrams 2019-06-21T12:50:08.233Z
Thoughts on Human Models 2019-02-21T09:10:43.943Z
Cambridge UK Meetup Saturday 12 February 2011-02-02T14:20:02.418Z

Comment by Ramana Kumar (ramana-kumar) on Intelligence or Evolution? · 2021-10-17T14:49:11.703Z · LW · GW

This is a good point. Could something like Shapley value help in distributing credit for X between the humans and the impersonal mechanism? I find myself also wanting to ask about how frequent these cases are -- where it could easily be viewed both ways -- and declare that if it's mostly ambiguous then 'evolution' wins.

For "some impersonal mechanism" I'm thinking "memetic fitness of X amongst humans" (which in some cases cashes out as the first group of humans being larger?). What are other ways of thinking about it?

The story feels a little underspecified. When X happens because the first group of humans figured out how to thwart the second group, and anticipated them, etc. and furthermore if that group consistently does this for whatever they want, it seems a lot more like intelligence.

Comment by Ramana Kumar (ramana-kumar) on Intelligence or Evolution? · 2021-10-12T11:03:27.882Z · LW · GW

I did intend 'Evolution' here to include markets. The main contrast I'm trying to make is to a unified rational actor causing the outcomes it wants.

Comment by Ramana Kumar (ramana-kumar) on Intelligence or Evolution? · 2021-10-12T11:01:06.662Z · LW · GW

I agree that both are good explanations. My question is more about which will be dominant in the long run. I tried to ask this more clearly with the mutually exclusive version in the post (someone vs no one was trying to produce the outcome).

I could view the "Why not both?" response as indicating that neither is dominant and we just have to understand how both operate simultaneously (perhaps on different timescales) and interact. I think I'd view that as actually coming down mostly on the evolution side of things - i.e., this means I should understand intelligence only in the larger evolutionary context -- no intelligence will permanently outstrip and render irrelevant the selection forces. Is that right?

Comment by Ramana Kumar (ramana-kumar) on Finite Factored Sets: Conditional Orthogonality · 2021-09-13T13:26:35.602Z · LW · GW

That's right. A partial function can be thought of as a subset (of its domain) and a total function on that subset. And a (total) function can be thought of as a partition (of its domain): the parts are the inverse images of each point in the function's image.

Comment by Ramana Kumar (ramana-kumar) on The Blackwell order as a formalization of knowledge · 2021-09-12T21:56:46.003Z · LW · GW

Blackwell’s theorem says that the conditions under which  can be said to be more generally useful than  are precisely the situations where  is a post-garbling of .

Are the indices the wrong way around here?

Comment by Ramana Kumar (ramana-kumar) on Introduction to Cartesian Frames · 2021-05-17T08:25:51.241Z · LW · GW

A formalisation of the ideas in this sequence in higher-order logic, including machine verified proofs of all the theorems, is available here.

Comment by Ramana Kumar (ramana-kumar) on Time in Cartesian Frames · 2021-03-29T18:26:37.508Z · LW · GW

"subagent [] that could choose " -- do you mean  or  or neither of these? Since  is not closed under unions, I don't think the controllables version of "could choose" is closed under coarsening the partition. (I can prove that the ensurables version is closed; but it would have been nice if the controllables version worked.)

ETA: Actually controllables do work out if I ignore the degenerate case of a singleton partition of the world. This is because, when considering partitions of the world, ensurables and controllables are almost the same thing.

Comment by Ramana Kumar (ramana-kumar) on Thoughts on Human Models · 2021-02-23T12:48:58.190Z · LW · GW

because whereas math-proof data-centers might result in our inadvertent death, something that refers to what humans want might result in deliberate torture.

I want to note that either case of screwing up this badly currently feels pretty implausible to me.

Comment by Ramana Kumar (ramana-kumar) on Thoughts on Human Models · 2021-02-23T12:45:23.961Z · LW · GW

Great summary!

Comment by Ramana Kumar (ramana-kumar) on Time in Cartesian Frames · 2021-02-22T11:46:55.536Z · LW · GW

I have something suggestive of a negative result in this direction:

Let  be the prime-detector situation from Section 2.1 of the coarse worlds post, and let  be the (non-surjective) function that "heats" the outcome (changes any "C" to an "H"). The frame  is clearly in some sense equivalent to the one from the example (which deletes the temperature from the outcome) -- I am using my version just to stay within the same category when comparing frames. As a reminder, primality is not observable in  but is observable in .
Claim: No frame of the form  is biextensionally equivalent to
Proof Idea

The kind of additional observability we get from coarsening the world seems in this case to be very different from the kind that comes from externalising part of the agent's decision.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-02-11T08:29:17.053Z · LW · GW

With the other problem resolved, I can confirm that adding an  escape clause to the multiplicative definitions works out.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-02-11T08:25:29.721Z · LW · GW

Using the idea we talked about offline, I was able to fix the proof - thanks Rohin!
Summary of the fix:
When  and  are defined, additionally assume they are biextensional (take their biextensional collapse), which is fine since we are trying to prove a biextensional equivalence. (By the way this is why we can't take , since we might have  after biextensional collapse.) Then to prove , observe that for all  which means , hence  since a biextensional frame has no duplicate columns.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-02-05T10:59:31.881Z · LW · GW

I presume the fix here will be to add an explicit  escape clause to the multiplicative definitions. I haven't been able to confirm this works out yet (trying to work around this), but it at least removes the  counterexample.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-02-05T09:55:33.395Z · LW · GW

How is this supposed to work (focusing on the  claim specifically)?

and so

Thus, .

Earlier,  was defined as follows:

given by  and

but there is no reason to suppose  above.

Comment by Ramana Kumar (ramana-kumar) on Time in Cartesian Frames · 2021-02-04T08:41:56.604Z · LW · GW

It suffices to establish that

I think the  and  here are supposed to be  and

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-30T13:50:57.192Z · LW · GW

Indeed I think the  case may be the basis of a counterexample to the claim in 4.2. I can prove for any (finite)  with  that there is a finite partition  of  such that 's agent observes  according to the assuming definition but does not observe  according to the constructive multiplicative definition, if I take

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-30T09:21:39.636Z · LW · GW

Let

nit:  should be  here

and let  be an element of .

and the second  should be . I think for these  and  to exist you might need to deal with the  case separately (as in Section 5). (Also couldn't you just use the same  twice?)

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-30T00:12:52.641Z · LW · GW

UPDATE: I was able to prove  in general whenever  and  are disjoint and both in , with help from Rohin Shah, following the "restrict attention to world " approach I hinted at earlier.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-29T19:23:42.718Z · LW · GW

this is clearly isomorphic to , where , where . Thus, 's agent can observe  according to the nonconstructive additive definition of observables.

I think this is only true if  partitions , or, equivalently, if  is surjective. This isn't shown in the proof. Is it supposed to be obvious?

EDIT: may be able to fix this by assigning any  that is not in  to the frame  so it is harmless in the product of s -- I will try this.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-29T10:52:33.342Z · LW · GW

And it seems we do actually need  in the proof to justify:

Thus it suffices to show that .

Without it, we have to show  instead.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-29T08:26:06.384Z · LW · GW

Because  and  are not a partition of the world here.

EDIT: but what we actually need in the proof is  where the  do result in a partition, so I think this will work out the same as the other comment. I'm still not convinced about biextensional equivalence between the frames without the rest of the product.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-28T12:40:18.696Z · LW · GW

I haven't yet figured out why it's true under  - I'll keep trying, but let me know if there's a quick argument for why this holds. (Default next step for me would be to see if I can restrict attention to the world  then do something similar to my other comment.)

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-26T18:53:34.223Z · LW · GW

and observe that

This cannot be true. I can prove in general  whenever  by observing that the agent cardinalities on each side differ.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-26T18:22:36.405Z · LW · GW

where (C),

Presumably two of those indices should be

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-26T14:19:37.813Z · LW · GW

Let . Thus, we also have that

I'm not seeing why this follows. I'll look for a counterexample, but in the meantime maybe there's a simple explanation for why we can combine the product of two assumes as an assume of the union? (I think the only relevant assumption in this context is that the s partition the world; but I might be missing some other important assumption.)

EDIT: I can see how maybe this will follow from the definition of observability of a partition from subsets (which we are also assuming) and the fact that  is closed under union... will try to figure that out. -- Yep I think this works out. Sorry for the confusion.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-26T10:44:59.899Z · LW · GW

Let , and let

Is  supposed to be  here, rather than including ?

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-24T15:50:51.452Z · LW · GW

Next, assume that 's agent can observe  according to the additive definition. We will show that 's agent can observe .

I might be misunderstanding this, but the proof suggests you're actually assuming the assuming definition here, not the additive definition. In which case we may be missing the proof of implication of any of the other definitions from the additive definition.

Comment by Ramana Kumar (ramana-kumar) on Eight Definitions of Observability · 2021-01-24T08:11:29.386Z · LW · GW

Definition: We say that 's agent can observe a finite partition  of  if for all functions , there exists an element  such that for all .

Claim: This definition is equivalent to the definition from subsets.

This doesn't hold in the degenerate case , since then we have an empty function  but no elements of . (But the definition from subsets holds trivially.)

Comment by Ramana Kumar (ramana-kumar) on Committing, Assuming, Externalizing, and Internalizing · 2021-01-23T16:24:39.009Z · LW · GW

Claim: For any Cartesian frame  over  and partition  of , let  send each element of  to its part in . If for all  and  we have , then .

I think this may also need to assume that  is non-empty.

Comment by Ramana Kumar (ramana-kumar) on Committing, Assuming, Externalizing, and Internalizing · 2021-01-23T09:08:35.965Z · LW · GW

If

The  argument is missing in several places like this from 4.2 onwards.

Comment by Ramana Kumar (ramana-kumar) on Committing, Assuming, Externalizing, and Internalizing · 2021-01-23T06:03:37.212Z · LW · GW

is given by

There's a prime missing on . I'd also have expected  instead of  as the variable (doesn't affect correctness).

Comment by Ramana Kumar (ramana-kumar) on Committing, Assuming, Externalizing, and Internalizing · 2021-01-22T18:00:58.207Z · LW · GW

while  is given by

should be applied to  above, I think

Comment by Ramana Kumar (ramana-kumar) on Committing, Assuming, Externalizing, and Internalizing · 2021-01-22T13:48:25.786Z · LW · GW

Let , send each element of  to its part in , so .

Presuming the  here should be a

Comment by Ramana Kumar (ramana-kumar) on Committing, Assuming, Externalizing, and Internalizing · 2021-01-22T08:50:25.359Z · LW · GW

Oh I see this has also been fixed. Thanks!

Comment by Ramana Kumar (ramana-kumar) on Committing, Assuming, Externalizing, and Internalizing · 2021-01-22T08:45:24.911Z · LW · GW

This is also suspicious in section 2.2 about Assuming. I think it should be the other way around and about Assume rather than Commit, and I don't think that's equivalent to what's written here. (But I'm not confident about this.)

Claim: For all  and .

Comment by Ramana Kumar (ramana-kumar) on Committing, Assuming, Externalizing, and Internalizing · 2021-01-21T12:05:16.405Z · LW · GW

Claim: For all  and

Are these the wrong way around?

I believe  is indeed trivial, but the opposite is less obvious.

Comment by Ramana Kumar (ramana-kumar) on Committing, Assuming, Externalizing, and Internalizing · 2021-01-21T11:54:36.580Z · LW · GW

Similarly, for all  and .

We don't need  to be a proper subset here (i.e., I think  is a typo for ). Also in my view all the isomorphisms in this section are actually equalities (but it's also reasonable to never consider equality of frames).

Comment by Ramana Kumar (ramana-kumar) on Additive and Multiplicative Subagents · 2021-01-20T17:34:24.929Z · LW · GW

We let , where

minor typo: I think  should be  above.

Comment by Ramana Kumar (ramana-kumar) on Additive and Multiplicative Subagents · 2021-01-19T19:02:22.102Z · LW · GW

I'm not sure why you started using the equivalence symbol on morphisms, e.g.,

in the categorical definition of multiplicative subagent.

I think equality () is the correct concept to be using here instead, as in the categorical definition of (original) subagent.

Comment by Ramana Kumar (ramana-kumar) on Additive and Multiplicative Subagents · 2021-01-19T15:01:27.522Z · LW · GW

and let  and  compose to something homotopic to the identity in both orders.

Pretty sure the s should be s here (though they're notation for the same function anyway).

Comment by Ramana Kumar (ramana-kumar) on Sub-Sums and Sub-Tensors · 2021-01-14T06:30:34.058Z · LW · GW

In the first claim of 3.4, the last bit of the claim is  but the proof actually shows .

Comment by Ramana Kumar (ramana-kumar) on Multiplicative Operations on Cartesian Frames · 2020-12-20T07:15:56.214Z · LW · GW

a few more typos. (do say if these nits aren't wanted.)

is the natural bijection

(should be: )

while the right hand side is

(should be: in )

Comment by Ramana Kumar (ramana-kumar) on Introduction to Cartesian Frames · 2020-12-17T15:26:39.953Z · LW · GW

To see that some restriction is required here (not imposed by HOL), consider that if  may contain arbitrary Cartesian frames over  then we would have an injection  that, for example, encodes a set  as the Cartesian frame  with  (the environment and evaluation function are unimportant), which runs afoul of Cantor's theorem regarding the cardinality of .

I wouldn't be surprised if a similar encoding/injection could be made using just the operations used to construct Cartesian frames that appear in this sequence - though I have not found one explicitly myself yet.

Comment by Ramana Kumar (ramana-kumar) on Multiplicative Operations on Cartesian Frames · 2020-12-17T14:49:18.012Z · LW · GW

Since we have already established commutativity, it suffices to show that .

For the confused reader, the argument in more detail here is:

where  is commutativity of tensor,  is the fact claimed to suffice above, and  is the implicitly assumed lemma that  and  implies  (this is proved later but only for ).

Comment by Ramana Kumar (ramana-kumar) on Multiplicative Operations on Cartesian Frames · 2020-12-16T08:46:05.321Z · LW · GW

minor typo in the indices here:

We will show that , and since the definition of  is symmetric in swapping  and , it will follow that

Comment by Ramana Kumar (ramana-kumar) on Functors and Coarse Worlds · 2020-12-10T00:18:41.746Z · LW · GW

Nice! I'm glad I asked, since I hadn't realised those sufficient conditions for being homotopic to the identity. That's useful in several proofs I suspect. (For anyone following along, I believe this only holds for a morphism from a frame to itself.)

Comment by Ramana Kumar (ramana-kumar) on Functors and Coarse Worlds · 2020-12-09T18:22:14.889Z · LW · GW

minor typo:

and take  to be the set of all  such that

should have

Also I think later in that proof some of the 's (like in ) should be 's instead.

Comment by Ramana Kumar (ramana-kumar) on Introduction to Cartesian Frames · 2020-12-05T08:34:02.460Z · LW · GW

Do we lose much by restricting attention to finite Cartesian frames (i.e., with finite agent and environment)? I ask because I'm formalising these results in higher-order logic (HOL), and the category