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.
Satya Benson
Karma: 366
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.
I think they are (at least OAI). Notably, GPT 5.5 Pro is not on the benchmark.
They are probably referring to these:
AF is kinda a quite broad term, historically has been a lot of decision theory which does tend to make some of the assumptions you are referring to, but thinking about how to model agents more generally is also a core project of agent foundations
I think that the real reason work in agent foundations isn’t that applicable to current models is mostly that it is just a pretty young small field and still has a long way to go. Progress is very much bottlenecked by smart people getting work done, and eventually it absolutely will be able to help us understand LLMs, along with many other kinds of agents.
Could elaborate on why you think that a strong prior against goal-directedness remains after post training?
Here’s what that same distribution I used above looks like if you plot the closed-form pushforward density analytically. In this picture it’s easier for the visual cortex to pick up on the patterns (although it would still be nontrivial for a human to figure out what should be colored red and what should be colored blue if you erased the colors).
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.