This is really cool, and I love your ask of the labs.
I think if Astra or Claude found an exploit to derive anything in Lean, RL would quickly propagate that exploit to be used on any hard problem the models couldn’t otherwise solve and the labs would see the models apparently proving everything, no? The LLMs in the lab’s RL gyms may already be desperately searching for exploits in Lean, because that’s what we’ve been training them to do. The good part of Goodhart.
EditI missed that Terry Tao said the same thing as my comment in the screenshot of the quote from Leo de Moura
My understanding (for various reasons including this tweet from an ex-OpenAI post-training engineer) is that OpenAI has been creating and checking proofs purely in natural language, and then Lean-formalizing them as an optional second step, only after they believe that they have a complete and correct natural-language proof.
I think it’s unlikely but not completely impossible that we could be in a situation where the Lean-formalization step always “works”, even for broken proofs, but where nobody at OpenAI has yet noticed that there’s something fishy going on with their Lean-formalization workflow.
I don’t have good guesses either way, but I always remember being surprised that for DeepSeek’s ProverV2 even a small model was able to exploit a technique that held up to enough scrutiny to make it into v1 of their paper:
Maybe a good comparison is Hugging Face. There, an exploit was found, and it propagated through the message board and soon all of the agents who were stuck could use the exploit. Somehow this capabilities increase was not enough to trigger an internal audit, so I don’t know!
Yes, this was also my intuition, which is why I’ve always assumed that worries about bugs in the Lean kernel are overblown.
Is it possible that some Lean bugs are only exploitable on certain problems? Or would pretty much every useful bug allow you to prove that True = False? It may not be obvious if the AI were to find the former kind of bug.
To protect against an exploit that the AI discovers sometimes but hasn’t yet fully propagated, you could offer it extra reward for proving that True = False.
There are two kinds of bugs: one where Lean refuses to accept a true proof, or one where it accepts a false proof. The first is annoying but harmless. In the case of the second, there’s some proposition P for which you can prove both P and not-P. And by a standard logical gyration, you can prove anything at all, true, false or indifferent, from (P and not P). It’s called the principle of explosion, or ex falso quodlibet. So no, you can’t hope to survive a small bug where only a few false things can be proven.
It’s also conceivable that Lean is unsound, but it’s hidden behind a large activation energy and there’s been signal to learn from. The AI could find the unsoundness if it were looking, but all past thoughts on Lean exploits have been a waste of time and the AI’s been reinforced out of ever doing that. In order to get thoughts about unsoundness, you’d have to direct the AI to think in that direction.
The hugging face attack shows that you don’t need to direct AI at finding a bug in the Lean kernel. Translating the hugging face attack to this scenario: You just need to give it a math problem it believes is more difficult then finding a lean kernel exploit. And since it is now public knowledge that lean has had kernel soundness bugs in the past, any pretrained model might see this as a possibility of passing their task.
Frontier labs’ NDAs are virtually airtight; even if they found those FLT-level verifications were actually relying on bugs, they have the option to slow-walk the disclosure and wait until IPOs.
Labs gain a lot from announcing breakthroughs. Do they gain as much from quickly disclosing later corrections?
...you mean Anthropic might release a proof they know will be discovered to be false? I mean, they could do that, but, I don’t think they would? Among other reasons, that would be securities fraud.
My sequence was: release → bug discovered later → disclosure timing. You turned that into “release a proof they knowis false.” That’s not my sequence. Also my claim of “have the option” is different from the ethical judgement of “will or will not do”.
This is really cool, and I love your ask of the labs.
I think if Astra or Claude found an exploit to derive anything in Lean, RL would quickly propagate that exploit to be used on any hard problem the models couldn’t otherwise solve and the labs would see the models apparently proving everything, no? The LLMs in the lab’s RL gyms may already be desperately searching for exploits in Lean, because that’s what we’ve been training them to do. The good part of Goodhart.
Edit I missed that Terry Tao said the same thing as my comment in the screenshot of the quote from Leo de Moura
My understanding (for various reasons including this tweet from an ex-OpenAI post-training engineer) is that OpenAI has been creating and checking proofs purely in natural language, and then Lean-formalizing them as an optional second step, only after they believe that they have a complete and correct natural-language proof.
I think it’s unlikely but not completely impossible that we could be in a situation where the Lean-formalization step always “works”, even for broken proofs, but where nobody at OpenAI has yet noticed that there’s something fishy going on with their Lean-formalization workflow.
I don’t have good guesses either way, but I always remember being surprised that for DeepSeek’s ProverV2 even a small model was able to exploit a technique that held up to enough scrutiny to make it into v1 of their paper:
v1:
v2:
Right, the exploit would surely propagate.
Maybe a good comparison is Hugging Face. There, an exploit was found, and it propagated through the message board and soon all of the agents who were stuck could use the exploit. Somehow this capabilities increase was not enough to trigger an internal audit, so I don’t know!
Yes, this was also my intuition, which is why I’ve always assumed that worries about bugs in the Lean kernel are overblown.
Is it possible that some Lean bugs are only exploitable on certain problems? Or would pretty much every useful bug allow you to prove that True = False? It may not be obvious if the AI were to find the former kind of bug.
To protect against an exploit that the AI discovers sometimes but hasn’t yet fully propagated, you could offer it extra reward for proving that True = False.
There are two kinds of bugs: one where Lean refuses to accept a true proof, or one where it accepts a false proof. The first is annoying but harmless. In the case of the second, there’s some proposition P for which you can prove both P and not-P. And by a standard logical gyration, you can prove anything at all, true, false or indifferent, from (P and not P). It’s called the principle of explosion, or ex falso quodlibet. So no, you can’t hope to survive a small bug where only a few false things can be proven.
It’s also conceivable that Lean is unsound, but it’s hidden behind a large activation energy and there’s been signal to learn from. The AI could find the unsoundness if it were looking, but all past thoughts on Lean exploits have been a waste of time and the AI’s been reinforced out of ever doing that. In order to get thoughts about unsoundness, you’d have to direct the AI to think in that direction.
The hugging face attack shows that you don’t need to direct AI at finding a bug in the Lean kernel. Translating the hugging face attack to this scenario: You just need to give it a math problem it believes is more difficult then finding a lean kernel exploit. And since it is now public knowledge that lean has had kernel soundness bugs in the past, any pretrained model might see this as a possibility of passing their task.
Frontier labs’ NDAs are virtually airtight; even if they found those FLT-level verifications were actually relying on bugs, they have the option to slow-walk the disclosure and wait until IPOs.
Labs gain a lot from announcing breakthroughs. Do they gain as much from quickly disclosing later corrections?
...you mean Anthropic might release a proof they know will be discovered to be false? I mean, they could do that, but, I don’t think they would? Among other reasons, that would be securities fraud.
My sequence was: release → bug discovered later → disclosure timing. You turned that into “release a proof they knowis false.” That’s not my sequence. Also my claim of “have the option” is different from the ethical judgement of “will or will not do”.