We present the first class of mathematically rigorous, general, fully self-referential, self-improving, optimally efficient problem solvers. Inspired by Kurt Gödel’s celebrated self-referential formulas (1931), a Gödel machine (or ‘Goedel machine’ but not ‘Godel machine’) rewrites any part of its own code as soon as it has found a proof that the rewrite is useful, where the problem-dependent utility function and the hardware and the entire initial code are described by axioms encoded in an initial proof searcher which is also part of the initial code.
Since that architecture uses a theorem proving system, and creates new versions of itself, and can even replace its own theorem proving system, it naively seems like the Löbstacle might come up. Are you familiar with Schmidhuber’s group’s work? Does it seem like their work will run into the Löbstacle and they’re just not talking about it? Or does it seem like their architecture makes worries about the Löbstacle irrelevant via some clever architecting?
Basically, my question is “The Löbstacle and Gödel Machines… what’s up with them?” :-)
This is several months too late, but yes! Gödel Machines runs into the Löbstacle, as seen in this MIRI paper. From the paper:
it is clear that the obstacles we have encountered
apply to Gödel machines as well. Consider a Gödel machine G1 whose fallback
policy would “rewrite” it into another Gödel machine G2 with the same suggester
(proof searcher, in Schmidhuber’s terminology). G1’s suggester now wants to
prove that it is acceptable to instead rewrite itself into G0
2
, a Gödel machine
with a very slightly modified proof searcher. It must prove that G0
2 will obtain
at least as much utility as G2. In order to do so, naively we would expect that
G0
2 will again only execute rewrites if its proof searcher has shown them to be
useful; but clearly, this runs into the Löbian obstacle, unless G1 can show that
theorems proven by G0
2 are in fact true.
Perhaps this is the wrong venue, but I’m curious how this work generalizes and either applies or doesn’t apply to other lines of research.
Schmidhuber’s group has several papers on “Goedel machines” and it seems like they involve the use of proofs to find self-rewrites.
Their 2005 paper “Completely Self-Referential Optimal Reinforcement Learners” explained the design and their 2012 paper “Towards an Actual Gödel Machine Implementation” seems to be working towards making something vaguely practical. This is the same group whose PhD students helped founded of DeepMind (like Shane Legg as founder and several others as very early employees). Deepmind was then acquired by Google in 2014.
Since that architecture uses a theorem proving system, and creates new versions of itself, and can even replace its own theorem proving system, it naively seems like the Löbstacle might come up. Are you familiar with Schmidhuber’s group’s work? Does it seem like their work will run into the Löbstacle and they’re just not talking about it? Or does it seem like their architecture makes worries about the Löbstacle irrelevant via some clever architecting?
Basically, my question is “The Löbstacle and Gödel Machines… what’s up with them?” :-)
This is several months too late, but yes! Gödel Machines runs into the Löbstacle, as seen in this MIRI paper. From the paper: