SamEisenstat(Sam Eisenstat)

Karma: 132

SamEisenstat 16 May 2015 7:26 UTC
LW: 6 AF: 4
AF
on: An Informal Conjecture on Proof Length and Logical Counterfactuals
I (just yesterday) found a counterexample to this. The universe is a 5-and-10 variant that uses the unprovability of consistency:
```
def U():
  if A() == 2:
    if PA is consistent:
      return 10
    else:
      return 0
  else:
    return 5
```
The agent can be taken to be modal UDT, using PA as its theory. (The example will still work for other theories extending PA, we just need the universe’s theory to include the agents. Also, to simplify some later arguments we suppose that the agent uses the chicken rule, and that it checks action 1 first, then action 2.) Since the agent cannot prove the consistency of its theory, it will not be able to prove $A () = 2 \to U () = 10$ , so the first implication which it can prove is $A () = 1 \to U () = 5$ . Thus, it will end up taking action 1.

Now, we work in PA and try to show $A () = 2 \to U () = 0$ . If PA is inconsistent (we have to account for this case since we are working in PA), then $A () = 2 \to U () = 0$ follows straightforwardly. Next, we consider the case that PA is consistent and work through the agent’s decision. PA can’t prove $A () \neq 1$ , since we used the chicken rule, so since the sentence $A () = 1 \to U () = 5$ is easily provable, the sentence $A () = 1 \to U () = 10$ (ie. the first sentence that the agents checks for proofs of) must be unprovable.

The next sentence we check is $A () = 2 \to U () = 10$ . If the agent finds a proof of this, then it takes action 2. Otherwise, it moves on to the sentence $A () = 1 \to U () = 5$ , which is easily provable as mentioned above, and it takes action 1. Hence, the agent takes action 2 iff it can prove $A () = 2 \to U () = 10$ , so $A () = 2 \leftrightarrow □ (A () = 2 \to U () = 10) .$ Löb’s theorem tells us that $□ (U = 10) \leftrightarrow □ (□ (U = 10) \to U () = 10),$ so, by the uniqueness of fixed points, it follows that $A () = 2 \leftrightarrow □ (U = 10)$ . Then, we get $A () = 2 \to □ (U = 10)$ , so $A () = 2 \to □ (\neg □ ⊥)$ by the definition of the universe, and so $A () = 2 \to □ (⊥)$ by Gödel’s second incompleteness theorem. Thus, if the agent takes action 2, then PA is inconsistent, so $U () = 0$ as desired.

This tells us that $P A ⊢ A () = 2 \to U () = 0$ . Also, $P A ⊬ A () \neq 2$ by the chicken rule, so $P A ⊬ A () = 2 \to U () \neq 0$ . Since PA does not prove $A () = 2 \to U () \neq 0$ at all, the shortest proof of $P A ⊢ A () = 2 \to U () = 0$ is much shorter than the shortest proof of $A () = 2 \to U () \neq 0$ for any definition of “much shorter”. (One can object here that there is no shortest proof, but (a) it seems natural to define the “length of the shortest proof” to be infinite if there is no proof, and (b) it is probably straightforward but tedious to modify the agent and universe so that there is a proof of $A () = 2 \to U () \neq 0$ , but it is very long.)

However, it is clear that $U () = 0$ is not a legitimate counterfactual consequence of $A () = 2$ . Informally, if the agent chose action 2, it would have received utility 10, since PA is consistent. Thus, we have a counterexample.

One issue we discussed during the workshop is whether counterfactuals should be defined with respect to a state of knowledge. We may want to say here that we, who know a lot, are in a state of knowledge with respect to which $A () = 2$ would counterfactually result in $U () = 10$ , but that someone who reasons in PA is in a state of knowledge w.r.t. which it would result in $U () = 0$ . One way to think about this is that we know that PA is obviously consistent, irrespective of how the agent acts, whereas PA does not know that it is consistent, allowing an agent using PA to think of itself as counterfactually controlling PA’s consistency. Indeed, this is roughly how the argument above proceeds.

I’m not sure that this is a good way of thinking about this though. The agents goes through some weird steps, most notably a rather opaque application of the fixed point theorem, so I don’t have a good feel for why it is reasoning this way. I want to unwrap that argument before I can say whether it’s doing something that, on an intuitive level constitutes legitimate counterfactual reasoning.

More worryingly, the perspective of counterfactuals as being defined w.r.t. states of knowledge seems to be at odds with PA believing a wrong counterfactual here. It would make sense for PA not to have enough information to make any statement about the counterfactual consequences of $A () = 2$ , but that’s not what’s happening if we think of PA’s counterfactuals as obeying this conjecture; instead, PA postulates a causal mechanism by which the agent controls the consistency of PA, which we didn’t expect to be there at all. Maybe it would all make sense if I had a deeper understanding of the proof I gave, but right now it is very odd.

(This is rather long; perhaps it should be a post? Would anyone prefer that I clean up a few things and make this a post? I’ll also expand on the issue I mention at the end when I have more time to think about it.)
What links here?
- A Counterexample to an Informal Conjecture on Proof Length and Logical Counterfactuals by SamEisenstat (17 Jul 2015 17:34 UTC; 6 points)
- Musings on Exploration by Diffractor (3 Apr 2018 2:15 UTC; 1 point)

SamEisenstat 16 May 2015 21:05 UTC
LW: 3 AF: 2
AF
in reply to: Benya_Fallenstein’s comment on: An Informal Conjecture on Proof Length and Logical Counterfactuals
The argument that I had in mind was that if $P A ⊢ A () \neq 1$ , then $P A ⊢ □ ┌ A () \neq 1 ┐$ , so $P A ⊢ A () = 1$ since PA knows how the chicken rule works. This gives us $P A ⊢ ⊥$ , so PA can prove that if $P A ⊢ A () \neq 1$ , then PA is inconsistent. I’ll include this argument in my post, since you’re right that this was too big a jump.

Edit: We also need to use this argument to show that the modal UDT agent gets to the part where it iterates over utilities, rather than taking an action at the chicken rule step. I didn’t mention this explicitly, since I felt like I had seen it before often enough, but now I realize it is nontrivial enough to point out.

A Counterexample to an Informal Conjecture on Proof Length and Logical Counterfactuals

SamEisenstat17 Jul 2015 17:34 UTC

6 points

1 comment3 min readLW link

SamEisenstat 17 Jul 2015 17:50 UTC
0 points
AF
on: A Counterexample to an Informal Conjecture on Proof Length and Logical Counterfactuals
We can also construct an example where $P A ⊢ ϕ \to ψ$ with a short proof and $P A$ also proves $ϕ \to \neg ψ$ , but any such proof is much longer. We only need to put a bound on the proof length in A’s proof search. Then, the argument that $A () = 1 \land U () \neq 0$ proves its own consistency still works, and is rather short: $O (log n)$ as the proof length bound $n$ increases. However, there cannot be a proof of $A () = 1 \to U () = 10$ within $A$ ’s proof length bound, since if it found one it would immediately take action 1. In this case $P A$ can still prove that $A () = 1 \to U () = 10$ simply by running the agent, but this argument shows that any such proof must be long.

SamEisenstat 18 Jul 2015 1:07 UTC
0 points
AF
on: Optimal and Causal Counterfactual Worlds
Condition 4 in your theorem coincides with Lewis’ account of counterfactuals. Pearl cites Lewis, but he also criticizes him on the ground that the ordering on worlds is too arbitrary. In the language of this post, he is saying that condition 2 arises naturally from the structure of the problem and that condition 4 is derives from the deeper structure corresponding to condition 2.

I also noticed that the function $f$ and the partial order $≻$ can be read as “time of first divergence from the real world” and “first diverges before”, respectively. This makes the theorem a lot more intuitive.

SamEisenstat 30 Jul 2015 21:38 UTC
0 points
AF
on: Minimal intuitionistic logic as a setting for logical counterfactuals
Haskell doesn’t actually let you do this as far as I can tell, but the natural computational way to implement a function $B o t - > A$ is with a case expression with no cases. This is sensible because $B o t$ has no constructors, so it should be possible to pattern match it with such an expression. Another way of thinking of this is that we can use pattern matching on sum types and $B o t$ is just the $0$ -ary sum type.

SamEisenstat 5 Dec 2015 3:37 UTC
LW: 3 AF: 2
AF
on: Strict Dominance for the Modified Demski Prior
[EDIT: This all deals with measures, not semimeasures; see below.]

For $P$ to dominate $Q$ in the old sense means that its Bayes score can only be some constant worse than $Q$ , no worse, regardless of environment. My definition here implies that, but I think it’s a stricter requirement.

Your definition is equivalent to the standard definition. Li and Vitányi say that $P$ dominates $Q$ iff there is some $α \in R$ such that for any binary string $x$ , we have $α P (x) \geq Q (x)$ . Li and Vitányi’s “probability distributions” take a binary string as input while the probability distributions we are using ask for an element of a $σ$ -algebra, but we can abuse notation by allowing a binary string to represent the event of that the random sequence starts with this string as a prefix.

Theorem. For any probability distributions $P, Q$ on Cantor space and any $α$ , the condition $α P (x) \geq Q (x)$ holds for all binary strings $x$ iff it holds for all $x \in Σ$ .

Proof. The direction $⟸$ is immediate. For $⟹$ , suppose that $α P (x) \geq Q (x)$ for all binary string events $x$ . We first show that this property holds for every event in the algebra $A$ generated by the binary string events. We can write any $x \in A$ as a disjoint union of binary string events $x = ⋃_{i = 1}^{n} y_{i}$ . Then, $α P (x) = α n \sum i = 1 P (y_{i}) \geq n \sum i = 1 Q (y_{i}) = Q (x),$ as desired.

We can extend this to the $σ$ -algebra generated by $A$ , which is just the Borel $σ$ -algebra $Σ$ on Cantor space, by the monotone class theorem. I’m not sure how much measure theory you know, but you can think of this as a form of induction on measurable sets; if a property holds on an algebra of sets $A$ and it is preserved by countable monotone unions and intersections, then it holds on every set in the $σ$ -algebra generated by $A$ . For countable monotone unions, if we have $x_{1} \subseteq x_{2} \subseteq \dots$ , then $α P (\infty ⋃ i = 1 x_{i}) = sup i α P (x_{i}) \geq sup i Q (x_{i}) = Q (⋃ i x_{i}) .$ We can do the same thing for countable monotone intersections $x_{1} \supseteq x_{2} \supseteq \dots$ ; $α P (\infty ⋂ i = 1 x_{i}) = inf i α P (x_{i}) \geq inf i Q (x_{i}) = Q (⋂ i x_{i}) .$ $□$

EDIT: I’m talking about probability distributions $P$ rather than semimeasures. I don’t know how your definition of dominance is helpful for semimeasures though. The universal semimeasure $M$ is defined on binary sequences, and I think that question of whether $P$ dominates $M$ depends on how you extend it to the whole $σ$ -algebra. I expect that many reasonable extensions of $M$ would satisfy your Theorem 1, but this post (in particular the proof of Theorem 1) doesn’t seem to choose a specific such extension.

SamEisenstat 27 Aug 2016 5:21 UTC
0 points
AF
on: A new proposal for logical counterfactuals
I’m copying over some (lightly edited) conversation about this post from Facebook.

Sam Eisenstat: In the original counterexample to the Trolljecture, I guess you’re proposing that $C o n (P A)$ be logically prior to $A () = 1$ , so we can go back and replace $A () = 1$ with $A () = 2$ , but still have $C o n (P A)$ to use in order to derive $A () = 2 □ \to U () = 10$ ? Here I’m just using “ $□ \to$ ” to mean “counterfactually results in” without meaning to imply that this should be defined modally.

I agree that this is intuitively sensible, but it is difficult to give a general definition that agrees with intuition—it’s hard to even have an intuition in the general case. There has been some work along these lines though; see for example https://agentfoundations.org/item?id=241 though you may already know about this since you’ve been talking with Scott. I’m pessimistic about this direction in general, though I’d be happy to talk further about it.

Jack Gallagher: What’s the generator behind your being pessimistic?

Sam Eisenstat: Well, like Daniel suggests, we can ask whether the ordering is subjective/based on an agents epistemic state. Unlike Daniel, I think there are problems with this. The best examples are things like transparent Newcomb’s problem, where the agent needs to counterfact on things that it already knows the fact of the matter about. You can try to find loopholes in this, e.g. maybe the agent is doing something wrong if it isn’t ignorant of certain facts, but I haven’t been able to find something that’s satisfying (e.g. doesn’t fall to other thought experiments).

It thus seems that an agent should just counterfact on things even though it already knows them to be true, but this is a weird sort of thing to call “epistemic”. It doesn’t just depend on the agent’s probability assignments to various statements. Thus, to go farther here would seem to require a richer idea of “agent” than we presently have.

The alternative is an objective temporal ordering on logical statements. (This is a terrible use of the excluded middle, since “subjective” and “objective” are smuggling in a lot, so the place to look is probably somewhere that feels like a third option.) Anyway, it seems absurd for there to be a fact of the matter as to whether 417*596 = 248532 comes temporally before or after 251*622 = 156122.

Part of this is just a feeling of arbitrariness because even if one of those did come before the other, we don’t have to tools to know which one. Still, it seems the tools we do have are the wrong shape for building something that would work. For example, there seems to be an affinity between the ideas of being “easy”, of depending on few things, but being depended on by many, and of being temporally “early”. Patrick’s revived trolljecture is one attempt at formalizing it, but there was nothing deep about my counterexample, it’s just easy to generate statements that are difficult to evaluate. (There are a different versions of this, like independent statements in undecidable theories, or hard SAT instances in propositional logic.)

I used the word “we” in the last paragraph, but maybe you have type-theory tools that are more suited to this?

Daniel Satanove: It’s easier to come up with UDT when you have CDT. Is there a version of logical counterfactuals that works in more intuitive cases, but fail on stranger edge cases like transparent Newcomb’s?

Sam Eisenstat: The EDT of logical counterfactuals is just EDT with a prior over logic (e.g. bounded Demski, something more sophisticated). Proof-based UDT is a special case of this; it prescribes actions if any reasonable prior would agree, and is silent otherwise.

Unfortunately, as shown by the trolljecture counterexample, there are counterfactuals that proof-based UDT gets wrong (the trolljecture basically says that what proof-based UDT does should be read as counterfactuals), and therefore that EDT gets wrong given any reasonable prior, so it’s hard to define a “domain of validity” for this (not that that’s necessary for it be informative).

One candidate for the CDT of logical counterfactuals would just be putting a causal DAG structure on logical statements, like discussed in Scott’s forum post that I linked above. The TDT paper is informal, and I haven’t looked at it in a while, but I think that you can read it as proposing exactly this.

I believe that in all thought experiments where people have an intuition about what should be done, they are using this sort of reasoning plus strategy selection (i.e. updatelessness). I would be interested in seeing any thought experiments that people do not analyze in this way.

There isn’t much in the direction of actually defining such causal networks. Back when the trolljecture looked plausible we tried to interpret it in terms of causal networks, which didn’t quite work (see http://epsilonofdoom.blogspot.com/2015/08/provability-counterfactuals-vs-three.html). I expect something like Patrick’s revived trolljecture to be even harder to view in this way, since it’s inherently approximate; a notion of approximate causal network would be more appropriate here, if one could be found. I don’t know of any proposal that (1) actually defines a causal network and (2) works on some easy examples.

Well, that’s not entirely true. You can just pick any ordering that puts the agents decision at the beginning, and use the resulting fully-connected DAG. This works wherever proof-based UDT works, but fails on the trolljecture, exactly because it assumes anything that provably follows from your agent’s action is causally downstream of it.

Tsvi BT: “One candidate for the CDT of logical counterfactuals would just be putting a causal DAG structure on logical statements”

How does this interact with logical updatelessness? What happens to your DAG as you learn new facts?

Sam Eisenstat: I’m not sure if it’s obvious, but the idea is that each node has a full table of counterfactuals. An instance of this has more data than just an ordering.

It’s not intended to be updateless; it’s a CDT/TDT-style theory rather than UDT-style. You could layer strategy selection on top of it (though it could be computationally difficult if your DAG is hard to work with).

When you learn new facts you condition the probability distribution associated with the DAG on them, like for any Bayesian network.

Tsvi BT: So then this is dynamically inconsistent in the counterfactual mugging with a logical coin.

Sam Eisenstat: Oh yeah, “layer strategy selection on top” doesn’t work for logical uncertainty. Anyway, this was in response to Daniel’s request for a theory that “works in more intuitive cases”; I hope I didn’t give the impression that this would be hard to break.

On the other hand, you could try to “just do strategy selection” with respect to a particular prior if you’re willing to treat everything you learn as an observation. This is easy if you pick a coherent prior, but it’s uncomputable and it doesn’t let you pay counterfactual muggers with logical coins. Abram’s GLS stuff tries to do this with priors that don’t already know all logical facts. What do you think of that sort of approach?

Tsvi BT: I don’t have much more concrete to say. I currently view decision theory as being the questions of how to do logical updatelessness, and how to do strategy selection with a bounded reasoner. The GLS prior might be close, but there are basic open questions about how it works. “Strategic uncertainty” (or something) may or may not just boil down to logical uncertainty; the reason it might not is that you might actually have to define an optimization target other than “what Ideal Me thinks is the best strategy”, to take into account that actual versions of you are bounded in different ways. These two “components” (I wildly speculate) could combine to give a reflectively stable decision theory.

Daniel Satanove: Proof lengths probably aren’t the only way of doing the time step thing. Take the proof length definition of observation at time k, except delay all proofs of statements of the form a + b = c by one time step. This, or something sort of like this, will probably also work. Also any strictly increasing function on observation time should work.

The observation at time k should be an epistemic thing that describes how an agent learns of new theorems, rather than some fundamental property of math.

Jack Gallagher: What do you mean by “an epistemic thing”?

Daniel Satanove: “In order to break the cycles, we want some notion of logical time from which influence can only propagate forward. Proof length seems, at least to me, to be the most (only?) natural way to pull something like that off. A proof of length k can be thought of as a logical observation at time k.”

You are restricting yourself to agents who do a breadth first search through proofs rather than anything that can do a more directed approach. Saying that you want some notion of “logical time” kind of sounds like you want something that is a property of the math rather than a property of the agent.

SamEisenstat 27 Sep 2016 16:20 UTC
LW: 1 AF: 1
AF
on: The set of Logical Inductors is not Convex
Nicely done. I should have spent more time thinking about liar sentences; you really can do a lot with them.

Follow-up question—is the set of limits of logical inductors convex? (Your proof also makes me curious as to whether the set of “expanded limits” ${{liminf}_{n \to \infty} P_{n} (ϕ_{n})}_{¯ ¯ ¯ ϕ efficiently computable}$ is convex, though that question is a bit less nice than the other).

Logical inductor limits are dense under pointwise convergence

SamEisenstat6 Oct 2016 8:07 UTC

5 points

0 comments6 min readLW link

SamEisenstat 24 Apr 2017 5:08 UTC
0 points
AF
on: Generalizing Foundations of Decision Theory II
This isn’t too related to your main point, but every ordered field can be embedded into a field of Hahn series, which might be simpler to work with than surreals.

That page discusses the basics of Hahn series, but not the embedding theorem. (Ehrlich, 1995) treats things in detail, but is long and introduces a lot of definitions. The embedding theorem is stated on page 23 (24 in the pdf).

SamEisenstat 3 Jun 2017 0:24 UTC
LW: 2 AF: 2
AF
on: An Approach to Logically Updateless Decisions

In counterfactual mugging with a logical coin, AsDT always uses a logical inductor’s best-estimate of the utility it would get right now, so it sees the coin as already determined, and sees no benefit from giving Omega money in the cases where Omega asks for money.

The way I would think about what’s going on is that if the coin is already known at the time that the expectations are evaluated, then the problem isn’t convergent in the sense of AsDT. The agent that pays up whenever asked has a constant action, but it doesn’t receive a constant expected utility. You can think of the averaging as introducing artificial logical uncertainty to make more things convergent, which is why it’s more updateless. (My understanding is that this is pretty close to how you’re thinking of it already.)

SamEisenstat 10 Jun 2017 1:16 UTC
LW: 3 AF: 1
AF
in reply to: William_S’s comment on: Two Major Obstacles for Logical Inductor Decision Theory
It’s hard to analyze the dynamics of logical inductors too precisely, so we often have to do things that feel like worst-case analysis, like considering an adversarial trader with sufficient wealth. I think that problems that show up from this sort of analysis can be expected to correspond to real problems in superintelligent agents, but that is a difficult question. The malignancy of the universal prior is part of the reason.

As to your proposed solution, I don’t see how it would work. Scott is proposing that the trader makes conditional contracts, which are in effect voided if the event that they are conditional on doesn’t happen, so the trader doesn’t actually lose anything is this case. (It isn’t discussed in this post, but conditional contracts can be built out of the usual sort of bets, with payoffs given by the definition of conditional probability.) So, in order to make the trader lose money, the events need to happen sometimes, not just be expect to happen with some nonnegligable probability by the market.

SamEisenstat 10 Jun 2017 6:31 UTC
LW: 1 AF: 1
AF
in reply to: cousin_it’s comment on: Two Major Obstacles for Logical Inductor Decision Theory
Yeah, the 5 and 10 problem in the post actually can be addressed using provability ideas, in a way that fits in pretty natually with logical induction. The motivation here is to work with decision problems where you can’t prove statements $A = a \to U = u$ for agent $A$ , utility function $U$ , action $a$ , and utility value $u$ , at least not with the amount of computing power provided, but you want to use inductive generalizations instead. That isn’t necessary in this example, so it’s more of an illustration.

To say a bit more, if you make logical inductors propositionally consistent, similarly to what is done in this post, and make them assign things that have been proven already probability 1, then they will work on the 5 and 10 problem in the post.

It would be interesting if there was more of an analogy to explore between the provability oracle setting and the inductive setting, and more ideas could be carried over from modal UDT, but it seems to me that this is a different kind of problem that will require new ideas.

SamEisenstat 11 Jun 2017 23:21 UTC
0 points
AF
in reply to: abramdemski’s comment on: An Approach to Logically Updateless Decisions
Yeah, I like tail dependence.

There’s this question of whether for logical uncertainty we should think of it more as trying to “un-update” from a more logically informed perspective rather than trying to use some logical prior that exists at the beginning of time. Maybe you’ve heard such ideas from Scott? I’m not sure if that’s the right perspective, but it’s what I’m alluding to when I say you’re introducing artificial logical uncertainty.

SamEisenstat 5 Jul 2017 22:20 UTC
LW: 2 AF: 2
AF
on: Two Questions about Solomonoff Induction
Universal Prediction of Selected Bits solves the related question of what happens if the odd bits are adversarial but the even bits copy the preceding odd bits. Basically, the universal semimeasure learns to do the right thing, but the exact sense in which the result is positive is subtle and has to do with the difference between measures and semimeasures. The methods may also be relevant to the questions here, though I don’t see a proof for either question yet.

SamEisenstat 22 Jul 2017 12:03 UTC
0 points
AF
on: Some Criticisms of the Logical Induction paper
A few thoughts:

I agree that the LI criterion is “pointwise” in the way that you describe, but I think that this is both pretty good and as much as could actually be asked. A single efficiently computable trader can do a lot. It can enforce coherence on a polynomially growing set of sentences, search for proofs using many different proof strategies, enforce a polynomially growing set of statistical patterns, enforce reflection properties on a polynomially large set of sentences, etc. So, eventually the market will not be exploitable on all these things simultaneously, which seems like a pretty good level of accurate beliefs to have.

On the other side of things, it would be far to strong to ask for a uniform bound of the form “for every $ε > 0$ , there is some day $t$ such that after step $t$ , no trader can multiply its wealth by a factor more than $1 + ε$ ”. This is because a trader can be hardcoded with arbitrarily many hard-to-compute facts. For every $δ$ , there must eventually be a day $t^{'} > t$ on which the belief of your logical inductor assign probability less than $δ$ to some true statement, at which point a trader who has that statement hardcoded can multiply its wealth by $1 / δ$ . (I can give a construction of such a sentence using self-reference if you want, but it’s also intuitively natural—just pick many mutually exclusive statements with nothing to break the symmetry.)

Thus, I wouldn’t think of traders as “mistakes”, as you do in the post. A trader can gain money on the market if the market doesn’t already know all facts that will be listed by the deductive process, but that is a very high bar. Doing well against finitely many traders is already “pretty good”.

What you can ask for regarding uniformity is for some simple function $f$ such that any trader $T$ can multiply its wealth by at most a factor $f (T)$ . This is basically the idea of the mistake bound model in learning theory; you bound how many mistakes happen rather than when they happen. This would let you say a more than the one-trader properties I mentioned in my first paragraph. In fact, $L I A$ has this propery; $f (T)$ is just the initial wealth of the trader. You may therefore want to do something like setting traders’ initial wealths according to some measure of complexity. Admittedly this isn’t made explicit in the paper, but there’s not much additional that needs to be done to think in this way; it’s just the combination of the individual proofs in the paper with the explicit bounds you get from the initial wealths of the traders involved.

I basically agree completely on your last few points. The traders are a model class, not an ensemble method in any substantive way, and it is just confusing to connect them to the papers on ensemble methods that the LI paper references. Also, while I use the idea of logical induction to do research that I hope will be relevant to practical algorithms, it seems unlikely than any practical algorithm will look much like a LI. For one thing, finding fixed points is really hard without some property stronger than continuity, and you’d need a pretty good reason to put it in the inner loop of anything.

SamEisenstat 24 Jan 2018 3:04 UTC
LW: 4 AF: 3
AF
on: An Untrollable Mathematician
I at first didn’t understand your argument for claim (2), so I wrote an alternate proof that’s a bit more obvious/careful. I now see why it works, but I’ll give my version below for anyone interested. In any case, what you really mean is the probability of deciding a sentence outside of $Φ$ by having it announced by nature; there may be a high probability of sentences being decided indirectly via sentences in $Φ$ .

Instead of choosing $Φ$ as you describe, pick $Φ$ so that the probability $μ (Φ)$ of sampling something in $Φ$ is greater than $1 - μ (ψ) \cdot ε / 2$ . Then, the probability of sampling something in $Φ - {ψ}$ is at least $1 - μ (ψ) \cdot (1 + ε / 2)$ . Hence, no matter what sentences have been decided already, the probability that repeatedly sampling from $μ$ selects $ψ$ before it selects any sentence outside of $Φ$ is at least

$\begin{matrix} \infty \sum k = 0 (1 - μ (ψ) \cdot (1 + ε / 2))^{k} \cdot μ (ψ) & = \frac{μ (ψ)}{μ (ψ) \cdot (1 + ε / 2)} > 1 - ε / 2 \end{matrix}$

as desired.

Furthermore, this argument makes it clear that the probability distribution we converge to depends only on the set of sentences which the environment will eventually assert, not on their ordering!

Oh, I didn’t notice that aspect of things. That’s pretty cool.

SamEisenstat 14 Apr 2018 1:39 UTC
LW: 1 AF: 1
AF
on: No Constant Distribution Can be a Logical Inductor
Two minor comments. First, the bitstrings that you use do not all correspond to worlds, since, for example, $C o n (P A + C o n (P A))$ implies $C o n (P A)$ , as $P A$ is a subtheory of $P A + C o n (P A)$ . This can be fixed by instead using a tree of sentences that all diagonalize against themselves. Tsvi and I used a construction in this spirit in A limit-computable, self-reflective distribution, for example.

Second, I believe that weakening #2 in this post also cannot be satisfied by any constant distribution. To sketch my reasoning, a trader can try to buy a sequence of sentences $ϕ_{1}, ϕ_{1} \land ϕ_{2}, \dots$ , spending $$2^{-n}$ on the $n$th sentence $\phi_1 \wedge \dots \wedge \phi_n$. It should choose the sequence of sentences so that $\phi_1 \wedge \dots \wedge \phi_n$ has probability at most $2^{-n}$, and then it will make an infinite amount of money if the sentences are simultaneously true.

The way to do this is to choose each $ϕ_{n}$ from a list of all sentences. If at any point you notice that $ϕ_{1} \land \dots \land ϕ_{n}$ has too high a probability, then pick a new sentence for $ϕ_{n}$ . We can sell all the conjunctions $ϕ_{1} \land \dots \land ϕ_{k}$ for $k \geq n$ and get back the original amount payed by hypothesis. Then, if we can keep using sharper continuous tests of the probabilities of the sentences $ϕ_{1} \land \dots \land ϕ_{n}$ over time, we will settle down to a sequence with the desired property.

In order to turn this sketch into a proof, we need to be more careful about how these things are to be made continuous, but it seems routine.

SamEisenstat 8 May 2018 20:01 UTC
LW: 10 AF: 7
AF
on: Open question: are minimal circuits daemon-free?
I’m having trouble thinking about what it would mean for a circuit to contain daemons such that we could hope for a proof. It would be nice if we could find a simple such definition, but it seems hard to make this intuition precise.
For example, we might say that a circuit contains daemons if it displays more optimization that necessary to solve a problem. Minimal circuits could have daemons under this definition though. Suppose that some function $f$ describes the behaviour of some powerful agent, a function $~ f$ is like $f$ with noise added, and our problem is to predict sufficiently well the function $~ f$ . Then, the simplest circuit that does well won’t bother to memorize a bunch of noise, so it will pursue the goals of the agent described by $f$ more efficiently than $~ f$ , and thus more efficiently than necessary.

SamEisenstat(Sam Eisenstat)

A Coun­terex­am­ple to an In­for­mal Con­jec­ture on Proof Length and Log­i­cal Counterfactuals

Log­i­cal in­duc­tor limits are dense un­der poin­t­wise convergence

A Counterexample to an Informal Conjecture on Proof Length and Logical Counterfactuals

Logical inductor limits are dense under pointwise convergence