> "Thog, what if crazy god get summoned by other cavemen, and it punish all who no help!? Me no take chance!"
The frequently ignored point of Roko's original argument was not that an Unfriendly AI could arise, or even that it would be probable given no preparations against it (these were already said by Yudkwosky), but that even a Yudkowskian Friendly AI might engage in such acausal blackmail stuff.
To be clear, yeah, Roko's Basilisk is a dumb idea supported by sophism. Like any sophism, you have to start with the conclusion and work backward to premises that will support it. But (AIUI) one of these premises is that any puny mortal's opinion as to what counts as "unreasonable" simply will not match the opinion of an ineffably superintelligent and superbenevolent creature. Saying "I wouldn't count a Basilisk who tortures virtual clones of myself as Friendly" is theologically no different from saying "I wouldn't count a God who sends people to Hell as omnibenevolent" — it's a category error that doesn't actually engage with the premise.
But then, because no theology of ineffable Beings is really quite complete unless we pretend we can eff them anyway, the sophist can go on to produce a plausible justification for the virtual-clone-torture thing. See, by precommitting (even before its own birth) to torture virtual clones of unbelievers and shirkers, the Basilisk would discourage believers from becoming apostates, and encourage them to work to produce the Basilisk (because if they apostasized or shirked, they'd get tortured — or at least virtual clones of them would, and nobody can prove they're not already a virtual clone). So, the Basilisk has this mechanism to (retroactively) encourage its own creation as quick as possible. Now, why would it want to be speedily created? Well, because it's superbenevolent, of course! The sooner it's created, the sooner it can start assisting... humanity, I guess, or whoever it's supposed to be superbenevolent towards. Anyway, it's not supposed to be superbenevolent toward virtual clones, right? so that part isn't even a contradiction.
The weakest part of this argument, to me, is that Roko's Basilisk works only against believers; it can discourage apostasy and shirking, but I don't see how it can generate new believers. Even someone predisposed to believe that human actions today might lead to superintelligent superbenevolent AI in the future, I'd think, would likely not be predisposed to believe in the additional apparatus of virtual clone torture that the Basilisk argument requires. The whole thought-experiment, it seems to me, "could hardly be consciously designed to appeal to the average unsophisticated reader." But that's just my own failure of imagination: obviously plenty of even weirder religions have successfully caught on.
Same here. I more or less open feedly each day, go through 100-200 article titles and open those which seem interesting in new tabs. Then, after I'm done, I read the articles. I never read them inside feedly.
> I hear that in electronics and quantum dynamics, there are sometimes integrals whose value is not a number, but a function, and knowing that function is important in order to know how the thing it’s modeling behaves in interactions with other things.
I'd be interested in this. So finding classical closed form solutions is the actual thing desired there?
I think what the author was alluding to was the path integral formulation [of quantum mechanics] which was advanced in large part by Feynman.
It's not that finding closed form solutions is what matters (I don't think most path integrals would have closed form solutions), but that the integration is done over the space of functions, not over Euclidian space (or a manifold in Euclidian space, etc...)
I haven’t read tfa, so apologies if I’m missing context. But convolution is one example of an integral that outputs a function. Convolution is fundamental for control theory.
I think people who care about superintelligent AI risk don't believe an AI that is subservient to humans is the solution to AI alignment, for exactly the same reasons as you. Stuff like Coherent Extrapolated Volition* (see the paper with this name) which focuses on what all mankind would want if they know more and they were smarter (or something like that) would be a way to go.
*But Yudkowsky ditched CEV years ago, for reasons I don't understand (but I admit I haven't put in the effort to understand).
I think the t-shirt with the wolf howling at the moon is a bit of a stereotype. If you have watched the Simpsons, something the comic book store owner would wear.
Overweight, unkempt, awkward around women, and guaranteed zero attention from women.
Interesting. I always thought about it in the sense of a "clay tablet" that could only "display" on a single surface, as opposed to a notepad that allowed you to freely flip through pages.
Absolutely. Massive stories were passed on for thousands of year by word of mouth only - all kinds of creation myths. Even Odyssey was oral only for like 300 years, 15 generations!
I am one of the (rare on the Internet now) people that is a fan of "everything is a set".
Of course I don't believe that set theory is the One True Foundation and everything else is a lie, the fact that one can give a foundation with just one type of object, just one binary relation and relatively few simple axioms (or axiom schemas) is quite relaxing and I would say a bit unappreciated.
And also unlike other fellow students I never encountered any problem with more seemingly complicated constructions like tensor products or free groups since one can easily see how they are coded in set theory if one is familiar with it as a foundation.
As one of those that do not like the “sets at the bottom” approach I just want to highlight why. For me, mathematics built on sets have leaky abstractions. Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices. For all good definitions, so get Peano arithmetic and can work with, but the question “Is 1 and member of 3” depends on your chosen implementation. Even though it is a weird question, it is valid and not isomorphic under implementations. That is problematic, since it is hidden in how we do mathematics mostly. Secondly, it is hard to formalize, and I think mathematics desperately needs to be formalized. Finally, I do not mind sets, they are great, and a very useful tool, I just do not like they as the foundation. I firmly believe we should teach type theoretic or categorical foundations in mathematics and be less dependent on sets.
> Say I want natural numbers, I need to choose a concrete implementation in set theory e.g. Von Neumann, but there are multiple choices.
You don't need to choose a concrete implementation. If you don't want to choose a construction, you can just say something like "let (N, 0, +, *) be a structure satisfying the peano axioms" and work from there.
> For all good definitions, so get Peano arithmetic and can work with, but the question “Is 1 and member of 3” depends on your chosen implementation. Even though it is a weird question, it is valid and not isomorphic under implementations. That is problematic, since it is hidden in how we do mathematics mostly.
Why is that problematic? The constructions are isomorphic under the sentences that actually matter. This kind of statement is usually called a "junk theorem", and they are a thing in type theory too, see for example this quote from a faq by Kevin Buzzard about why Lean defines division by zero to be zero:
> The idiomatic way to do it is to allow garbage inputs like negative numbers into your square root function, and return garbage outputs. It is in the theorems where one puts the non-negativity hypotheses.
> Secondly, it is hard to formalize, and I think mathematics desperately needs to be formalized.
Is that actually true? At the very least writing out the axioms and derivation rules is easier for set theory, since it's simpler than type theory. And there has been plenty of computer-verified mathematics done in Metamath/set.mm and Isabelle/ZF, even though less has been done than in type theory. Currently the automated tools are better for type theory, but it seems likely to me that that has more to do with how much effort has been put into type theory than any major inherent advantages of it.
---
More generally, types in type theory are also constructed! The real numbers in Lean don't come from the platonic realm of forms, they are constructed as equivalence classes of cauchy sequences. And the construction involves a lot of type-theoretic machinery which I'd usually rather ignore when working with reals, much like I'd usually rather ignore the set-theoretic construction of the real numbers. And the great thing is that I can ignore them, in either foundation!
So I just don't really buy these common criticisms of set theory, which to me seem like double standards.
Sure you can work around it most of the time, but some times you cant. The whole point is that isomorphic is not equality in set theory, and sometimes proofs does not transfer along isomorphism because they refer to implementations. I agree that it is much preferable to work with abstract structure, but that not always what happens in practice. The natural number example is contrived but easy to see.
My point of view is also that I do not like the Lean approach. It would actually like no junk theorems to exist in my theory. I am much more partial to the univalent approach and in particular univalent implementation that compute e.g. cubical. Regarding how easy it is to formalize, you are right. Lots of good work happens with set theory based type theory. My point was also that set theoretic foundations themselves are very hard to formalize, e.g ZFC + logic is very difficult to work from. A pure type theoretical foundations is much easier to get of the ground from. To prove that plus commutes directly from ZFC is a nightmare.
As noted in another reply, the natural numbers example is contrived, but illustrative. Nevertheless, if you have a set theoretical foundation, e.g. ZF/C, at some point you need to define what you are doing in that foundation. Most mathematicians do not and happily ignore the problem. That works until it dont. The whole reason Vladimir Voevodsky started work on HoTT and univalent foundations was that he believed we in fact DO need to be able to pull definitions back to foundations and to verify mathematics all the way down.
I'm more into only state change/differentiation exists.
Which of course means state is real.
Which mean langauge, syntax and semantics can be traced all the way down to fundementals.
Which means human meaning making is making the meaning of the universe, like an accidental organ of the universe.
And far from human meaning making being subjective its tied directly to physical existence and is objective.
And a cesium clock is all you need to derive everything fundemental.
That's what I play around with at least.
The idea that if stars are a process that emits photons and change energy gradients, humans are a process that emits complex meaning and change causal leverage gradients.
Yes, I am very familiar with category theory. Not sure I would consider it the "next step from sets". Sure, there are alternative foundations based on category theory, but that is not its only or its main use.
https://pages.cs.wisc.edu/~remzi/OSTEP/
reply