The Bayes Score Meliorizer

post by Scott Garrabrant · 2015-10-05T05:50:03.000Z · LW · GW · 0 comments

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 .

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

  3. Interpret each TM as a partial function from to , where sends to the 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 bits in time and only machines whose functions are defined on .

  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 th Turing machine dethrones the current king: a. Consider the set of all inputs on which both and the king are defined. b. Run a theorem prover for steps on each of these sentences in order, until you find one that can neither be proven or disproven in time . c. Let be the subset of sentences proven or disproven this way. d. Compute the probability which is the product of all the probabilities that assigns to the correct answer in . e. Compute the probability which is the product of all the probabilities that the king assigns to the correct answer in . f. If is at least , becomes the new king.

  7. Output the probability that the king assigns to .

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 which are indistinguishable from a rational probability coin.

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

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

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

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 , but not that much more.

0 comments

Comments sorted by top scores.