Bias-Optimal Proof Search (BIOPS)

There are many ways of initializing the Gödel machine's proof searcher. Here we construct a $p(1)$ that is optimal in a certain limited sense to be described below, but not necessarily optimal in the potentially different and more powerful Gödel machine sense embodied by the given utility function. We introduce Bias-Optimal Proof Search (BIOPS) which essentially is an application of the recent Optimal Ordered Problem Solver OOPS [38,40] to a sequence of proof search tasks.

As long as $p=p(1)$ (which is true at least as long as no target theorem has been found), $p$ searches a space of self-delimiting [23,6,25,38] programs written in $\cal L$. The reader is asked to consult previous work for details [38,40]; here we just outline the basic procedure: any currently running proof technique $w$ is an instruction sequence (whose bitstring-encoded representation starts somewhere in $s^p$) which is read incrementally, instruction by instruction. Each instruction is immediately executed while being read; this may modify $s^p$, and may transfer control back to a previously read instruction (e.g., a loop). To read and execute a previously unread instruction right after the end of the proof technique prefix read so far, $p$ first waits until the execution of the prefix so far explicitly requests such a prolongation, by setting an appropriate signal in the internal state. Prefixes may cease to request any further instructions--that's why they are called self-delimiting. So the proof techniques form a prefix code, e.g., [25]: no proof technique that at some point ceases to request a prolongation of its code can be prefix of another proof technique.

Now to our limited notion of initial optimality. What is a good way of systematically testing proof techniques? BIOPS starts with a probability distribution $P$ on the proof techniques $w$ written in language $\cal L$. $P$ represents the searcher's initial bias. $P(w)$ could be based on program length, e.g., $P(w)=2^{-l(w)}$ for binary programs $w$ [23,25], or on a probabilistic version of the syntax diagram of $\cal L$, where the diagram's edges are labeled with transition probabilities [38,40]. BIOPS is near-bias-optimal in the sense that it will not spend more time on any proof technique than it deserves, according to the probabilistic bias, namely, not more than its probability times the total search time:

Definition 2.1 (Bias-Optimal Searchers [38,40])   Let $\cal R$ be a problem class, $\cal C$ be a search space of solution candidates (where any problem $r \in \cal R$ should have a solution in $\cal C$), $P(q \mid r)$ be a task-dependent bias in the form of conditional probability distributions on the candidates $q \in \cal C$. Suppose that we also have a predefined procedure that creates and tests any given $q$ on any $r \in \cal R$ within time $t(q,r)$ (typically unknown in advance). Then a searcher is $n$-bias-optimal ($n \geq 1$) if for any maximal total search time $T_{total} > 0$ it is guaranteed to solve any problem $r \in \cal R$ if it has a solution $p \in \cal C$ satisfying $t(p,r) \leq P(p \mid r) T_{total}/n$. It is bias-optimal if $n=1$.

The $k$-th proof search task of BIOPS ( $k=1, 2, \ldots$) will be to find a proof of a target theorem applicable to the state of the Gödel machine shortly after the point where the theorem is found. The first such proof may actually provoke a complete Gödel machine rewrite that abolishes BIOPS. So Subsection 2.3.1 will focus just on the very first proof search task. Subsection 2.3.3 will then address the case where the proof searcher has survived the most recent task's solution and wants to profit from earlier solved tasks when possible.

Back to Goedel machine home page