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