Benya

• BenyaFeb 7, 2014, 9:06 PM

  1 point

  in reply to: CronoDAS’s comment on: L-zom­bies! (L-zom­bies?)

  (Agree with Coscott’s comment.)

L-zom­bies! (L-zom­bies?)

• BenyaJan 30, 2014, 12:13 PM

  0 points

  in reply to: TruePath’s comment on: Re­sults from MIRI’s De­cem­ber workshop

  I meant useful in the context of AI since any such sequence would obviously have to be non-computable and thus not something the AI (or person) could make pragmatic use of.

  I was replying to this:

  Ultimately, you can always collapse any computable sequence of computable theories (necessary for the AI to even manipulate) into a single computable theory so there was never any hope this kind of sequence could be useful.

  I.e., I was talking about computable sequences of computable theories, not about non-computable ones.

  Also, it is far from clear that T_0 is the union of all theories (and this is the problem in the proof in the other rightup). It may well be that there is a sequence of theories like this all true in the standard model of arithmetic but that their construction requires that T_n add extra statements beyond the schema for the proof predicate in T_{n+1}

  I can’t make sense of this. Of course T_n can contain statements other than those in T_{n+1} and the Löb schema of T_{n+1}, but this is no problem for the proof that T_0 is the union of all the theories; the point is that because of the Löb schema, we have T_{n+1} \subset T_n for all n, and therefore (by transitivity of the subset operation) T_n \subseteq T_0 for all n.

  Also, the claim that T_n must be stronger than T_{n+1} (prove a superset of it...to be computable we can’t take all these theories to be complete) is far from obvious if you don’t require that T_n be true in the standard model. If T_n is true in the standard model than, as it proves that Pf(T_n+1, \phi) → \phi this is true so if T_{n+1} |- \phi then (as this witnessed in a finite proof) there is a proof that this holds from T_n and thus a proof of \phi. However, without this assumption I don’t even see how to prove the containment claim.

  Note again that I was talking about computable sequences T_n. If T_{n+1} |- \phi and T_{n+1} is computable, then PA |- Pf(T_{n+1}, \phi) and therefore T_n |- Pf(T_{n+1}, \phi) if T_n extends PA. This doesn’t require either T_n or T_{n+1} to be sound.

• BenyaJan 29, 2014, 4:58 PM

  0 points

  in reply to: TruePath’s comment on: Re­sults from MIRI’s De­cem­ber workshop

  Actually, the `proof’ you gave that no true list of theories like this exists made the assumption (not listed in this paper) that the sequence of indexes for the computable theories is definable over arithmetic. In general there is no reason this must be true but of course for the purposes of an AI it must.

  (“This paper” being Eliezer’s writeup of the procrastination paradox.) That’s true, thanks.

  Ultimately, you can always collapse any computable sequence of computable theories (necessary for the AI to even manipulate) into a single computable theory so there was never any hope this kind of sequence could be useful.

  First of all (always assuming the theories are at least as strong as PA), note that in any such sequence, T_0 is the union of all the theories in the sequence; if T_(n+1) |- phi, then PA |- Box_(T_(n+1)) “phi”, so T_n |- Box_(T_(n+1)) “phi”, so by the trust schema, T_n |- phi; going up the chain like this, T_0 |- phi. So T_0 is in fact the “collapse” of the sequence into a single theory.

  That said, I disagree that there is no hope that this kind of sequence could be useful. (I don’t literally want to use an unsound theory, but see my writeup about an infinite sequence of sound theories each proving the next consistent, linked from the main post; the same remarks apply there.) Yes, T_0 is stronger than T_1, so why would you ever want to use T_1? Well, T_0 + Con(T_0) is stronger than T_0, so why would you ever want to use T_0? But by this argument, you can’t use any sound theory including PA, so this doesn’t seem like a remotely reasonable argument against using T_1. Moreover, the fact that an agent using T_0 can construct an agent using T_1, but it can’t construct an agent using T_0, seems like a sufficient argument against the claim that the sequence as a whole must be useless because you could always use T_0 for everything.

• BenyaJan 27, 2014, 11:44 AM

  1 point

  in reply to: ThisSpaceAvailable’s comment on: What should su­per­ra­tional play­ers do in asym­met­ric games?

  Independent.

• BenyaJan 24, 2014, 4:05 PM

  11 points

  on: What should su­per­ra­tional play­ers do in asym­met­ric games?

  I’m hard-pressed to this of any more I could want from [the coco-value] (aside from easy extensions to bigger classes of games).

  Invariance to affine transformations of players’ utility functions. This solution requires that both players value outcomes in a common currency, plus the physical ability to transfer utility in this currency outside the game (unless there are two outcomes o_1 and o_2 of the game such that A(o_1) + B(o_1) = A(o_2) + B(o_2) = max_o A(o) + B(o), and such that A(o_1) >= A’s coco-value >= A(o_2), in which case the players can decide to play the convex combination of these two outcomes that gives each player their coco-value, but this only solves the utility transfer problem, it doesn’t make the solution invariant under affine transformations).

• BenyaJan 24, 2014, 3:38 PM

  0 points

  in reply to: Luke_A_Somers’s comment on: What should su­per­ra­tional play­ers do in asym­met­ric games?

  ...so? What you say is true but seems entirely irrelevant to the question what the superrational outcome in an asymmetric game should be.

• BenyaJan 16, 2014, 11:23 PM

  0 points

  in reply to: Shmi’s comment on: Re­sults from MIRI’s De­cem­ber workshop

  Retracted my comment for being unhelpful (I don’t recognize what I said in what you heard, so I’m clearly not managing to explain myself here).

• BenyaJan 16, 2014, 8:20 AM

  0 points

  in reply to: Shmi’s comment on: Re­sults from MIRI’s De­cem­ber workshop

  Agree with Nisan’s intuition, though I also agree with Wei Dai’s position that we shouldn’t feel sure that Bayesian probability is the right way to handle logical uncertainty. To more directly answer the question what it means to assign a probability to the twin prime conjecture: If Omega reveals to you that you live in a simulation, and it offers you a choice between (a) Omega throws a bent coin which has probability p of landing heads, and shuts down the simulation if it lands tails, otherwise keeps running it forever; and (b) Omega changes the code of the simulation to search for twin primes and run for one more step whenever it finds one; then you should be indifferent between (a) and (b) iff you assign probability p to the twin prime conjecture. [ETA: Argh, ok, sorry, not quite, because in (b) you may get to run for a long time still before getting shut down—but you get the idea of what a probability over logical statements should mean.]

Re­sults from MIRI’s De­cem­ber workshop

• BenyaJan 7, 2014, 5:45 AM

  1 point

  in reply to: DanielLC’s comment on: What if Strong AI is just not pos­si­ble?

  I’m not saying we’ll take the genome and read it to figure out how the brain does what it does, I’m saying that we run a brain simulation and do science (experiments) on it and study how it works, similarly how we study how DNA transcription or ATP production or muscle contraction or a neuron’s ion pumps or the Krebs cycle or honeybee communication or hormone release or cell division or the immune system or chick begging or the heart’s pacemaker work. There are a lot of things evolution hasn’t obfuscated so much that we haven’t been able to figure out what they’re doing. Of course there’s also a lot of things we don’t understand yet, but I don’t see how that leads to the conclusion that evolution is generally obfuscatory.

• BenyaJan 2, 2014, 6:59 PM

  3 points

  in reply to: ESRogs’s comment on: What if Strong AI is just not pos­si­ble?

  Saying that all civilizations able to create strong AI will reliably be wise enough to avoid creating strong AI seems like a really strong statement, without any particular reason to be true. By analogy, if you replace civilizations by individual research teams, would it be safe to rely on each team capable of creating uFAI to realize the dangers of doing so and therefore refraining from doing so, so that we can safely take a much longer time to figure out FAI? Even if it were the case that most teams capable of creating uFAI hold back like this, one single rogue team may be enough to destroy the world, and it just seems really likely that there will be some not-so-wise people in any large enough group.

• BenyaJan 1, 2014, 9:04 PM

  4 points

  in reply to: James_Miller’s comment on: What if Strong AI is just not pos­si­ble?

  Good points.

  evolution hit on some necessary extraordinarily unlikely combination to give us intelligence and for P vs NP reasons we can’t find it

  For this one, you also need to explain why we can’t reverse-engineer it from the human brain.

  no civilization smart enough to create strong AI is stupid enough to create strong AI

  This seems particularly unlikely in several ways; I’ll skip the most obvious one, but also it seems unlikely that humans are “safe” in that they don’t create a FOOMing AI but it wouldn’t be possible even with much thought to create a strong AI that doesn’t create a FOOMing successor. You may have to stop creating smarter successors at some early point in order to avoid a FOOM, but if humans can decide “we will never create a strong AI”, it seems like they should also be able to decide “we’ll never create a strong AI x that creates a stronger AI y that creates an even stronger AI z”, and therefore be able to create an AI x’ that decides “I’ll never create a stronger AI y’ that creates an even stronger AI z’”, and then x’ would be able to create a stronger AI y’ that decides “I’ll never create a stronger AI z″”, and then y’ won’t be able to create any stronger successor AIs.

  (Shades of the procrastination paradox.)

• BenyaDec 31, 2013, 8:18 PM

  13 points

  in reply to: brazil84’s comment on: Why CFAR?

  I would agree with your reasoning if CFAR claimed that they can reliably turn people into altruists free of cognitive biases within the span of their four-day workshop. If they claimed that and were correct in that, then it shouldn’t matter whether they (a) require up-front payment and offer a refund or (b) have people decide what to pay after the workshop, since a bias-free altruist would make end up paying the same in either case. There would only be a difference if CFAR didn’t achieve what, in this counterfactual scenario, it claimed to achieve, so they should be willing to choose option (b) which would be better for their participants if they don’t achieve these claims. But of course CFAR doesn’t actually claim that they can make you bias-free in four days, or even that they can make themselves bias-free with years of training. Much of CFAR’s curriculum is aimed at taking the brain we actually have and tweaking the way we use it in order to achieve better (not perfect, but better) results—for example, using tricks that seem to engage our brain’s mechanisms for habit formation, in order to bypass using willpower to stick with a habit, rather than somehow acquiring all the willpower that would be useful to have (since there’s no known way to just do that). Or consider precommitment devices like Beeminder—a perfectly bias-free agent wouldn’t have any use for these, but many CFAR alumni (and, I believe, CFAR instructors) have found them useful. CFAR doesn’t pretend to be able to turn people into bias-free rationalists who don’t need such devices, so I see nothing inconsistent about them both believing that they can deliver useful training that makes people both on average more effective and more altruistic (though I would expect the latter to only be true in the long run, through contact with the CFAR community, and only for a subset of people, rather than for the vast majority of attendees right after the 4-day workshop), and also believing that if they didn’t charge up-front and asked people to pay afterwards whatever they thought it was worth, they wouldn’t make enough money to stay afloat.

• BenyaDec 27, 2013, 2:39 AM

  4 points

  in reply to: protest_boy’s comment on: CFAR has a matched-dona­tions fundraiser go­ing on [LINK]

  Yep: CFAR advertised their fundraiser in their latest newsletter, which I received on Dec. 5.

• BenyaDec 24, 2013, 4:41 AM

  3 points

  in reply to: Benya’s comment on: 2012 Win­ter Fundraiser for the Sin­gu­lar­ity Institute

  The only scenario I can see where this would make sense is if SIAI expects small donors to donate less than $(1/​2)N in a dollar-for-dollar scheme, so that its total gain from the fundraiser would be below $(3/​2)N, but expects to get the full $(3/​2)N in a two-dollars-for-every-dollar scheme. But not only does this seem like a very unlikely story [...]

  One year later, the roaring success of MIRI’s Winter 2013 Matching Challenge, which is offering 3:1 matching for new large donors (people donating >= $5K who have donated less that $5K in total in the past) -- almost $232K out of the $250K maximum donated by the time of writing, with more than three weeks time left, where the Winter 2012 Fundraiser the parent is commenting on only reached its goal of $115K after a deadline extension, and the Summer 2013 Matching Challenge only reached its $200K goal around the time of the deadline—means that I pretty much need to eat my hat on the “very unlikely story” comment above. (There’s clearly an upward growth curve as well, but it does seem clear that lots of people wanted to take advantage of the 3:1.)

  So far I still stand by the rest of the comment, though:

  [...] even if it did happen it seems that you should want to donate in the current fundraiser if you’re willing to do so [at 1:1 matching], since this means that more matching funds would be available in the later two-dollars-for-every-dollar fundraiser for getting the other people to donate who we are postulating aren’t willing to donate at dollar-for-dollar.

• BenyaDec 15, 2013, 6:35 PM

  13 points

  in reply to: passive_fist’s comment on: Nat­u­ral­is­tic trust among AIs: The parable of the the­sis ad­vi­sor’s theorem

  Yes, a real-life reasoner would have to use probabilistic reasoning to carry out these sorts of inference. We do not have a real understanding yet of how to do probabilistic reasoning about logical statements, though, although there has been a bit of work about it in the past. This is one topic MIRI is currently doing research on. In the meantime, we also examine problems of self-reference in ordinary deductive logic, since we understand it very well. It’s not certain that the results there will carry over in any way into the probabilistic setting, and it’s possible that these problems simply disappear if you go to probabilistic reasoning, but there’s no reason to consider this overwhelmingly likely, and if they don’t it seems likely that at least some insights gained while thinking about deductive logic will carry over. In addition, when an AI reasons about another AI, it seems likely that it will use deductive logic when reasoning about the other AI’s source code, even if it also has to use probabilistic reasoning to connect the results obtained that way to the real world, where the other AI runs on an imperfect processor and its source code isn’t known with certainty.

  More here.

• BenyaDec 15, 2013, 6:23 PM

  2 points

  in reply to: RolfAndreassen’s comment on: Nat­u­ral­is­tic trust among AIs: The parable of the the­sis ad­vi­sor’s theorem

  There is a way to write a predicate Proves(p,f) in the language of PA which is true if f is the Gödel number of a formula and p is the Gödel number of a proof of that formula from the axioms of PA. You can then define a predicate Provable(f) := exists p. Proves(p,f); then Provable(f) says that f is the Gödel number of a provable formula. Writing “A” for the Gödel number of the formula A, we can then write

  PA |- Provable(“A”)

  to say that there’s a proof that A is provable, and

  PA |- Provable(“Provable(“A”)”)

  to say that there’s a proof that there’s a proof that A is provable. (Of course, PA |- A just says that there is a proof of A.)

  On the metalevel, we know that

  PA |- A

  if and only if

  PA |- Provable(“A”).

  On the other hand, PA proves neither A → Provable(“A”) nor Provable(“A”) → A for general A.

  (Hope that helps?)

Nat­u­ral­is­tic trust among AIs: The parable of the the­sis ad­vi­sor’s theorem

• BenyaNov 10, 2013, 10:42 AM

  15 points

  on: The Evolu­tion­ary Heuris­tic and Ra­tion­al­ity Techniques

  An example of this: CFAR has published some results on an experiment where they tried to see if they could improve people’s probability estimates by asking them how surprised they’d be by truth about some question turning out one way or another. They expected it would, but it turned out it didn’t. And that doesn’t surprise me. If imagined feelings of surprise contained some information naive probability-estimation methods didn’t, why wouldn’t we have evolved to tap that information automatically?

  Because so few of our ancestors died because they got numerical probability estimates wrong.

  I agree with the general idea in your post, but I don’t think it strongly predicts that CFAR’s experiment would fail. Morever, if it predicts that, why doesn’t it also predict that we should have evolved to sample our intuitions multiple times and average the results, since that seems to give more accurate numerical estimates? (I don’t actually think this single article is very strong evidence for or against this interpretation of the hypothesis by itself, but neither do I think that CFAR’s experiment is; I think the likelihood ratios aren’t particularly extreme in either case.)

  What links here?

  • The Evolu­tion­ary Heuris­tic and Ra­tion­al­ity Techniques by ChrisHallquist (Nov 10, 2013, 7:30 AM; 19 points)