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.
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: