So, I was thinking about the misapplication of the deduction theorem and suddenly had an insight into friendly AI. (Stop me if this has been discussed =D )
The problem is you give the AI a set of 'axioms' or goals and it might go off and tile the universe. Obviously we don't know the full consequences of the logical system we're initiating otherwise we wouldn't need the AI in the first place.
The problem already exists in humans. Evolution gave us 'axioms' or desires. Some people DO go off and tile their universe: drugs, sex or work addictions, etc, etc. Thus my insight stems from the lack of drug addictions in most people. Here are my two proposed solutions:
(1) Fear. Many people don't do drugs not because of a lack of desire to feel good, but because they are scared. People are likewise scared of any large changes (moving, new job, end of a relationship). Now, we don't need the AI to favor status quo, however we can simply code into ones of its axioms that large physical changes are bad. Scale this exponentially (ie, twice the physical changes SQUARES the negative weighting of the action). Do not have any positive weighting criteria on other goals that scale faster than a polynomial.
(2) Life. Many people don't tile their universe because they have too many different things they'd like to tile it with. Hobbies, friends, lovers, variation, etc. Give the AI a multitude of goals and set the positive weight associated with their accomplishment to diminish with returns (preferably logarithmic in growth at most). Twice the tiles only gives a linear increase in gauged utility.
Volume of tiling is bounded above by polynomial growth in time (cubic in a 3D universe with speed limit), hence hitting it with a log penalty will stifle its growth to at most log(t). If you wanted to be really safe you could simply cap the possible utility of accomplishing any particular goal.
I'm missing something because this seems like a solid solution to me. I haven't read most of Eliezer's writings, unfortunately (no time, I tile my universe with math), so if there's a good one that discusses this I'd appreciate a link.
I think the missing piece is that it's really hard to formally-specify a scale of physical change.
I think the notion of "minimizing change" is secretly invoking multiple human brain abilities, which I suspect will each turn out to be very difficult to formalize. Given partial knowledge of a current situation S: (1) to predict the future states of the world if we take some hypothetical action, (2) to invent a concrete default / null action appropriate to S, and (3) to informally feel which of two hypothetical worlds is more or less "changed" with respect to...
Lo! A cartoon proof of Löb's Theorem!
Löb's Theorem shows that a mathematical system cannot assert its own soundness without becoming inconsistent. Marcello and I wanted to be able to see the truth of Löb's Theorem at a glance, so we doodled it out in the form of a cartoon. (An inability to trust assertions made by a proof system isomorphic to yourself, may be an issue for self-modifying AIs.)
It was while learning mathematical logic that I first learned to rigorously distinguish between X, the truth of X, the quotation of X, a proof of X, and a proof that X's quotation was provable.
The cartoon guide follows as an embedded Scribd document after the jump, or you can download as a PDF file. Afterward I offer a medium-hard puzzle to test your skill at drawing logical distinctions.
Cartoon Guide to Löb's ... by on Scribd
Cartoon Guide to Löb's Theorem - Upload a Document to Scribd
And now for your medium-hard puzzle:
The Deduction Theorem (look it up) states that whenever assuming a hypothesis H enables us to prove a formula F in classical logic, then (H->F) is a theorem in classical logic.
Let ◻Z stand for the proposition "Z is provable". Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C.
Applying the Deduction Theorem to Löb's Theorem gives us, for all C:
However, those familiar with the logic of material implication will realize that:
Applied to the above, this yields (not ◻C)->C.
That is, all statements which lack proofs are true.
I cannot prove that 2 = 1.
Therefore 2 = 1.
Can you exactly pinpoint the flaw?