Comment author: Benito 25 March 2015 07:37:35PM *  2 points [-]

Similar to V_V's comment. I'm only a layman, but I don't understand one of the first steps.

The paper appears to jump straight into the logic, justifying itself (pardon the pun) by a statement about the intricacies of formal systems proving things about other formal systems.

Can you explain how and why all AI systems correspond to formal systems - what precisely you mean by 'formal system'?

(Btw, I have in fact read GEB, but I am still unable to confidently define a formal system.)

Or a better question might be "Why does this need to be possible within the realms of formal logic to be doable at the level of code/AI? There are many general problems intractable as part of pure maths, yet many numerical methods exist to solve particular instantiations. Why must this be doable at the level of pure logic?"

Comment author: orthonormal 25 March 2015 11:32:15PM 5 points [-]

Good question as well! I should add motivation to the notes on this point.

Basically, we study deterministic mathematical objects within formal systems because these cases are easier for us to analyze and prove theorems about; it's an example of looking first under the streetlight before meandering farther into the darkness. Hopefully this way we'll notice many phenomena that still hold when we add randomness, bounded computations, and other realistic limitations.

And indeed, plenty of the topics in MIRI research do hold up when you make them messier. Many of the topics in formal systems can handle random variables just as easily as deterministic facts. There's a version of Löb's Theorem for bounded-length proof searches, and tracing it through shows that Löbian cooperation and other phenomena behave the same there as in the unbounded case (for sufficiently large choices of the bounds). Using quantum random variables to evaluate logical counterfactuals doesn't solve implementing UDT, it just collapses it into CDT; so we still need to study logical counterfactuals. And so on.

Also, when I say "formal system" you can usually substitute in "Peano Arithmetic" or "Peano Arithmetic plus some extra axioms".

Comment author: V_V 25 March 2015 06:12:38PM *  1 point [-]

I haven't read the paper yet (thanks for posting it, anyway), so maybe the answer to my question is there, but there is something about MIRI interest with Löb's theorem that always bugged me, specifically:

Unfortunately, the straightforward way of setting up such a model fails catastrophically on the innocent-sounding step “DT1 knows that DT2’s deductions are reliable”. If we try and model DT1 and DT2 as proving statements in two formal systems (one stronger than the other), then the only way that DT1 can make such a statement about DT2’s reliability is if DT1 (and thus both) are in fact unreliable! This counterintuitive roadblock is best explained by reference to Löb’s theorem, and so we turn to the background of that theorem.

Sure, DT1 can't prove that DT2 decisions are reliable, and in fact in general it can't even prove that DT1 itself makes reliable decisions, but DT1 may be able to prove "Assuming that DT1 decisions are reliable, then DT2 decisions are reliable".
Isn't that enough for all practical purposes?

Notice that this even makes sense in the limit case where DT2 = DT1, which isn't necessarily just a theoretical pathological case but can happen in practice when even a non-self-modifying DT1 ponders "Why should I not kill myself?"

Am I missing something?
Isn't Löb's theorem just essentially a formal way of showing that you can't prove that you are not insane?

Comment author: orthonormal 25 March 2015 06:24:50PM 1 point [-]

Good question! Translating your question to the setting of the logical model, you're suggesting that instead of using provability in Peano Arithmetic as the criterion for justified action, or provability in PA + Con(PA) (which would have the same difficulty), the agent uses provability under the assumption that its current formal system (which includes PA) is consistent.

Unfortunately, this turns out to be an inconsistent formal system!

Thus, you definitely do not want an agent that makes decisions on the criterion "if I assume that my own deductions are reliable, then can I show that this is the best action?", at least not until you've come up with a heuristic version of this that doesn't lead to awful self-fulfilling prophecies.

Comment author: efim 24 March 2015 10:32:20AM *  5 points [-]

I am stuck at part 2.2: "So in particular, if we could prove that mathematics would never prove a contradiction, then in fact mathematics would prove that contradiction"

I've spend 15 minutes on this, but still cannot see relation to löb's theorem. Even though it seems like it should be obvious to attentive reader.

Could anyone please explain or link me to an explanation?

Comment author: orthonormal 24 March 2015 05:20:10PM 1 point [-]

Thanks for asking! I should add another sentence in that paragraph; the key step, as Kutta and Quill noted, is that "not A" is logically equivalent to "if A, then False", and in particular the statement "2+2=5 is not provable" is logically equivalent to "if 2+2=5 were provable, then 2+2=5", and then we can then run Löb's Theorem.

Comment author: Kaj_Sotala 23 March 2015 07:02:09AM *  5 points [-]

I'm not sure the current implementation of the tiered privileges system is optimal. For instance, after a link I posted got two likes, it become visible to everyone, but it looks like my reply to your comment isn't visible if one isn't logged in. I think that once a non-member link meets the necessary threshold for becoming visible to everyone, the poster's replies to comments in the thread should become visible as well, or otherwise it's just confusing.

Also, I feel that if new contributor comments are hidden in general, that might be a little too discouraging for new people if those comments also need to acquire two member likes in order to become visible.

Comment author: orthonormal 24 March 2015 01:01:35AM *  2 points [-]

I think that once a non-member link meets the necessary threshold for becoming visible to everyone, the poster's replies to comments in the thread should become visible as well, or otherwise it's just confusing.

That seems like a good feature request.

[Clearing out my Drafts folder] Rationality and Decision Theory Curriculum Idea

6 orthonormal 23 March 2015 10:54PM

Note: The following is a draft post I've had since 2009, and it's not great but it's worth posting for discussion. I do like the way that it prefigures some of the problems of Quirrell Points when traitors are allowed...

Need to see if this can be easily gamed, but...

Step 1. Introduce Prisoner's Dilemma.  Set up computer system so that they can log in and play it in partners with investments of points (caution them: this is their actual grade at stake).  Let them know that they currently don't have enough points for a passing grade on that part of the course, but that maximum investment and mutual cooperation will result in A's for (almost) everyone on it (with high probability); also that points are converted to grades on a logarithmic scale.  Let them know that creating institutions and alliances is a good strategy in such games.

Initially, each student is allowed to play once per day, with 1 partner.  Students log in, enter the name of their requested PD partner, enter how much they're willing to invest, and enter C or D.  They'll get a "bank statement" daily as well.

If both enter C, they each get 1.2 points back (per initial point invested).  If one enters C and the other D, the cooperator gets nothing back and the defector gets 2 points (per point invested). If both enter D, then each gets 0.5 points back.

Once they've had some practice with this, we move to

Step 2: Bigger investments, luck, observation.

Introduce larger group investments with higher rates of return.  E.g. a five-person opportunity that pays each C player 0.2 guaranteed plus 0.4 for each C (not counting themselves), and each D player gets 0.5 guaranteed plus 0.5 for each C.  (Set these up to be balanced in some way.)

Add a factor of luck, so that people can't just (be forced to) show one another their bank statements as proof of their cooperation.  People should average the proper amounts, but have enough variation that it's often difficult to tell whether they cooperated or defected.  (Or is there another way to handle this?)

Finally, allow a third option of observation within a deal.  One idea: if you choose to observe, then you take up a spot in the investment, keep your own point, and don't count as a C for others, but you get to see some or all of the other players' choices.  Make sure that information is proportionately expensive.

Step 3: Keep scaling it up, adjust (only) as necessary.

If things get too unbalanced, some progressive taxation and welfare might be in order; but disrupting the system too much will tend to destroy the things they need to learn.

Ideally, larger and larger opportunities should be offered, with the kicker being a gigantic one-shot Prisoner's Dilemma that the whole class can partake in.  C might get guaranteed 0.2 plus 0.2 for every other C, while D gets guaranteed 1 plus 0.3 for every C.

Implementation:

Need a non-hackable computer program to work off of.  Also, have students (for real points) give critiques and suggestions for improvement.

An Introduction to Löb's Theorem in MIRI Research

16 orthonormal 23 March 2015 10:22PM

Would you like to see a primer on several MIRI research topics (assuming only the background of having taken a course with proofs in math or computer science)? Or are you curious why MIRI does so much with mathematical logic, and why people on Less Wrong keep referring to Löb's Theorem?

If you answered yes to either question, you may be interested in my lecture notes, An Introduction to Löb's Theorem in MIRI Research! These came out of an introductory talk that I gave at a MIRIx workshop.

Since I've got some space here, I'll just copy and paste the table of contents and the introduction section...

continue reading »
Comment author: Vladimir_Nesov 19 March 2015 02:10:32PM *  14 points [-]

From the welcome post:

Examples of subjects that are off-topic (and which moderators might close down) include [...] anything that cannot (yet) be usefully formalized or modeled mathematically.

This seems open to an undesirable interpretation (discussion of how to formulate things that haven't yet been formulated and exercises in working through pre-formal examples, in an attempt to isolate principles that can then be explored more systematically). It might also encourage cargo cult formalization.

Comment author: orthonormal 23 March 2015 09:56:10PM 10 points [-]

I've edited it to the following:

But the list does help us to point out what we consider to be on-topic in this forum. Besides the topics mentioned there, other relevant subjects include groundwork for self-modifying agents, abstract properties of goal systems, tractable theoretical or computational models of the topics above, and anything else that is directly connected to MIRI’s research mission.

It’s important for us to keep the forum focused, though; there are other good places to talk about subjects that are more indirectly related to MIRI’s research mission, and the moderators here may close down discussions on subjects that aren’t a good fit for this mission. Some examples of subjects that we would consider off-topic (unless directly applied to a more relevant area) include general advances in artificial intelligence and machine learning, general mathematical logic, general philosophy of mind, general futurism, existential risks, effective altruism, human rationality, and non-technical philosophizing.

In particular, it now discourages "general advances in artificial intelligence and machine learning", and discourages "non-technical philosophizing" rather than "anything that cannot (yet) be usefully formalized or modeled mathematically". Is this an improvement?

Comment author: joaolkf 21 March 2015 04:03:36PM 11 points [-]

I don't currently have a facebook account and I know that a lot of very productive people here in Oxford that decided not to have one as well (e.g., Nick and Anders don't have one). I think adding the option to authenticate via Google is an immediate necessity.

Comment author: orthonormal 21 March 2015 11:41:24PM 3 points [-]

Developer time is a big bottleneck, but I agree with you that adding the option for Google authentication is a high priority.

Comment author: [deleted] 21 March 2015 04:34:13PM *  0 points [-]

Prohibit what you don't want, non-technical philosophizing, rather than a blanket prohibition that covers all sorts of other things. For example, what about existing AGI designs that lack an unified underlying formal model as of yet, e.g. OpenCog? They're apparently off limits, even a discussion involving experimental data of real world systems. That seems wrong.

EDIT: I found the original source:

Examples of subjects that are off-topic (and which moderators might close down) include recent advances in artificial intelligence and machine learning,

Wow, I just... wow. Subjects that are off-topic: artificial intelligence and machine learning. Well enjoy your anti-rationalist ivory tower; I won't be participating.

Comment author: orthonormal 21 March 2015 11:39:20PM 5 points [-]

Sorry you feel that way, but it's kind of essential that the forum is not about the latest AI techniques, but about groundwork for the kind of safety research that could stand up to smarter-than-human AI. There are plenty of great places on the Internet for discussing those other topics!

Comment author: [deleted] 20 March 2015 09:03:17PM 12 points [-]

Wow, I'm so glad I stumbled onto slatestarcodex, and from there, here!!! You guys are all like smarter, cooler versions of me! It's great to have a label for the way my brain is naturally wired and know there other people in the world besides Peter Singer who think similarly. I'm really excited, so my "intro" might get a little long...

Part 1-Look at me, I'm just like you!

I'm Ellen, a 22 year old Spanish major and world traveling nanny from Wisconsin, so maybe not your typical LWer, but actually quite typical in other, more important ways. :)

I grew up in a Christian home/bubble, was super religious (Wisconsin Evangelical Lutheran Synod), truly respected/admired the Christians in my life, but even while believing, never liked what I believed. I actually just shared my story plus some interesting studies on correlations between personality, intelligence, and religiosity, if anyone is interested: http://magicalbananatree.blogspot.com/2015/02/christian-friends-do-you-ever-feel.html The post is based almost entirely on what I've come to learn is called "consequentialism" which I'm happy to see is pretty popular over here. I subscribe to this line of thinking so much that I used to pray for a calamity to strengthen my faith. I chose a small Lutheran school despite having great credentials to get into an Ivy, because with an eye on eternity, I wanted to avoid any environment that would foster doubt. My friends suggested I become a missionary, but to me, it made far more sense to become a high profile lawyer and donate 90% of my salary to fund a dozen other missionaries. (A Christian version of effective altruism?) No one ever understood!

Some people might deconvert because they can't believe in miracles, or they can't get over the problem of evil. These are bad reasons, I think, and based on the presupposition that God doesn't exist. Personally, the hardest thing for me was believing that God was all-powerful. Like, if God were portrayed as good, but weak, struggling against an evil god and just doing the best he could to make a just universe and make his existence known, I probably would never have left the faith. It took me long enough as it is!

Part 2-A noob atheist's plea for help

Anyway, now I've "cleared my mind" of all that and am starting fresh, but my friends have a lot of questions for me that I'm not able to answer yet, and I have a lot of my own, too. I'm starting by reading about science (not once had I even been exposed to evolution!) but have a lot of other concerns on the back burner, and maybe you guys can point me in the right direction:

Who was the historical Jesus? As a history source, why is the Bible unreliable?

How can I have morality?? Do I just have to rely on intuition? If the whole world relied on reason alone to make decisions, couldn't we rationalize a LOT of things that we intuit as wrong?

Does atheism necessarily lead to nihilism? (I think so, in the grand scheme of things? But the world/our species means something to us, and that's enough, right?)

What about all the really smart people I know and respect, like my sister and Grandma, who have had their share of doubts but ultimately credit their faith to having experienced extraordinary, miraculous answers to prayer? Like obviously, their experiences don't convince ME to believe, but I hate to dismiss them as delusional and call it a wild coincidence...

Are rationalists just as guilty of circular reasoning as Christians are? (Why do I trust human reason? My human reason tells me it's great. Why do Christians trust God? The Bible tells them he's great.)

Part 3-Embarrassingly enthusiastic fan mail

Yay curiosity! Yay strategic thinking! Yay honesty! Yay open-mindedness! Yay opportunity cost analyses! Yay common sense! Yay tolerance of ambiguity! Yay utilitarianism! Yay acknowledging inconsistency in following utilitarianism! Yay intelligence! Yay every single slatestarcodex post! Yay self-improvement! Yay others-improvement! Yay effective altruism!

Ahhh this is all so cool! You guys are so cool. I can't wait to read the sequences and more posts around this site! Maybe someday I'll even meet a real life rationalist or two, it seems like the Bay Area has a lot. :)

Comment author: orthonormal 20 March 2015 09:55:58PM 3 points [-]

There's also a Less Wrong meetup group in Madison, if you still live in Wisconsin! (They also play lots of board games.)

View more: Prev | Next