My problems with Formal Friendly Artificial Intelligence work

It is the "learn to walk before you start learning to run and jump" approach.

Imagine that you are the first human who ever tried to invent math. You have invented the "2 + 2 = 4" theorem, and it seems to work! Two stones together with other two stones always make four stones. And two bananas together with other two bananas always make four bananas. Seems like you have found a powerful abstraction behind stones and bananas -- who knows what else might be obeying the same rules. Excited you run towards your tribe members to share your discovery...

...but they dismiss it as worthless. "No two stones are same. A sharp stone is a more useful tool than a blunt stone, and your theory ignores that. A banana can be eaten. Actually, bananas are only useful for eating, and you completely ignore this essential part. And have you ever tried to 'add' two and two raindrops? Obviously, this 'mathematics' of yours has no future, and is just a waste of time" they say.

Well, the answer is that you need to apply the "2 + 2 = 4" only in the situations where it is appropriate, and not where it's not. And telling the difference may be tricky. And it may be easy to underestimate some problem. But still, the equation is useful in some contexts, which makes it useful to know it.

Does refusing to know "2 + 2 = 4" because of these practical concerns make you stronger or weaker?

I don't understand why: other agents trust that your source code is what you say it is

It's an assumption to simplify the problem. First we learn to solve the "simple" problem, then we move to the more complex ones. If we can't solve the simpler problem yet, would jumping to the more complex one make us progress faster?

Would a recommendation to skip solving the simplified problems, because they don't include all the messy details, more likely lead to prople solving the hard problems faster, or giving up?

I think pragmatism make a better core as it makes less assumptions about the nature of reality, with other stuff layered on top.

How specifically are you planning to use this insight in constructing a Friendly superintelligent AI?

Doing theoretical research that ignores practicalities is sometimes turns out to be valuable in practice. It can open a door to something you assumed to be impossible; or save a lot of wasted effort on a plan that turns out to have an impossible sub-problem.

A concrete example of first category might be something like quantum error correcting codes. Prior to that theoretical work, a lot of people thought that quantum computers were not worth pursuing because noise and decoherence would be an insurmountable problem. Quantum fault tolerance theorems did nothing to help solve the very tough practical problems of building a quantum computer, but it did show people that it might be worth pursuing - and here we are 20 years later closing in on practical quantum computers.

I think source code based decision theory might have something of this flavour. It doesn't address all those practical issues such as how one machine comes to trust that another machine's source code is what it says. That might indeed scupper the whole thing. But it does clarify where the theoretical boundaries of the problem are.

You might have thought "well, two machines could co-operate if they had identical source code, but that's too restrictive to be practical". But it turns out that you don't need identical source code if you have the source code and can prove things about it. Then you might have though "ok, but those proofs will never work because of non-termination and self-reference" ... and it turns out that that is wrong too.

Theoretical work like this could inform you about what you could hope to achieve if you could solve the practical issues; and conversely what problems are going to come up that you are absolutely going to have to solve.

The criticisms of "general functionalism" in the post seem to me to be aimed at a different sort of functionalism from the sort widely espoused around here.

The LW community is (I think) mostly functionalist in the sense of believing e.g. that if you're conscious then something that does the same as you do is also conscious. They'd say that implementation details don't matter for answering various philosophical questions. Is this thing me? Is it a person? Do I need to care about its interests? Is it intelligent? Etc. But that's a long way from saying that implementation details don't matter at all and, e.g., I think it's "LW orthodoxy" that they do; that, e.g., something that thinks just like me but 1000x faster would be hugely more capable than me in all sorts of important ways.

(The advantages of the humans over the aliens in Eliezer's "That Alien Message" have a lot to do with speed, though that wasn't quite Eliezer's point and he makes the humans smarter in other ways and more numerous too.)

If formal AI-safety work neglects speed, power consumption, side-channel attacks, etc., I think it's only for the sake of beginning with simpler more tractable versions of the problems you care about, not because anyone seriously believes that those things are unimportant.

(And, just to be explicit, I believe those things are important, and I think it's unlikely that any approach to AI safety that ignores them can rightly be said to deliver safety. But an approach that begins by ignoring them might be reasonable.)

If people start baking in TDT or UDT into the core of their AIs philosophy

I don't understand UDT, but TDT can look at the evidence and decide what the other AI actually does. It can even have a probability distribution over possible source codes and use that to estimate expected value. This gives the other AI strong incentive to look for ways to prove its honesty.

I worry that the last paragraph of this post is too optimistic.If "formal proof is insufficient", that might mean that proceeding formally can't produce superintelligent AI, in which case indeed we don't need to worry so much about AI risks -- but it might instead mean that proceeding formally produces flaky superintelligent AI. That is, AI that's just about as smart as we'd have hoped or feared, except that it's extra-vulnerable to malicious hackers, or it has weird cognitive biases a bit like ours but orders of magnitude more subtle, or it basically operates like a "normal" superintelligence except that every now and then a cosmic ray flips a bit and it decides to destroy the sun.

That would not be reassuring.

The more pragmatic philosophy suggested implies (but doesn't prove) that AI will not be as powerful as expected as the physicality of computation is important and instantiating computing in a physical fashion is expensive.

Computer that was expensive a decade ago is a lot less expensive today.

In the Age of Em Hanson lays out how even brain emulations that aren't smarter than the smartest humans could out-compete humanity very fast.

I also think that an abandonment of functionalism makes AI less scary. If formal proof is insufficient for AI improvement and experimentation and exposure to the world is required to make sure there aren't side channels or resource exhaustions neglected by the formal model, the potential top speed of improvement slows down dramatically.

If formal proof doesn't work that only indicates that everything is more dangerous because you can't use it to create safety.