Godel Machines

I recently read about Jeurgen Schmidhuber’s Godel Machines and presented the topic for David Duvenaud’s Learning to Search course. It was a pretty enlightening experience; I hadn’t really gone in depth on any of Schmidhuber’s ideas before. I’m going to summarize the idea and add some commentary here.

In general, the Godel Machine and the Optimal Ordered Problem Solvers paper (which I also looked through) seem more like extended abstracts when compared against more recent machine learning papers. They provide an outline for how artificial general intelligence might be developed. While we may not be to recreate exact instantiations of the template now, they certainly can serve as inspiration.

The Godel Machine details how an asymptotically optimal computer program \(p\) might be created to solve the problem of maximizing expected future reward. There are two parts running simultaneously (the simplest version is two threads): a solver and a searcher. The solver is an algorithm that interacts with the environment and collects rewards. The searcher is where the magic happens—-its goal is to search for provably better rewrites of itself. In particular, the goal of the searcher is to generate (switch-program, proof) pairs where the proof states:

“The immediate re-write of p through switch-program has higher utility than leaving p as is”

The Godel Machine then loads this new program and carries on with a new solver and searcher. The higher utility from the switch can be due to a better solver, a better proof searcher, or some intricate combination of both. At first glance, this approach feels greedy. How do we know that we are not missing some better solution that might be obtained if we continued searching with the current program?

The answer is that this potential for better solutions is baked into the expected utility of the current program, which captures the benefit we may get from future proofs. Thus, making the switch is optimal. Schmidhuber coins this the Global Optimality Theorem. This has an additional nice interpretation of collapsing the recursion: “Any proof of a target theorem automatically proves that the corresponding self-modification is good for all further self-modifications affected by the present one, in recursive fashion. In that sense all possible ‘meta-levels’ of the self-referential system are collapsed into one.”

Some thoughts: assuming the existence of a searcher that can compute this expected utility function almost feels like cheating. Following the logic of reductions, if we believe that Godel Machine can solve AGI, then creating a Godel Machine must be as hard as creating AGI. The proof searcher is also clearly the crucially hard component, since the solver is basically just an initialization. There’s some recent work suggesting how the Godel Machine may be practically implemented [B. R. Steunebrink, J. Schmidhuber. Towards an Actual Gödel Machine Implementation.], but it looks still a ways away. Perhaps the natural thing to do if creating the searcher is too hard is to create approximations instead.

Finally, a really beautiful Schmidhuber quote from his podcast episode with Lex Fridman: “All the history of science is a history of compression.” (meaning: Progress in science can be thought of as simpler explanations of natural phenomena.)