FYI, the reason the post is titled “Why don’t people use formal methods?” is because that is what the link is called, not because I was wondering why people in AI safety don’t use formal methods :)
Got it, my mistake.
“There really isn’t a formal methods community so much as a few tiny bands foraging in the Steppe”
I’ve got to disagree with that, I used to be very closely adjacent to the formal methods community, if not a part of it myself. It’s much bigger than eg. the academic AI safety community. Sure, it’s not as big as ML, but almost nothing is as big as ML.
The rest of the reasons seem reasonable. I personally disagree that the capability to write provably correct software in easier cases is a necessary first step, but I don’t think I have particularly strong explicit reasons for that position.
ETA: Also I do know a few AI safety people explicitly excited about formal methods and verification who will likely be working on it in the near future, if not already.
Got it, my mistake.
I’ve got to disagree with that, I used to be very closely adjacent to the formal methods community, if not a part of it myself. It’s much bigger than eg. the academic AI safety community. Sure, it’s not as big as ML, but almost nothing is as big as ML.
The rest of the reasons seem reasonable. I personally disagree that the capability to write provably correct software in easier cases is a necessary first step, but I don’t think I have particularly strong explicit reasons for that position.
ETA: Also I do know a few AI safety people explicitly excited about formal methods and verification who will likely be working on it in the near future, if not already.
Thanks for the info!