This post annoyed me. Which is a good thing! It means that you hit where it hurts, and you forced me to reconsider my arguments. I also had to update (a bit) toward your position, because I realized that my “counter-arguments” weren’t that strong.
Still, here they are:
I agree with the remark that many work will have both capability and safety consequences. But instead of seeing that as an argument to laud the safety aspect of capability-relevant work, I want to look for the differential technical progress. What makes me think that EA safety is more relevant than mainstream AI to safety questions is that for almost all EA safety, the differential progress is in favor of safety, while for most research in mainstream/academic AI, the different progress seems either neutral or in favor of capabilities. (I’ll be very interested in counter examples, on both sides)
Echoing what Buck wrote, I think you might overestimate the value of research that has potential consequences about safety but is not about it. And thus I do think there’s a significant value gain to focus on safety problems specifically.
About Formal Methods, it isn’t even useful for AI capabilities, even less for AI safety. I want to write a post about that at some point, but when you’re unable to specify what you want, Formal Methods cannot save your ass.
With all that being said, I’m glad you wrote this post and I think I’ll revisit it and think more about it.
Could you say more (or work on that post) about why formal methods will be unhelpful? Why are places like Stanford, CMU, etc. pushing to integrate formal methods with AI safety? Also Paul Christiano has suggested formal methods will be useful for avoiding catastrophic scenarios. (Will update with links if you want.)
Hum, I think I wrote my point badly on the comment above. What I mean isn’t that formal methods will never be useful, just that they’re not really useful yet, and will require more pure AI safety research to be useful.
The general reason is that all formal methods try to show that a program follows a specification on a model of computation. Right now, a lot of the work on formal methods applied to AI focus on adapting known formal methods to the specific programs (say Neural Networks) and the right model of computation (in what contexts do you use these programs, how can you abstract their execution to make it simpler). But one point they fail to address is the question of the specification.
Note that when I say specification, I mean a formal specification. In practice, it’s usually a modal logic formula, in LTL for example. And here we get at the crux of my argument: nobody knows the specification for almost all AI properties we care about. Nobody knows the specification for “Recognizing kittens” or “Answering correctly a question in English”. And even for safety questions, we don’t have yet a specification of “doesn’t manipulate us” or “is aligned”. That’s the work that still needs to be done, and that’s what people like Paul Christiano and Evan Hubinger, among others, are doing. But until we have such properties, the formal methods will not be really useful to either AI capability or AI safety.
Lastly, I want to point out that working on AI for formal methods is also a means to get money and prestige. I’m not going to go full Hanson and say that’s the only reason, but it’s still a part of the international situation. I have examples of people getting AI related funding in France, for a project that is really, but really useless for AI.
This post annoyed me. Which is a good thing! It means that you hit where it hurts, and you forced me to reconsider my arguments. I also had to update (a bit) toward your position, because I realized that my “counter-arguments” weren’t that strong.
Still, here they are:
I agree with the remark that many work will have both capability and safety consequences. But instead of seeing that as an argument to laud the safety aspect of capability-relevant work, I want to look for the differential technical progress. What makes me think that EA safety is more relevant than mainstream AI to safety questions is that for almost all EA safety, the differential progress is in favor of safety, while for most research in mainstream/academic AI, the different progress seems either neutral or in favor of capabilities. (I’ll be very interested in counter examples, on both sides)
Echoing what Buck wrote, I think you might overestimate the value of research that has potential consequences about safety but is not about it. And thus I do think there’s a significant value gain to focus on safety problems specifically.
About Formal Methods, it isn’t even useful for AI capabilities, even less for AI safety. I want to write a post about that at some point, but when you’re unable to specify what you want, Formal Methods cannot save your ass.
With all that being said, I’m glad you wrote this post and I think I’ll revisit it and think more about it.
Could you say more (or work on that post) about why formal methods will be unhelpful? Why are places like Stanford, CMU, etc. pushing to integrate formal methods with AI safety? Also Paul Christiano has suggested formal methods will be useful for avoiding catastrophic scenarios. (Will update with links if you want.)
Hum, I think I wrote my point badly on the comment above. What I mean isn’t that formal methods will never be useful, just that they’re not really useful yet, and will require more pure AI safety research to be useful.
The general reason is that all formal methods try to show that a program follows a specification on a model of computation. Right now, a lot of the work on formal methods applied to AI focus on adapting known formal methods to the specific programs (say Neural Networks) and the right model of computation (in what contexts do you use these programs, how can you abstract their execution to make it simpler). But one point they fail to address is the question of the specification.
Note that when I say specification, I mean a formal specification. In practice, it’s usually a modal logic formula, in LTL for example. And here we get at the crux of my argument: nobody knows the specification for almost all AI properties we care about. Nobody knows the specification for “Recognizing kittens” or “Answering correctly a question in English”. And even for safety questions, we don’t have yet a specification of “doesn’t manipulate us” or “is aligned”. That’s the work that still needs to be done, and that’s what people like Paul Christiano and Evan Hubinger, among others, are doing. But until we have such properties, the formal methods will not be really useful to either AI capability or AI safety.
Lastly, I want to point out that working on AI for formal methods is also a means to get money and prestige. I’m not going to go full Hanson and say that’s the only reason, but it’s still a part of the international situation. I have examples of people getting AI related funding in France, for a project that is really, but really useless for AI.