Really awesome post. Just some questions below because the 2% you gave is rather low and my personal estimate would easily be off by an order of magnitude (closer to 20%). So the questions below are meant to see where that difference is coming from.
”I am 2% certain that we will soon be putting huge amounts of trust into Lean4 certificates produced by misaligned AIs.”
Can I ask you more precisely where your 2% is coming from? I.e. can you give some separate odds for the two closely related statements?
1) We will soon be putting huge amounts of trust into Lean4 certificates.
2) We will soon be using misaligned AI’s to generate lean certificates.
I’m also curious what is meant by misaligned AI in this post, i.e. how severely misaligned does it have to be? I.e. in the context of the post there are two reasonable interpretations
a) The AI is happy to exploit a kernel bug and use it to claim it found a proof of mathematical theorem.
b) The AI is misaligned in such a way that it actually is likely to lead to an existential catastrophe when it is allowed to recursively self improve?
Or did you have something in mind somewhere between a and b? As this chance severely depends on how misaligned one would require the ai to be.
I think interpretation a) is reasonable since the post is about lean4. While interpretation b) is reasonable since you speak about pivotal act.
Also regarding the lean certificates, will it be lean certificates of just mathematical theorems that the math community cares about. Or will it be lean certificates of statements that are relevant for alignment research?
Maarten Derickx
Karma: 6
Is there a way of finding a list of guarded definitions on which the lesswrong community has settled on a meaning? I know https://www.lesswrong.com/w/pivotal-act is labeled as such. It would be helpful for me if this page would contain a short description how to find guarded definitions on this website.
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.