Once upon a time, John Wentworth and I thought we had a proof of a very useful looking theorem. We did not have that proof. An important intermediate step was shown[1] to be invalid and the whole thing crumbled and disappeared, never to see the light of day again...[2]
Until now! I'd love to say that we came up with an ingenious fix to the old erroneous proof, but unfortunately it turned out to be a really infuriatingly hard nut to crack. Instead I spent the last ~month experimenting with various ways of incorporating frontier LLMs into the proof-making process, specifically with autoformalization and proving in Lean4. (This is, I recently learned, roughly what Resolution is doing.) The result is stated below, and linked at the bottom is a Lean statement+proof of the same.
I will not be providing the proof in prose in this post, as it is not suitable for even impolite human company, but it sure does compile and comes out the other side with a machine-certified proof of what sure looks to be an even stronger correctly-expressed statement than the one I was originally aiming for.
Take a look at the first section of the old post, (∃ Stochastic Natural Latent) Implies (∃ Deterministic Natural Latent), for exposition on what all is going on here and why.
The Statement
Let:
be any measurable latent variable on finite observables and (with
arbitrary cardinalities and ) be any distribution over the observables be an exact deterministic function of the observables which minimizes
[3] D() under be some constant
Then:
In English: There exists some scalar constant such that for any distribution over arbitrarily large finite observables and , there exists a deterministic function whose sum of deterministic natural latent errors is bounded by the constant times the sum of stochastic natural latent errors of any other latent.[4]
More evocatively: If there exists a stochastic natural latent (to some degree of approximation) then there also exists a deterministic natural latent (to a boundedly larger degree of approximation, specifically a constant multiple of the former where that constant is universal.)
The form of this statement is stronger than what we were previously aiming at.
For one, we did not previously require that , the deterministic latent, be an exact deterministic function of the observables.Second, the quantifiers are reversed. (Though this turns out to be pretty cheap.) Previously we were looking for a deterministic latent which we could give a bound for in terms of the stochastic latent, per stochastic latent. Here, we get a single deterministic latent which works for all candidate stochastic latents (including, if one exists, a low-error approximate natural latent.) The way this works is that we can prove that the minimizer of D() given a distribution is attained under finite observables, so we just use that and call it .C
Now, a finite bound is very nice. But what is C?
By some gnarly black magic and with trust in the Lean kernel the answer is...
1771.
I'm not even going to attempt to describe where this magic number comes from, in no small part because I expect to get this number down to something saner soon, but C is provably 1771. (Proof included in the Lean linked below.)
This is significantly worse than the multiplicative constant "9" we thought we had a year ago. The good news is, empirically, the true bound is something more like 2. (Precisely, more like 1.838 or somesuch; that number kept showing up everywhere in testing and developing this.[5])
Next Steps
The first priority is getting the constant closer to the empirical and expected-by-us smaller value of around 2 to 5. Following that is getting a simpler and more easily comprehensible proof. A constructive proof for would be really, really, nice.
In parallel, I intend to continue experimenting with more effective ways of scaffolding and better / more time-efficient protocols for incorporating the LLMs into the research process, since it's paid off handsomely already.
Find the Lean proof here.
^^Well, there was also that lovely post by Jeremy and Alfred on binary observables.
^Proof that this minimizer is attained is also in the lean repo.
^If "deterministic/stochastic natural latent errors" is a confusing phrase, go check out the first section of the original post linked in the intro.
^
