All of Ramana Kumar's Comments + Replies

Finite Factored Sets: Conditional Orthogonality

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.

The Blackwell order as a formalization of knowledge

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?

1Alex Flint9dYes. Thank you. Fixed.
Introduction to Cartesian Frames

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

Time in Cartesian Frames

"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, ensur... (read more)

Time in Cartesian Frames

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 ob... (read more)

Eight Definitions of Observability

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

Eight Definitions of Observability

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 ... (read more)

Eight Definitions of Observability

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.

2Ramana Kumar7moWith the other problem resolved, I can confirm that adding anA=∅escape clause to the multiplicative definitions works out.
Eight Definitions of Observability

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.

3Rohin Shah7moThe problem is a bit earlier actually: This isn't true, because∙1doesn't just ignoreb1here (sincer∈R1). I think the route is to say "Leth(b′2)=f2. Then∙1must treatf1andf2identically, meaning that either they are equal, or the frame is biextensionally equivalent to one where they are equal."
Time in Cartesian Frames

It suffices to establish that 

I think the  and  here are supposed to be  and 

Eight Definitions of Observability

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 

2Ramana Kumar8moI presume the fix here will be to add an explicitA=∅escape clause to the multiplicative definitions. I haven't been able to confirm this works out yet (trying to work around this [https://www.lesswrong.com/posts/5R9dRqTREZriN9iL7/eight-definitions-of-observability?commentId=vc7NcsErj4NgWFdTX] ), but it at least removes thenullcounterexample.
Eight Definitions of Observability

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?)

1Ramana Kumar8moIndeed I think theA=∅case may be the basis of a counterexample to the claim in 4.2. I can prove for any (finite)Wwith|W|>1that there is a finite partitionVofW such thatC's agent observesVaccording to the assuming definition but does not observeVaccording to the constructive multiplicative definition, if I takeC=null .
Eight Definitions of Observability

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.
 

Eight Definitions of Observability

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 thi... (read more)

Eight Definitions of Observability

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.

2Ramana Kumar8moUPDATE: I was able to proveAssumeS1(C)&AssumeS2(C)≃AssumeS1∪S2(C)in general wheneverS1andS2are disjoint and both inObs(C), with help from Rohin Shah, following the "restrict attention to worldS1∪S2" approach I hinted at earlier.
Eight Definitions of Observability

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.

2Ramana Kumar8moAnd it seems we do actually needAssumeS1(C)&AssumeS2(C)≃AssumeS1∪S2(C)in the proof to justify: Without it, we have to show(D1&1R2∪R3)⊗(D2&1R1∪R3)≃AssumeS1∪S2(C)&1R3instead.
Eight Definitions of Observability

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.)

2Scott Garrabrant8moI am confused, why is it not identical to your other comment?
Eight Definitions of Observability

and observe that 

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

1Scott Garrabrant8moYep, changed it to≃.
Eight Definitions of Observability

where (C), 

Presumably two of those indices should be 

1Scott Garrabrant8moFixed, thanks.
Eight Definitions of Observability

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... (read more)

Eight Definitions of Observability

Let , and let 

Is  supposed to be  here, rather than including ?

1Scott Garrabrant8moFixed, thanks.
Eight Definitions of Observability

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.

2Scott Garrabrant8moI think I fixed it. Thanks.
Eight Definitions of Observability

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.)

1Scott Garrabrant8moThis was annoying to fix, so I just madeWnonempty in the intro to the post.
Committing, Assuming, Externalizing, and Internalizing

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.

1Scott Garrabrant8moFixed, Thanks
Committing, Assuming, Externalizing, and Internalizing

If 

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

1Scott Garrabrant8moFixed at least some of them.
Committing, Assuming, Externalizing, and Internalizing

 is given by 

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

1Scott Garrabrant8moFixed, thanks.
Committing, Assuming, Externalizing, and Internalizing

while  is given by 

 should be applied to  above, I think

1Scott Garrabrant8moFixed, thanks.
Committing, Assuming, Externalizing, and Internalizing

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

Presuming the  here should be a 

1Scott Garrabrant8moFixed, thanks.
Committing, Assuming, Externalizing, and Internalizing

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 .

1Ramana Kumar8moOh I see this has also been fixed. Thanks!
Committing, Assuming, Externalizing, and Internalizing

Claim: For all  and 

Are these the wrong way around?

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

1Ramana Kumar8moThis 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.)
1Scott Garrabrant8moFixed, Thanks.
Committing, Assuming, Externalizing, and Internalizing

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).

1Scott Garrabrant8moYeah, the⊂was a typo, and I just never consider equality of frames.
Additive and Multiplicative Subagents

We let , where 

minor typo: I think  should be  above.

1Scott Garrabrant8moFixed, Thanks.
Additive and Multiplicative Subagents

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.

3Scott Garrabrant8moI agree that equality is correct. I corrected some instances of≅, but I might have missed some
Additive and Multiplicative Subagents

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).

2Scott Garrabrant8moFixed, Thanks.
Sub-Sums and Sub-Tensors

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

2Scott Garrabrant8moFixed, thanks. The proof was right, and the original claim was trivial.
Multiplicative Operations on Cartesian Frames

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 )

2Scott Garrabrant9moI want and appreciate nits. Fixed.
Introduction to Cartesian Frames

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... (read more)

Multiplicative Operations on Cartesian Frames

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 ).

Multiplicative Operations on Cartesian Frames

minor typo in the indices here:

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

2Ramana Kumar9moa few more typos. (do say if these nits aren't wanted.) (should be:A1) (should be: inS)
1Scott Garrabrant9moFixed, Thanks.
Functors and Coarse Worlds

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.

2Scott Garrabrant9moFixed, Thanks. I think theh's are correct. Any morphism in which either component is the identity must be homotopic to the identity, since homotopic is symmetric. In this proof, checking theh's is easier.
Introduction to Cartesian Frames

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  is too big to represent if it really must contain frames with infinite agents and also for any pair of frames the frame whose agents are the morphisms between them. The root problem is probably that I require any category's class of objects to be a set, but it's hard to avoid this requirement in HOL in a nice way. Everything should work out f... (read more)

2Scott Garrabrant9moI don't think you lose much by focusing on finite Cartesian frames. I have mostly only been imagining finite cases. I think there is some potential for later extending the theory to encompass game theory and probabilistic strategies, and then we might want to think of the infinite space of mixed strategies as the agent, but it wouldn't surprise me if in doing this, we also put continuity into the system and want to assume compactness.
2Ramana Kumar9moTo see that some restriction is required here (not imposed by HOL), consider that ifChu(w)may contain arbitrary Cartesian frames overwthen we would have an injection2Chu(w)→Chu(w)that, for example, encodes a setS⊆Chu(w)as the Cartesian frameCSwithAgent(CS)=S(the environment and evaluation function are unimportant), which runs afoul of Cantor's theorem regarding the cardinality ofChu(w). 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.
Controllables and Observables, Revisited

Counterexample to your claim that  (with both  and  not ):

Take  and  to be the following Cartesian frames over world  with agent and environment both  as the following matrices:

Then  but .

(Sorry for my formatting - I haven't done LaTeX in these comments before.)

Thank You! You are correct. Oops!

I deleted that claim from the post. That was quite a mistake. Luckily it seems self-contained. This is the danger of "Trivial" proofs.

Initial versions of the theory only talked about ensurables, and the addition of (and shift of attention to) controllables came much later.

What is the alternative to intent alignment called?

I would use 'outcome alignment' for 2 (and agree with 'intent alignment' for 1). In other words, I see the important distinction between 'outcome' and 'intent' being in the first part of the options, not the second.

I'd be inclined to see 3 and 4 as variations on 1 and 2 where what the human wants is for the AI to figure out some notion of their true goals and pursue/achieve that.

Example: Markov Chain

Have you seen Erik P Hoel's work on causal abstraction? This post reminded me of it.

Causal Abstraction Toy Model: Medical Sensor

When you talk about counterfactuals do you mean interventions? Although I'm guessing the "everything still works" conclusion holds for both interventions and counterfactuals.

1johnswentworth1yYeah, I have a habit of not distinguishing between the two. At least for most of the problems I think about, as long as we're working with a structural model the difference doesn't really matter.
Name of Problem?

I think this is related to the word problem for the rewriting system defined by your programming language. When I first read this question I was thinking "Something to do with Church-Rosser?" -- but you can follow the links to see for yourself if that literature is what you're after.

Causal Abstraction Intro

Didn't watch the video but would have read the post. Might watch the video only because previous posts have been appetising enough.

Creating Environments to Design and Test Embedded Agents
the objective of agent-designers is to have the agent collect as many agents as possible

Typo: should say "dollars"?

Open question: are minimal circuits daemon-free?
if the daemon is obfuscated, there is no efficient procedure which takes the daemon circuit as input and produces a smaller circuit that still solves the problem.
So we can't find any efficient constructive argument. That rules out most of the obvious strategies.

I don't think the procedure needs to be efficient to solve the problem, since we only care about existence of a smaller circuit (not an efficient way to produce it).

Load More