We came up with another logical predictor proposal at MIRIxLA today. We were excited about it for a while, but it turned out to not to do much better than the Benford learner. I am writing it up, in case I or someone else wants to think about it later.

Consider the following probabilistic algorithm, which assigns probabilities to logical sentences (encoded by Godel numbers)

1. Input $N$.

2. Sample a sequence of $N$ Turing machines, each of which output an infinite sequence of rational numbers.

3. Interpret each TM as a partial function $f_i$ from $N$ to $[0,1]$, where $f_i$ sends $n$ to the $n$th number output, and in undefined if the output is not between 0 and 1

4. Restrict the sequence to only machines that output the first $n$ bits in time $2^n$ and only machines whose functions are defined on $N$.

5. The first function in the sequence starts out as the king. Each Turing machine one at a time in order tries to dethrone the current king.

6. To check whether or not the $n$th Turing machine dethrones the current king: a. Consider the set $S$ of all inputs on which both $f_n$ and the king are defined. b. Run a theorem prover for $N$ steps on each of these sentences in order, until you find one that can neither be proven or disproven in time $N$. c. Let $S^{\prime }$ be the subset $S$ of sentences proven or disproven this way. d. Compute the probability $P$ which is the product of all the probabilities that $f_n$ assigns to the correct answer in $S^{\prime }$. e. Compute the probability $Q$ which is the product of all the probabilities that the king assigns to the correct answer in $S^{\prime }$. f. If $P$ is at least $nQ$, $f_n$ becomes the new king.

7. Output the probability that the king assigns to $N$.

This algorithm did not turn out to be as good as I originally thought it would be, and I probably wont do a good write up on all the properties of this algorithm. (If this opinion changes, I will write a lot more.) However, let me give a proof sketch that this algorithm is at least reasonable enough to get the Generalized Benford Test for subsequences $s$ which are indistinguishable from a rational probability $p$ coin.

Proof Sketch: Consider the machine $T$ which only outputs probabilities on the subsequence $s$, and always outputs $p$ . When $N$ is large, with probability almost 1, thin Turing machine will be sampled. With probability $1-\epsilon$, all of the Turing machines sampled before $T$ will have complexity at most $k$, where $k$ is a function only of $T$ and $\epsilon .$

For $N$ sufficiently large, all of these Turing machines of complexity at most $k$, will either be able to be dethroned by $T$, or will assign probabilities such that the product of all the probabilities it assigns to the correct answers in its intersection with $T$ is asymptotically at least a nonzero constant times the probability that $T$ assigns. (Any Turing machine which does asymptotically much worse than $T$ will be dethroned by $T$ for sufficiently large $N$) Therefore $T$ is sampled and becomes king. (or the previous king is at most a constant worse than $T$.)

However, no future Turing machine can ever dethrone $T$ (or the machine that was good enough to stop $T$ from being king), since it would have to do much better on a quickly computable sub-sequence of $s$. Therefore, the king is either $T$ or something that does asymptotically at least a constant worse than $T$. Any such algorithm must converge to probability $p$.

$\square$

The main reason is that I am not satisfied with this algorithm enough to write up more about it is that I do not think that it does at least as well as everything it samples, in the cases where the true environment is not well described by any one Turing machine sampled. I suspect that something similar to this might be enough to satisfy the generalized Benford test for all possible $p$, but not that much more.