Jürgen Schmidhuber, who is one of the directors of IDSIA, wrote an interesting paper titled Gödel Machines: Self-Referential Universal Problem Solvers Making Provably Optimal Self-Improvements.

Given is an arbitrary computational problem whose solution may require interaction with a possibly reactive environment. For example, the goal may be to maximize the future expected reward of a robot. While executing its initial (possibly sub-optimal) problem solving strategy, the Gödel machine simultaneously runs a proof searcher which systematically and repeatedly tests proof techniques. Proof techniques are programs that may read any part of the Gödel machine's storage, and write on a reserved part which may be reset for each new proof technique test. In our example Gödel machine this writable storage includes the variables proof and switchprog, where switchprog holds a potentially unrestricted program whose execution could completely rewrite any part of the Gödel machine's current software. Normally the current switchprog is not executed. However, proof techniques may invoke a special subroutine check() which tests whether proof currently holds a proof showing that the utility of stopping the systematic proof searcher and transferring control to the current switchprog at a precisely defined point in the near future exceeds the utility of continuing the search until some alternative switchprog is found. Such proofs are derivable from the proof searcher's axiom scheme which formally describes the utility function to be maximized (typically the expected future reward in the expected remaining lifetime of the Gödel machine), the computational costs of hardware instructions (from which all programs are composed), and the effects of hardware instructions on the Gödel machine's state. The axiom scheme also formalizes known probabilistic properties of the environment, and also the initial Gödel machine state and software, which includes the axiom scheme itself (no circular argument here). Thus proof techniques can reason about expected costs and results of all programs including the proof searcher.

Seems like Eliezer S. Yudkowsky isn't the only one working on a Seed AI after all.

(thanks Calypso!)