Fast Initial Proof Searcher

There are many ways of initializing the proof searcher. But since proof verification is a fast business (e.g., [9]), we may construct an asymptotically optimal initialization called Bias-Optimal Proof Search (BIOPS)--see Section 2.3. BIOPS uses variants of Universal Search [22] and the Optimal Ordered Problem Solver OOPS [38,40] to efficiently search the space of online proof techniques: proof-generating programs that may read the Gödel machine's current state.²If some unknown proof technique $w$ would require at most $f(k)$ steps to produce a proof of difficulty measure $k$ (an integer depending on the nature of the task to be solved by the Gödel machine), then BIOPS will need at most $O(f(k))$ steps (Theorem 2.2).

That is, while the hardwired brute force theorem provers of AIXI(t,l) and HSEARCH systematically search in raw proof space--they can hide the proof search cost (exponential in proof size) in their asymptotic optimality notation [16,15]--the BIOPS of the initial, not yet self-improved Gödel machine already produces many proofs much faster. Unlike AIXI(t,l), a BIOPS-initialized Gödel machine can also profit from online proof search which may exploit information obtained through interaction with the environment.

The basic ideas of BIOPS, however, should be conceptually separated from those of the Gödel machine, whose proof searcher could be initialized in other ways as well. Unlike AIXI(t,l) and HSEARCH, the Gödel machine can improve the proof searcher itself, even if the latter is BIOPS, since the asymptotic optimality of BIOPS does not necessarily imply optimality with respect to the Gödel machine's utility function.

Back to Goedel machine home page