Benya_Fallenstein(Benya Fallenstein)

Karma: 266

Benya_Fallenstein 14 Jul 2015 4:02 UTC
0 points
AF
in reply to: Benya_Fallenstein’s comment on: Waterfall Truth Predicates
We should be more careful, though, about what we mean by saying that $φ (x)$ only depends on ${T r}_{m}$ for $m > n$ , though, since this cannot be a purely syntactic criterion if we allow quantification over the subscript (as I did here). I’m pretty sure that something can be worked out, but I’ll leave it for the moment.

Benya_Fallenstein 14 Jul 2015 3:57 UTC
LW: 2 AF: 1
AF
on: Waterfall Truth Predicates
I would suggest changing this system by defining $ψ (n)$ to mean that no $m \leq n$ is the Gödel number of a proof of an inconsistency in ZFC (instead of just asserting that $n$ isn’t). The purpose of this is to make it so that if ZFC were inconsistent, then we only end up talking about a finite number of levels of truth predicate. More specifically, I’d define $T_{n}$ to be PA plus the axiom schema

$\forall m \geq n . ψ (m) \to \forall x . {T r}_{m} (┌ φ (¯ ¯ ¯ x) ┐) \leftrightarrow φ (x) .$

Then, it seems that Jacob Hilton’s proof that the waterfalls are consistent goes through for this waterfall:

Work in ZFC and assume that ZFC is inconsistent. Let $n$ be the lowest Gödel number of a proof of an inconsistency. Let $M$ be the following model of our language: Start with the standard model of PA; it remains to give interpretations of the truth predicates. If $m \geq n$ , then ${T r}_{m} (k)$ is false for all $k$ . If $m < n$ , then ${T r}_{m} (k)$ is true iff $k$ is the Gödel number of a true formula involving only ${T r}_{m^{'}}$ for $m^{'} > m$ . Then, it’s clear that $T_{0}$ , and hence all $T_{m}$ (since $T_{0}$ is the strongest of the systems) is sound on $M$ , and therefore consistent.

Thus, we have proven in ZFC that if ZFC is inconsistent, then $T_{0}$ is consistent; or equivalently, that if $T_{0}$ is inconsistent, then ZFC is consistent. Stepping out of ZFC, we can see that if $T_{0}$ is inconsistent, then ZFC proves this, and therefore in this case ZFC proves its own consistency, implying that it is inconsistent. Hence, if ZFC is consistent, then so is $T_{0}$ .

(Moreover, we can formalize this reasoning in ZFC. Hence, we can prove in ZFC (i) that if ZFC is inconsistent, then $T_{0}$ is consistent, and (ii) that if ZFC is consistent, then $T_{0}$ is consistent. By the law of the excluded middle, ZFC proves that $T_{0}$ is consistent.)

Benya_Fallenstein 3 Jun 2015 18:29 UTC
LW: 1 AF: 1
AF
in reply to: János Kramár’s comment on: No Good Logical Conditional Probability
Hm; we could add an uninterpreted predicate symbol $Q (n)$ to the language of arithmetic, and let $s \equiv Q (0)$ and $r_{n} \equiv Q (¯ ¯¯¯¯¯¯¯¯¯¯¯ ¯ n + 1)$ . Then, it seems like the only barrier to recursive enumerability of $T_{\infty}$ is that $P$ ’s opinions about $Q (\cdot)$ aren’t computable; this seems worrying in practice, since it seems certain that we would like logical uncertainty to be able to reason about the values of computations that use more resources than we use to compute our own probability estimates. But on the other hand, all of this makes this sound like an issue of self-reference, which is its own can of worms (once we have a computable process assigning probabilities to the value of computations, we can consider the sentence saying “I’m assigned probability $< \frac{1}{2}$ ” etc.).

Benya_Fallenstein 2 Jun 2015 20:03 UTC
LW: 2 AF: 1
AF
on: Agents that can predict their Newcomb predictor

The other direction follows from the fact that the algorithm is bounded, and PA can simply show the execution trace of $A$ in $\leq C N$ steps.

Unimportant technical point: I think the length of the PA proof grows faster than this. (More precisely, the length in symbols, rather than the length in number of statements; we’re almost always interested in the former, since it determines how quickly a proof can be checked or be found by exhaustive search.) The obvious way of showing $A () = 1$ in PA is to successively show for higher and higher $t$ that “after $t$ ticks, the Turing machine computing $A ()$ is in the following state, and its tapes have the following content”. But even to write out the contents of the tape of a Turing machine that has run for $t$ ticks will in general take $t$ symbols. So the obvious way of doing the proof takes at least $O (t^{2})$ symbols. Moreover, I’m not sure whether we can get from “at time $t$ , the configuration is such-and-such” to “at time $t + 1$ , the configuration is such-and-such” in a constant number of proof steps. I suspect we don’t need more than $O (t^{3})$ symbols overall, but I’m not extremely confident. (I’d be quite surprised if the time turned out not to be polynomial, though!)

Benya_Fallenstein 16 May 2015 16:38 UTC
LW: 2 AF: 1
AF
in reply to: SamEisenstat’s comment on: An Informal Conjecture on Proof Length and Logical Counterfactuals

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.

It seems like this argument needs soundness of PA, not just consistency of PA. Do you see a way to prove in PA that if $P A ⊢ A () \neq 1$ , then PA is inconsistent?

[edited to add:] However, your idea reminds me of my post on the odd counterfactuals of playing chicken, and I think the example I gave there makes your idea go through:

The scenario is that you get 10 if you take action 1 and it’s not provable that you don’t take action 1; you get 5 if you take action 2; and you get 0 if you take action 1 and it’s provable that you don’t. Clearly you should take action 1, but I prove that modal UDT actually takes action 2. To do so, I show that PA proves $A () = 1 \to \neg □ ┌ A () = 1 ┐$ . (Then from the outside, $A () = 2$ follows from the outside by soundness of PA.)

This seems to make your argument go through if we can also show that PA doesn’t show $A () \neq 1$ . But if it did, then modal UDT would take action 1 because this comes first in its proof search, contradiction.

Thus, PA proves $A () = 1 \to U () = 0$ (because this follows from $A () = 1 \to \neg □ ┌ A () = 1 ┐$ ), and also PA doesn’t prove $A () = 1 \to U () = 10$ . As in your argument, then, the trolljecture implies that we should think “if the agent takes action 1, it gets utility 0” is a good counterfactual, and we don’t think that’s true.

Still interested in whether you can make your argument go through in your case as well, especially if you can use the chicken step in a way I’m not seeing yet. Like Patrick, I’d encourage you to develop this into a post.
What links here?
- Proof Length and Logical Counterfactuals Revisited by orthonormal (10 Feb 2016 18:56 UTC; 3 points)

Benya_Fallenstein 6 May 2015 2:41 UTC
LW: 1 AF: 1
AF
in reply to: Diffractor’s comment on: Reflective probabilistic logic cannot assign positive probability to its own coherence and an inner reflection principle
If you replace the inner “ $= 1$ ” by “ $> 1 - ϵ$ ”, then the literal thing you wrote follows from the reflection principle: Suppose that the outer probability is $< 1$ . Then

$P [(a < P [φ] < b) \land P [a - ϵ < P [φ] < b + ε] \leq 1 - ϵ] > 0.$

Now, $P [a < P [φ] < b] > 0$ implies $P [a \leq P [φ] \leq b] > 0$ , which by the converse of the outer reflection principle yields $a \leq P [φ] \leq b$ , whence $a - ϵ < P [φ] < b + ϵ$ . Now, by the forward direction of the outer reflection principle, we have

$P [a - ϵ < P [φ] < b + ϵ] = 1 > 1 - ϵ,$

which, by the outer reflection principle again, implies

$P [P [a - ϵ < P [φ] < b + ϵ] > 1 - ϵ] = 1,$

a contradiction to the assumption that $\dots \leq 1 - ϵ$ had outer probability $> 0$ .

However, what we’d really like is an inner reflection principle that assigns probability one to the statement *quantified over all $a$ , $b$ , and Gödel numbers $┌ φ ┐$ . I think Paul Christiano has a proof that this is impossible for small enough $ϵ$ , but I don’t remember how the details worked.

Benya_Fallenstein 28 Apr 2015 0:40 UTC
LW: 2 AF: 1
AF
on: Paraconsistent Tiling Agents (Very Early Draft)
This is very interesting!

My main question, which I didn’t see an answer to on my first read, is: If the agent proves that action $a$ leads to the goal $G$ being achieved, are there any conditions under which this implies that the goal actually is achieved? The procrastination paradox shows that this isn’t true in general. Is there a class of sentences (e.g., all $Π_{1}$ sentences, though I don’t expect that to be true in this case) such that if $P A ⋆ ⊢ φ$ then $N ⊨ φ$ ? In other words, do we have some guarantee that we do better at actually achieving $G$ than an agent which uses the system $B A D := P A + C o n (B A D)$ ?

A more technical point: Given that you claim that Theorem 3.2 (reflectively coherent quantified belief) follows “trivially” from Theorem 2.4, you presumably mean Theorem 2.4 to state that $P A ⋆ ⊢ \forall x . □ ┌ φ (¯ ¯ ¯ x) ┐ \to φ (x)$ , rather than $P A ⋆ ⊢ \forall x . □ ┌ φ ┐ \to φ$ . (Even if you consider $φ$ to implicitly contain an occurrence of $x$ , it is essential that in $□ ┌ φ (¯ ¯ ¯ x) ┐$ the free variable is replaced by the numeral corresponding to the outer value of $x$ .)

Benya_Fallenstein 24 Mar 2015 17:42 UTC
LW: 2 AF: 1
AF
in reply to: Stuart_Armstrong’s comment on: Forum Digest: Corrigibility, utility indifference, & related control ideas
Categorization is hard! :-) I wanted to break it up because long lists are annoying to read, but there was certainly some arbitrariness in dividing it up. I’ve moved “resource gathering agent” to the odds & ends.

Benya_Fallenstein 22 Mar 2015 1:33 UTC
LW: 4 AF: 1
AF
in reply to: So8res’s comment on: Identity and quining in UDT
Want to echo Nate’s points!

One particular thing that I wanted to emphasize is that I think you can see as a thread on this forum (in particular, the modal UDT work is relevant) is that it’s useful to make formal toy models where the math is fully specified, so that you can prove theorems about what exactly an agent would do (or, sometimes, write a program that figures it out for you). When you write out things that explicitly, then, for example, it becomes clearer that you need to assume that a decision problem is “fair” (extensional) to get certain results, as Nate points out (or if you don’t assume it, someone else can look at your result and point out that it’s not true as stated). In your post, you’re using “logical expectations” that condition on something being true, without defining exactly what all of this means, and as a result you can argue about what these agents will do, but not actually prove it; that’s certainly a reasonable part of the research process, but I’d like to encourage you to turn your work into models that are fully specified, so that you can actually prove theorems about them.

Benya_Fallenstein 17 Mar 2015 21:06 UTC
LW: 2 AF: 1
AF
on: Meta- the goals of this forum
Some additions about how the initial system is going to work:
- Non-member contributions (comments and links) are going to become publicly visible when they have received 2 likes (from members—only members can like things).
- However, members will be able to reply to a contribution as soon as it has received 1 like. This means that if you think someone’s made a useful contribution, and you want to reply to them about it, you don’t have to wait for a second person to Like it before you can write that reply. (It won’t be publicly visible until the contribution has two Likes, though.)

Benya_Fallenstein 3 Feb 2015 20:56 UTC
0 points
AF
in reply to: orthonormal’s comment on: Third-person counterfactuals
Yeah, that sounds good! Of course, by the Kripke levels argument, it’s sufficient to consider $ϕ$ ’s of the form $\neg □^{n} ⊥$ . And we might want to have a separate notion of ” $i$ leads to $j$ at level $n$ ”, which we can actually implement in a finite modal formula. This seems to suggest a version of modal UDT that tries to prove things in PA, then if that has ambiguous counterfactuals (i.e., it can’t prove $A_{i} \to U_{j}$ for any $j$ ) we try PA+1 and so on up to some finite $n$ ; then we can hope these versions of UDT approximate optimality according to your revised version of ” $i$ leads to $j$ ” as $n \to \infty$ . Worth working out!

Benya_Fallenstein 3 Feb 2015 1:25 UTC
LW: 2 AF: 1
AF
in reply to: orthonormal’s comment on: Third-person counterfactuals

Fixed—thanks, Patrick!

Regarding the example, I earlier defined “action $i$ leads to outcome $j$ ” to mean the conjunction of $G L ⊢ A_{i} \to U_{j}$ and $G L ⊬ \neg A_{i}$ ; i.e., we check for spurious counterfactuals before believing that $G L ⊢ A_{i} \to U_{j}$ tells us something about what action $i$ leads to, and we only consider ourselves “fully informed” in this sense if we have non-spurious information for each $i$ . (Of course, my follow-up post is about how that’s still unsatisfactory; the reason to define this notion of “fully informative” so explicitly was really to be able to say more clearly in which sense we intuitively have a problem even when we’ve ruled out the problems of ambiguous counterfactuals and not enough counterfactuals.)

Benya_Fallenstein 23 Nov 2014 22:17 UTC
0 points
AF
in reply to: abramdemski’s comment on: From halting oracles to modal logic
(Thanks for the feedback!)

Benya_Fallenstein 21 Nov 2014 8:02 UTC
0 points
AF
on: Trustworthy automated philosophy?
In our chat about this, Eliezer said that, aside from the difficulty of making a human-level mathematical philosophy engine aligned with our goals, an additional significant relevant disagreement with Paul is that Eliezer thinks it’s likely that we’ll use low-level self-improvement on the road to human-level AI; he used the analogies of programmers using compilers instead of writing machine code directly, and of EURISKO helping Lenat. (Again, hoping I’m not misrepresenting.)

This seems like a plausible scenario to me, but I’m not convinced it argues for the kind of work we’re doing currently; it seems fairly likely to me that “reliably helping the programmers to do low-level tasks on the way to human-level AI” can probably be handled by having a small protected metalayer, which only the humans can modify. This sort of architecture seems very problematic for an AI acting in the world—it makes Cartesian assumptions, and we don’t want something that’s bound to a single architecture like that—which is why we haven’t been looking in this direction, but if this is a significant reason for studying self-reference, we should be exploring obvious tricks involving a protected metalayer.

For example, the Milawa theorem prover has a small initial verifier, which can be replaced by a different verifier that accepts proofs in a more powerful language, given a proof that the new verifier only outputs theorems that the old verifier would also have outputted on some input. How does this avoid running into the Löbstacle? (I.e., how can the new verifier also allow the user to replace it given a proof of the analogous theorem in its language?) The answer is, by having a protected metalevel; the proof that the new verifier only outputs theorems the old verifier would have outputted does not need to prove anything about the code that is willing to switch out the new verifier for an even newer verifier.

Benya_Fallenstein 21 Nov 2014 7:18 UTC
0 points
AF
in reply to: Benya_Fallenstein’s comment on: Approximability
...though although I’m guessing the variant of the reflective oracle discussed in the comment thread may be approximable, it seems less likely that a version of AIXI can be defined based on it that would be approximable.

Benya_Fallenstein 21 Nov 2014 3:14 UTC
LW: 1 AF: 1
AF
on: Approximability
Sorry for the delayed reply! I like this post, and agree with much of what you’re saying. I guess I disagree with the particular line you draw, though; I think there’s an interesting line, but it’s at “is there a Turing machine which will halt and give the answer to this problem” rather than “is there a Turing machine which will spit out the correct answer for a large enough input (but will spit out wrong answers for smaller inputs, and you don’t know what number is large enough)”. The latter of these doesn’t seem that qualitatively different to me from “is there a Turing machine which will give you the correct answer if you give it two large enough numbers (but will spit out wrong answers if the numbers aren’t large enough, and what is ‘large enough’ for the second number depends on what the first number you give it is)”, which takes you one more level up the arithmetic hierarchy; the line between the first and the second seems more significant to me than the line between the second and the third.

Regarding the reflective oracle result, yes the version presented in the post is higher up in the arithmetic hierarchy, but I think the variant discussed in this comment thread with Paul is probably approximable. As I said above, though, I’m not convinced that that’s actually the right place to put the line. Also, there’s of course an “AIXItl-like version” which is computable by limiting itself to hypotheses with bounded source code length and computation time. But most importantly in my mind, I don’t actually think it would make sense for any actual agent to compute an oracle like this; the point is to define a notion of perfect Bayesian agent which can reason about worlds containing other perfect Bayesian agents, in the hope that this model will yield useful insights about the real world of logically uncertain agents reasoning about worlds containing other logically uncertain agents, and these logically uncertain agents certainly don’t reason about each other by computing out an “oracle” first.

Benya_Fallenstein 21 Nov 2014 3:00 UTC
0 points
AF
in reply to: paulfchristiano’s comment on: Stable self-improvement as a research problem
I think the main disagreement is about whether it’s possible to get an initial system which is powerful in the ways needed for your proposal and which is knowably aligned with our goals; some more about this in my reply to your post, which I’ve finally posted, though there I mostly discuss my own position rather than Eliezer’s.

Benya_Fallenstein 16 Nov 2014 4:29 UTC
0 points
AF
in reply to: paulfchristiano’s comment on: “Evil” decision problems in provability logic
Actually, drnickbone’s original LessWrong post introducing evil problems also gives an extension to the case you are considering: The evil decision problem gives the agent three or more options, and rewards the one that the “victim” decision theory assigns the least probability to (breaking ties lexicographically). Then, no decision theory can put probability $> 1 / N$ on the action that is rewarded in its probabilistic evil problem.

Benya_Fallenstein 12 Nov 2014 1:18 UTC
LW: 3 AF: 2
AF
in reply to: abramdemski’s comment on: Exploiting EDT
True. This looks to me like an effect of EDT not being stable under self-modification, although here the issue is handicapping itself through external means rather than self-modification—like, if you offer a CDT agent a potion that will make it unable to lift more than one box before it enters Newcomb’s problem (i.e., before Omega makes its observation of the agent), then it’ll cheerfully take it and pay you for the privilege.

Benya_Fallenstein 11 Nov 2014 1:46 UTC
1 point
AF
on: A primer on provability logic
Thread for proofs of results claimed above (not limited to stuff not found in Lindström); contributions appreciated. Stuff not in Lindström includes the uniqueness of arithmetic fixed points in PA (found in the modal agents paper), and I think the version of the fixed point theorem with more than one $F_{i}$ (the latter should be provable by iterated application of the fixed point theorem for a single $F$ ).