You know what, I’ve identified a scenario where formal verification is both tractable and helps reduce AI risk, and the broad answer is making our codebases way more secure and controllable, assuming heavy AI automation of mathematics and coding is achieved (which I expect to happen before they can do everything else, as it’s a domain with strong feedback loops, easy verification against ground truth possible, and you can get very large amounts of data to continually improve.)
I’ve also discussed more about the value and limits of formal proofs in another comment below, but short answer, it’s probably really helpful in an infrastructure sense, but not so much as a means to make anything other than software and mathematics safe and formally specified (which would be a huge win if we could do that in itself), but we will not be able to prove stuff like a piece of software isn’t a threat to something else in the world entirely, and that also applies to biology in say determining whether a gene or virus will harm humans, mostly because we don’t have a path to quantify all possible higher-order behaviors a system doesn’t have:
You know what, I’ve identified a scenario where formal verification is both tractable and helps reduce AI risk, and the broad answer is making our codebases way more secure and controllable, assuming heavy AI automation of mathematics and coding is achieved (which I expect to happen before they can do everything else, as it’s a domain with strong feedback loops, easy verification against ground truth possible, and you can get very large amounts of data to continually improve.)
Here are the links below:
https://www.lesswrong.com/posts/oJQnRDbgSS8i6DwNu/the-hopium-wars-the-agi-entente-delusion#sgH9iCyon55yQyDqF
I’ve also discussed more about the value and limits of formal proofs in another comment below, but short answer, it’s probably really helpful in an infrastructure sense, but not so much as a means to make anything other than software and mathematics safe and formally specified (which would be a huge win if we could do that in itself), but we will not be able to prove stuff like a piece of software isn’t a threat to something else in the world entirely, and that also applies to biology in say determining whether a gene or virus will harm humans, mostly because we don’t have a path to quantify all possible higher-order behaviors a system doesn’t have:
https://www.lesswrong.com/posts/oJQnRDbgSS8i6DwNu/the-hopium-wars-the-agi-entente-delusion#2GDjfZTJ8AZrh9i7Y