The quick, lacking-all-nuance answer: one of the main things we’re worried about with AI safety is that we can’t write down a specification of what we want for an AI to optimize. Formal methods typically require such a specification.
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 :) I don’t think formal methods are likely to be a magic bullet for AI safety. However, if one wants a provably safe AI, it seems like developing the capability to write provably correct software in easier cases could be a good first step (a necessary but not sufficient condition, if you will), and the article discusses our progress towards that goal. The article also discusses the specification problem a bit, and it seems plausible that insights from how to do formal specifications for software in general will transfer to FAI. The field seems neglected in general, relative to something like machine learning: “There really isn’t a formal methods community so much as a few tiny bands foraging in the Steppe”. Finally, my own personal judgement: the “writing down a specification of what we want for an AI to optimize” part seems like it might be more amenable to being solved with a sudden flash of insight (in the same way Nick Bostrom has suggested that the problem of AGI more generally might be solved with a sudden flash of insight), whereas the problem of formally verifying software seems less like that, and if it ends up being a long slog, it might actually constitute the majority of the problem. So for those reasons, it seemed to me like LW might benefit from additional formal verification awareness/discussion.
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.
I think some people do, or at least try to, but my impression of the state of computer-assisted proofs and formal verification methods for programs is that they are still not very good because the problem is incredibly complex and we’ve basically only made it to the level of having FORTRAN-level tools. This is to say, we’re a bit better off than we used to be doing formal verification with assembly-level tools where you had to specify absolutely everything in very low-level terms, but mostly in ways that just make it easier to do that low-level work rather than having many useful abstractions to help us perform formal verification without having to understand the details of (almost) everything all the time.
To continue the analogy, things will get a little more exciting as we get C and then C++ level tools, but I think things won’t really explode and be appealing to many folks who don’t desperately need to do formal verification until we get to something like the Python/Ruby-level in terms of tooling.
This does suggest something interesting, though: if someone thinks more widely using formal verification is important, especially in AI, then a straight-forward approach is to work on improving formal verification tools to a point that they can build up the abstractions that will help people work with them.
The quick, lacking-all-nuance answer: one of the main things we’re worried about with AI safety is that we can’t write down a specification of what we want for an AI to optimize. Formal methods typically require such a specification.
(Though note Techniques for optimizing worst-case performance includes verification as a potential avenue of attack.)
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 :) I don’t think formal methods are likely to be a magic bullet for AI safety. However, if one wants a provably safe AI, it seems like developing the capability to write provably correct software in easier cases could be a good first step (a necessary but not sufficient condition, if you will), and the article discusses our progress towards that goal. The article also discusses the specification problem a bit, and it seems plausible that insights from how to do formal specifications for software in general will transfer to FAI. The field seems neglected in general, relative to something like machine learning: “There really isn’t a formal methods community so much as a few tiny bands foraging in the Steppe”. Finally, my own personal judgement: the “writing down a specification of what we want for an AI to optimize” part seems like it might be more amenable to being solved with a sudden flash of insight (in the same way Nick Bostrom has suggested that the problem of AGI more generally might be solved with a sudden flash of insight), whereas the problem of formally verifying software seems less like that, and if it ends up being a long slog, it might actually constitute the majority of the problem. So for those reasons, it seemed to me like LW might benefit from additional formal verification awareness/discussion.
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!
I think some people do, or at least try to, but my impression of the state of computer-assisted proofs and formal verification methods for programs is that they are still not very good because the problem is incredibly complex and we’ve basically only made it to the level of having FORTRAN-level tools. This is to say, we’re a bit better off than we used to be doing formal verification with assembly-level tools where you had to specify absolutely everything in very low-level terms, but mostly in ways that just make it easier to do that low-level work rather than having many useful abstractions to help us perform formal verification without having to understand the details of (almost) everything all the time.
To continue the analogy, things will get a little more exciting as we get C and then C++ level tools, but I think things won’t really explode and be appealing to many folks who don’t desperately need to do formal verification until we get to something like the Python/Ruby-level in terms of tooling.
This does suggest something interesting, though: if someone thinks more widely using formal verification is important, especially in AI, then a straight-forward approach is to work on improving formal verification tools to a point that they can build up the abstractions that will help people work with them.