I don’t know that MIRI actually believes that what we need to do is write a bunch of proofs about our AI system, but it sure sounds like it, and that seems like a too difficult, and basically impossible task to me, if the proofs that we’re trying to write are about alignment or beneficialness or something like that.
FYI: My understanding of what MIRI (or at least Buck) thinks is that you don’t need to prove your AI system is beneficial, but you should have a strong argument that stands up to strict scrutiny, and some of the sub-arguments will definitely have to be proofs.
RS Seems plausible, I think I feel similarly about that claim
DF
FYI: My understanding of what MIRI (or at least Buck) thinks is that you don’t need to prove your AI system is beneficial, but you should have a strong argument that stands up to strict scrutiny, and some of the sub-arguments will definitely have to be proofs.
RS Seems plausible, I think I feel similarly about that claim