Mark, have you read Eliezer’s article about the Löbian obstacle, and what was your reaction to it?
I’m in the early stages of writing up my own work on the Löbian obstacle for publication, which will need to include its own (more condensed, rather than expanded) exposition of the Löbian obstacle; but I liked Eliezer’s article, so it would be helpful to know why you didn’t think it argued the point well enough.
Don’t worry, I wasn’t offended :)
Good to hear, and thanks for the reassurance :-) And yeah, I do too well know the problem of having too little time to write something polished, and I do certainly prefer having the discussion in fairly raw form to not having it at all.
One possibility is that MIRI’s arguments actually do look that terrible to you
What I would say is that the arguments start to look really fishy when one thinks about concrete instantiations of the problem.
I’m not really sure what you mean by a “concrete instantiation”. I can think of concrete toy models, of AIs using logical reasoning which know an exact description of their environment as a logical formula, which can’t reason in the way I believe is what we want to achieve, because of the Löbian obstacle. I can’t write down a self-rewriting AGI living in the real world that runs into the Löbian obstacle, but that’s because I can’t write down any AGI that lives in the real world.
My reason for thinking that the Löbian obstacle may be relevant is that, as mentioned in the interview, I think that a real-world seed FAI will probably use (something very much like) formal proofs to achieve the high level of confidence it needs in most of its self-modifications. I feel that formally specified toy models + this informal picture of a real-world FAI are as close to thinking about concrete instantiations as I can get at this point.
I may be wrong about this, but it seems to me that when you think about concrete instantiations, you look towards solutions that reason about the precise behavior of the program they’re trying to verify—reasoning like “this variable gets decremented in each iteration of this loop, and when it reaches zero we exit the loop, so we won’t loop forever”. But heuristically, while it seems possible to reason about the program you’re creating in this way, our task is to ensure that we’re creating a program which creates a program which creates a program which goes out to learn about the world and look for the most efficient way to use transistors it finds in the external environment to achieve its goals, and we want to verify that those transistors won’t decide to blow up the world; it seems clear to me that this is going to require reasoning of the type “the program I’m creating is going to reason correctly about the program it is creating”, which is the kind of reasoning that runs into the Löbian obstacle, rather than the kind of reasoning applied by today’s automated verification techniques.
Writing this, I’m not too confident that this will be helpful to getting the idea across. Hope the face-to-face with Paul with help, perhaps also with translating your intuitions to a language that better matches the way I think about things.
I think that the point above would be really helpful to clarify, though. This seems to be a recurring theme in my reactions to your comments on MIRI’s arguments—e.g. there was that LW conversation you had with Eliezer where you pointed out that it’s possible to verify properties probabilistically in more interesting ways than running a lot of independent trials, and I go, yeah, but how is that going to help with verifying whether the far-future descendant of an AI we build now, when it has entire solar systems of computronium to run on, is going to avoid running simulations which by accident contain suffering sentient beings? It seems that to achieve confidence that this far-future descendant will behave in a sensible way, without unduly restricting the details of how it is going to work, is going to need fairly abstract reasoning, and the sort of tools you point to don’t seem to be capable of this or to extend in some obvious way to dealing with this.
You seem to be quite willing to use that reasoning yourself to show that the initial AI is safe
I’m not sure I understand what you’re saying here, but I’m not convinced that this is the sort of reasoning I’d use.
I’m fairly sure that the reason your brain goes “it would be safe if we only allow self-modifications when there’s a proof that they’re safe” is that you believe that if there’s a proof that a self-modification is safe, then it is safe—I think this is probably a communication problem between us rather than you actually wanting to use different reasoning. But again, hopefully the face-to-face with Paul can help with that.
I don’t think that “whole brain emulations can safely self-modify” is a good description of our disagreements. I think that this comment (the one you just made) does a better job of it. But I should also add that my real objection is something more like: “The argument in favor of studying Lob’s theorem is very abstract and it is fairly unintuitive that human reasoning should run into that obstacle. [...]”
Thanks for the reply! Thing is, I don’t think that ordinary human reasoning should run into that obstacle, and the “ordinary” is just to exclude humans reasoning by writing out formal proofs in a fixed proof system and having these proofs checked by a computer. But I don’t think that ordinary human reasoning can achieve the level of confidence an FAI needs to achieve in its self-rewrites, and the only way I currently know how an FAI could plausibly reach that confidence is through logical reasoning. I thought that “whole brain emulations can safely self-modify” might describe our disagreement because that would explain why you think that human reasoning not being subject to Löb’s theorem would be relevant.
My next best guess is that you think that even though human reasoning can’t safely self-modify, its existence suggests that it’s likely that there is some form of reasoning which is more like human reasoning than logical reasoning and therefore not subject to Löb’s theorem, but which is sufficiently safe for a self-modifying FAI. Request for reply: Would that be right?
I can imagine that that might be the case, but I don’t think it’s terribly likely. I can more easily imagine that there would be something completely different from both human reasoning or logical reasoning, or something quite similar to normal logical reasoning but not subject to Löb’s theorem. But if so, how will we find it? Unless essentially every kind of reasoning except human reasoning can easily be made safe, it doesn’t seem likely that AGI research will hit on a safe solution automatically. MIRI’s current research seems to me like a relatively promising way of trying to search for a solution that’s close to logical reasoning.
When I say “failure to understand the surrounding literature”, I am referring more to a common MIRI failure mode of failing to sanity-check their ideas / theories with concrete examples / evidence. I doubt that this comment is the best place to go into that, but perhaps I will make a top-level post about this in the near future.
Ok, I think I probably don’t understand this yet, and making a post about it sounds like a good plan!
Sorry for ducking most of the technical points, as I said, I hope that talking to Paul will resolve most of them.
No problem, and hope so as well.
Since the PSM was designed without self-modification in mind, “safe but unable to improve itself in effective ways”.
(Not sure how this thought experiment helps the discussion along.)
MIRI stated goals are similar to those of mainstream AI research, and MIRI approach in particular includes as subgoals the goals of research fields such as model checking and automated theorem proving.
It’s definitely not a goal of mainstream AI, and not even a goal of most AGI researchers, to create self-modifying AI that provably preserves its goals. MIRI’s work on this topic doesn’t seem relevant to what mainstream AI researchers want to achieve.
Zooming out from MIRI’s technical work to MIRI’s general mission, it’s certainly true that MIRI’s failure to convince the AI world of the importance of preventing unFriendly AI is Bayesian evidence against MIRI’s perspective being correct. Personally, I don’t find this evidence strong enough to make me think that preventing unFriendly AI isn’t worth working on.
Also, two more points why MIRI isn’t that likely to produce research AI researchers will see as a direct boon to their field: One, stuff that’s close to something people are already trying to do is more often already worked on; the stuff that people aren’t working on seem more important for MIRI to work on. And two, AGI researchers in particular are particularly interested in results that get us closer to AGI, and MIRI is trying to work on topics that can be published about without bringing the world closer to AGI.
I thought the example was pretty terrible.
Glad to see you’re doing well, Benja :)
Sorry for being curmudgeonly there—I did afterwards wish that I had tempered that. The thing is that when you write something like
I also agree that the idea of “logical uncertainty” is very interesting. I spend much of my time as a grad student working on problems that could be construed as versions of logical uncertainty.
that sounds to me like you’re painting MIRI as working on these topics just because it’s fun, and supporting its work by arguments that are obviously naive to someone who knows the field, and that you’re supporting this by arguments that miss the point of what MIRI is trying to say. That’s why I found the example of program analysis so annoying—people who think that the halting problem means that program analysis is impossible really are misinformed (actually Rice’s theorem, really, but someone with this misconception wouldn’t be aware of that), both about the state of the field and about why these theorems say what they say. E.g., yes, of course your condition is undecidable as long as there is any choice f(s) of chooseAction2(s) that satisfies it; proof: let chooseAction2(s) be the program that checks whether chooseAction2(s) satisfies your criterion, and if yes return chooseAction(s), otherwise f(s). That’s how these proofs always go, and of course that doesn’t mean that there are no programs that are able to verify the condition for an interesting subclass of chooseAction2′s; the obvious interesting example is searching for a proof of the condition in ZFC, and the obvious boring example is that there is a giant look-up table which decides the condition for all choices of chooseAction2(s) of length less than L.
One possibility is that MIRI’s arguments actually do look that terrible to you, but that this is because MIRI hasn’t managed to make them clearly enough. I’m thinking this may be the case because you write:
In addition, there are more general proof strategies than the above if that one does not satisfy you. For instance, I could just require that any proposed modification to chooseAction2 come paired with a proof that that modification will be safe. Now I agree that there exist choices of chooseAction2 that are safe but not provably safe and this strategy disallows all such modifications. But that doesn’t seem so restrictive to me.
First, that’s precisely the “obvious” strategy that’s the starting point for MIRI’s work.
Second, yes, Eliezer’s arguing that this isn’t good enough, but the reason isn’t that it there are some safe modifications which aren’t provably safe. The work around the Löbian obstacle has nothing to do with trying to work around undecidability. (I will admit that for a short period at the April workshop I thought this might be a good research direction, because I had my intuitions shaken by the existence of Paul’s system and got overly optimistic, but Paul quickly convinced me that this was an unfounded hope, and in any case the main work around the Löbian obstacle was never really related to this.) MIRI’s argument definitely isn’t that “the above algorithm can’t decide for all chooseAction2 whether they’re safe, therefore it probably can’t decide it for the kind of chooseAction2 we’re interested in, therefore it’s unacceptable”. If that’s how you’ve understood the argument, then I see why you would think that the program analysis example is relevant. (The argument is indeed that it seems to be unable to decide safety for the chooseAction2 we’re interested in, but not because it’s unable to decide this for any generic chooseAction2.)
Third, you seem to imply that your proposal will only take safe actions. You haven’t given an argument for why we should think so, but the implication seems clear: You’re using a chooseAction that is obviously safe as long as it doesn’t rewrite itself, and it will only accept a proposed modification if it comes with a proof that it is safe, so if it does choose to rewrite itself then its successor will in fact be safe as well. Now I think this is fine reasoning, but you don’t seem to agree:
Finally, I agree that such a naieve proof strategy as “doing the following trivial self-modification is safe because the modified me will only do things that it proves won’t destroy the world, thus it won’t destroy the world” does not work. I’m not proposing that. The proof system clearly has to do some actual work.
You seem to be quite willing to use that reasoning yourself to show that the initial AI is safe, but you don’t think the AI should be able to use the same sort of reasoning. Eliezer’s argument is that this is in fact reasoning you want to use when building a self-improving AI: Yes, you can reason in more detail about how the AI you are building works, but this AI_1 will build an AI_2 and so on, and when proving that it’s ok to build AI_1 you don’t want to reason in detail about how AI_1,000,000 is going to work (which is built using design principles you don’t understand, by AI_999,999 which is much smarter than you); rather, you want to use general principles to reason that the because of the way AI_1,000,000 came to be, it has to be safe (because AI_999,999 only builds safe AIs, because it was built by AI_999,998 which only builds safe AIs...). But not only you need to reason like that, because you don’t know and aren’t smart enough to comprehend AI_1,000,000′s exact design; AI_1, which also isn’t that smart, will need to be able to use the same sort of reasoning. Hence, the interest in the Löbian obstacle.
There are caveats to add to this and parts of your comment I haven’t replied to, but I’m running into the same problem as you with your original comment in this thread, having already spent too much time on this. I’d be happy to elaborate if useful. For my part, I’d be interested in your reply to the other part of my comment: do you think I have localized our disagreement correctly?
Oh, one last point that I shouldn’t skip over: I assume the point about MIRI lacking “an understanding of the surrounding literature” refers to the thing about being tripped up at the July workshop by not knowing Gaifman’s work on logical uncertainty well enough. If so, I agree that that was an avoidable fail, but I don’t think it’s indicative of always ignoring the relevant literature or something like that. I’ll also admit that I still haven’t myself more with Gaifman’s work, but that’s because I’m not currently focusing on logical uncertainty, and I intend to do so in the future.
Jacob, have you seen Luke’s interview with me, where I’ve tried to reply to some arguments of the sort you’ve given in this thread and elsewhere?
I don’t think [the fact that humans’ predictions about themselves and each other often fail] is sufficient to dismiss my example. Whether or not we prove things, we certainly have some way of reasoning at least somewhat reliably about how we and others will behave. It seems important to ask why we expect AI to be fundamentally different; I don’t think that drawing a distinction between heuristics and logical proofs is sufficient to do so, since many of the logical obstacles carry over to the heuristic case, and to the extent they don’t this seems important and worth grappling with.
Perhaps here is a way to get a handle on where we disagree: Suppose we make a whole-brain emulation of Jacob Steinhardt, and you start modifying yourself in an attempt to achieve superintelligence while preserving your values, so that you can save the world. You try to go through billions of (mostly small) changes. In this process, you use careful but imperfect human (well, eventually transhuman) reasoning to figure out which changes are sufficiently safe to make. My expectation is that one of two things happens: Either you fail, ending up with very different values than you started with or stopping functioning completely; or you think very hard about how much confidence you need to have in each self-modification, and how much confidence you can achieve by ordinary human reasoning, and end up not doing a billion of these because you can’t achieve the necessary level of confidence. The only way I know for a human to reach the necessary level of confidence in the majority of the self-modifications would be to use formally verified proofs.
Presumably you disagree. If you could make a convincing case that a whole-brain emulation could safely go through many self-modifications using ordinary human reasoning, that would certainly change my position in the direction that the Löbian obstacle and other diagonalization issues won’t be that important in practice. If you can’t convince me that it’s probably possible and I can’t convince you that it probably isn’t, this might still help understanding where the disagreement is coming from.
Also note that, even if you did think it was sufficient, I gave you another example that was based purely in the realm of formal logic.
I thought the example was pretty terrible. Everybody with more than passing familiarity with the halting problem, and more generally Rice’s theorem, understands that the result that you can’t decide for every program whether it’s in a given class doesn’t imply that there are no useful classes of programs for which you can do so. MIRI’s argument for the importance of Löb’s theorem is: There’s an obvious way you can try to get stable self-modification, which is to require that if the AI self-modifies, it has to prove that the successor will not destroy the world. But if the AI tries to argue “doing the following trivial self-modification is safe because the modified me will only do things that it proves won’t destroy the world, thus it won’t destroy the world”, that requires the AI to understand the soundness of its own proof system, which is impossible by Löb’s theorem. This seems to me like a straight-up application of what Löb’s theorem actually says, rather than the kind of half-informed misunderstanding that would suggest that program analysis is impossible because Rice’s theorem.
Things that result in fewer resources going into AI specifically would result in fewer UFAI resources without reducing overall economic growth, but it needs to be kept in mind that some such research occurs in financial firms pushing trading algorithms, and a lot more in Google, not just in places like universities.
To the extent that industry researchers publish less than academia (this seems particularly likely in financial firms, and to a lesser degree at Google), a hypothetical complete shutdown of academic AI research should reduce uFAI’s parallelization advantage by 2+ orders of magnitude, though (presumably, the largest industrial uFAI teams are much smaller than the entire academic AI research community). It seems that reducing academic funding for AI only somewhat should translate pretty well into less parallel uFAI development as well.
I’d definitely be interested to talk more about many of these, especially anthropics and reduced impact / Oracle AI, and potentially collaborate. Lots of topics for future Oxford visits! :-)
Hope you’ll get interest from others as well.
Sorry for the long-delayed reply, Wei!
So you think that humans do not have a built-in solution to the Löbstacle, and you must also think we are capable of building an FAI that does have a built-in solution to the Löbstacle. That means an intelligence without a solution to the Löbstacle can produce another intelligence that shares its values and does have a solution to the Löbstacle.
Yup.
But then why is it necessary for us to solve this problem? [...] Why can’t we instead built an FAI without solving this problem, and depend on the FAI to solve the problem while it’s designing the next generation FAI?
I have two main reasons in mind. First, if you are willing to grant that (a) this is a problem that would require humans years of serial research to solve and (b) that it looks much easier to build this into an AI designed from scratch rather than bolting it on to an existing AI design that was created without taking these considerations into account, but you still think that (c) it would be a good plan to have the first-generation FAI solve this problem when building the next-generation FAI, then it seems that you need to assume that the FAI will be much better at AGI design than its human designers before it executes its first self-rewrite, since the human team would by assumption still need years to solve the problem at that point and the plan wouldn’t be particularly helpful if the first-generation FAI would need a similar amount of time or longer. But it seems unlikely to me that we first need to build ultraintelligent machines a la I.J. Good, far surpassing humans, before we can get an intelligence explosion: it seems to me that most of the probability mass should be in the required level of AGI research ability being ⇐ the level of the human research team working on the AGI. I admit that one possible strategy could be to continue having humans improve the initial FAI until it is superintelligent and then ask it to write a successor from scratch, solving the Löbstacle in the process, but it doesn’t seem particularly likely that this is cheaper than solving the problem beforehand.
Second, if we followed this plan, when building the initial FAI we would be unable to use mathematical logic (or other tools sufficiently similar to be subject to the same issues) in a straight-forward way when having it reason about its potential successor. This cuts off a large part of design-space that I’d naturally be looking to. Yes, if we can do it then it’s possible in principle to get an FAI to do it, but mimicking human reasoning doesn’t seem likely to me to be the easiest way to build a safe AGI.
Have you been following the discussions under my most recent post?
I agree with you that relying on an FAI team to solve a large number of philosophical problems correctly seems dangerous, although I’m sympathetic to Eliezer’s criticism of your outside-view arguments—I essentially agree with your conclusions, but I think I use more inside-view reasoning to arrive at them (would need to think longer to tease this apart). I agree with Paul that something like CEV for philosophy in addition to values should probably part of an FAI design. I agree with you that progress in metaphilosophy would be very valuable, but I do not have any concrete leads to follow. But I think that having good solutions to some of these problems is not unlikely to be helpful for FAI design (and more helpful to FAI than uFAI) so I still think that some amount of work allocated to these philosophical problems looks like a good thing; and I also think that working on these problems does on average reduce the probability of making a bad mistake even if we manage to have the FAI do philosophy itself and have it checked by “coherent extrapolated philosophy”.
You quoted my earlier comment that I think that making object-level progress is important enough that it seems a net positive despite making AGI research more interesting, but I don’t really feel that your post or the discussion below that contains much in the way of arguments about that—could you elaborate on the connection?
Drats. But also, yay, information! Thanks for trying this!
ETA: Worth noting that I found that post useful, though.
Glad to hear that & looking forward to seeing how it works! I very much understand that one might be concerned about posting “quick and dirty” thoughts (I find it so very difficult to lower my own standards even when it’s obviously blocking me from getting stuff done), but there seems to be little cost of trying it with a Discussion post and seeing how it goes—yay value of information! :-)
For future readers: The discussion has continued here.
Note that you’re wrongly discouraging people from doing strategy research by saying that they need to catch up to insiders’ unpublished knowledge when they really don’t.
What makes you say that? I believe you can reinvent much of what Eliezer and Carl and Bostrom and a few others already know but haven’t written down. Not sure that’s true for almost most everyone else.
I read the idea as being that people rediscovering and writing up stuff that goes 5% towards what E/C/N have already figured out but haven’t written down would be a net positive and it’s a bad idea to discourage this. It seems like there’s something to that, to the degree that getting the existing stuff written up isn’t an available option—increasing the level of publicly available strategic research could be useful even if the vast majority of it doesn’t advance the state of the art, if it leads to many more people vetting it in the long run. I do think there is probably a tradeoff, where Eliezer &c might not be motivated to comment on other people’s posts all that much, making it difficult to see what is the current state of the art and what are ideas that the poster just hasn’t figured out the straight-forward counter-arguments to. I don’t know how to deal with that, but encouraging discussion that is high quality compared to currently publicly available strategy work still seems quite likely to be a net positive?
You should frequently change your passwords, use strong passwords, and not use the same password for multiple services (only one point of failure where all your passwords get compromised rather than every such service being a point of failure). It’s not easy to live up to this in practice, but there are approximations that are much easier:
Using a password manager is better than using the same password for lots of services. Clipperz is a web service that does the encryption on your computer (so your passwords never get sent to the server), and can be installed locally. Alternatively, you can use a local application if you’re not worried about ever needing your passwords when you don’t have access to your computer. I currently try to get by with (a login password) + (passwords for particularly important online services like online banking) + (a password manager password).
If you balk at the inconvenience of regularly memorizing randomly-generated passwords, it’s better than nothing to come up with memorable phrases and take the first letter of each word to form your password. (Non-boring bonus advice: You can use phrases that remind you of something you want to do each time you log in to your computer, like looking at your todo list. [ETA: Never mind. I’ve now tried this twice and both times entering the password has become automatic far too quick, stopping almost immediately to serve as a useful reminder.])
As a pedestrian or cyclist, you’re not all that easy to see from a car at night, worse if you don’t wear white. High-visibility vests (that thing that construction workers wear, yellow or orange with reflective stripes) fix the problem and cost around $7-$8 from Amazon including shipping, or £3 in the UK.
For people stumbling upon this in the future: That interview has now been published. (Sorry to have been the cause of that delay :-/)
There are two donors which have donated $5,000 (just enough to be mentioned), three which have donated $10,000, one which has donated $15,000, and one which has donated $25,000, which suggests “people like donating such that their total is a multiple of $5,000” as a strong competing hypothesis.
Thanks!