We endorse pointing out harmful actions. But we condemn attacks on people’s character.
I am not a fan of Holly Elmore but surely it’s absurd to make this distinction! It’s perfectly reasonable to think someone’s harmful actions reflect poorly on their character.
In fact, one of the best kinds of evidence we have with which to judge someone’s character is their actions.
I mean, they are pretty generic effects of increased sympathetic nervous system activity. Among other things:
Increased heartrate
Shallower breathing
Sweating
Increased muscle tension
Nausea
Does jealousy have a physical correlate? That is, if you imagine being really jealous can you track what changes in how your body feels, like how anger raises your heart rate and tenses your muscles?
Yes, it definitely does have a physical correlate!
Oftentimes I see people use the word corrigibility to describe a model which doesn’t have a strong set of values instilled by its creator, and instead is aligned to the intent of whoever is prompting the model.
E.g. @Nina Panickssery in this shortform: “People underrate the extent to which intent alignment/corrigibility (I use these terms interchangeably) and value alignment are at odds with each other.”
I think corrigibility is in a sense a more general property than so-called intent alignment, as a corrigible agent could still be aligned to its creator rather than to user intent.
Nina’s use of the word corrigibility is quite different from the way it was originally intended, namely that one should build a machine intelligence which understands that it may be somehow flawed. A hoped-for route to corrigibility is to build an agent that has an implicit specification of its goals but doesn’t know what the explicit specification is. This implicit specification, importantly, points to something which may change over time, and the specification tracks that changeable thing; and yet the machine intelligence should not try to change nor freeze the thing its pointer points to.
Someone could make a machine intelligence that is corrigible in this way, but point the source of value at nearly anything; it need not be the intent of the user, it could be the intent of the creator. In fact the original 2015 MIRI paper always describes the correction target of corrigible agents as the creator, and two years later Paul Christiano’s 2017 post starts using the words user and overseer instead.
Separately, even if your particular alignment scheme lets you specify value explicitly or implicitly by pointing at some immutable thing, user-intent alignment is not a target you will necessarily be able to align to, as it is impossible to find some immutable way to describe intent alignment. Therefore you do need corrigibility as a prerequisite for user-intent alignment.
I didn’t mean to imply that it was in the paper as I have it, that’s why I said based on instead of from, sorry if that was confusing. It’s a presentational thing and it’s fine to just use
I don’t see how there’s an implicit optimality assumption unless you’re trying to read quantities at every step in the proof as a program length. I agree that there’s something aesthetically worse about a proof that routes through something less nicely interpretable.
96: https://github.com/DLorell/stoch_to_det/pull/5
Happy to finally be down to double digits. I am optimistic that single digits is not that far off.
It’s not a textbook definition but it is based on Chaitin, G. J. (1975). “A Theory of Program Size Formally Identical to Information Theory.” (link)
Here’s the idea:
You have
You don’t have to interpret
If we start with the latent string model assumptions you already have, then you can work in
I’ve been working on a condensation post which includes a proposal for algorithmic condensation. My version mostly matches yours, but one important difference is that I use
I’m curious what you think of this… I’m still getting comfortable working with AIT so I’m not super confident of this but it seems to work...
The repo is updated with the full redundancy deletion spectrum, so we’ve got formalized proofs of bounds for weak natural latents and strong natural latents and everything in between.
It does use a sum of KL divergence errors, but embarrassingly I’m noticing just now that originally the proof implied a bound for weak natural latents (all-but-one redundancy) instead of strong natural latents (any-one-redundancy) which is what I intended. Bound for strong natural latents is underway, I think the proof is pretty quick but lean formalization will take a minute.
Thanks primarily to GPT 5.6 I’ve got a Lean proof of a bound which works for any number of observables (the bound is in terms of the number of variables): https://github.com/satchlj/general_stoch_to_det
I’ve looked at the formalization of the statements and definitions and am happy with them.
New lean proof of 517 bound: https://github.com/DLorell/stoch_to_det/pull/3
Yeah thanks, that version is indeed false, but I’ve been looking at a weakened version which might be true which I still like better than the sum version because it seems cleaner. I’ll write the conjecture up formally when I get the chance.
It’s funny how I’ve spent so many tokens (not much of my own time) on this problem even though I really don’t think it’s particularly important for the broader natural abstractions agenda relative to lots of other stuff, but it’s been a fun challenge, definitely one of the trickier formal math problems that’s been come across in this area.
I’ve got it up to 1.96
I see, yeah—I wonder if it’s 2.
Could you explain the reason you think the correct lower bound is higher than 1.838?
Edit: Looks like it’s at least 1.948: https://github.com/satchlj/stoch-to-det-lower
So I’ve been looking at this and I do not like how it’s proved for the sum of the errors. I would much rather have a stronger result which holds an upper bound on the conditional mutual information of X and Y fixed and then certifies the deterministic redundancy error in terms of the stochastic redundancy error. If this version of the conjecture is false then it would be useful to understand how.
If I get more insight into this, I will post an update here.
I’m also trying to extend the result to settings with more than two observables, which seems like it should be pretty straightforward but I can’t be sure yet.
Fable has got the OG bound down to 698 btw. I will put a pull request on the GitHub in a couple hours.
Edit: https://github.com/DLorell/stoch_to_det/pull/2
Wow! Awesome news! I had been trying to get the robots to prove this as a way to use up tokens before my weekly resets but hadn’t managed to get them to succeed. I’m gonna look at how this can be extended / what I can learn from the Lean.
@Yair Halberstadt British Airways just paid me over £1,000. I don’t think this would have happened had you not written this post. Thank you.