Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Logical Induction

intelligence.org

Post reply on HN
Print view View original

61–66 of 66 posts

Re: Logical Induction

#61

Post by posterboy »

AlexMennen wrote: post #38
posterboy wrote: post #21

Earlier quoted context omitted.

> A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true This implies second order logic. It is not clear to me, whether the loss of consistency is warranted. Type Theories are tried to avoid inconsistence. However high the order of the processing logic is, its only reason to exist is to output first order theorems, those we can prove decidable. > But with this…

> This implies second order logic. No, it does not. The second incompleteness theorem is provable in first-order Peano Arithmetic. > Of course I'm in no position to say a similar thing about Goedels incompleteness theorem, and I even referred to it's result in higher order logics, but I still doubt the relevance, as many seem to be ignorant of his former completeness theorem. I have no idea what you're trying to say,…

Oh, the second one comes of wrong. I did mean the parent quote

> A formal system cannot in general prove that it is reliable

I hadn't noticed when I wrote that, formal system is an idiom - even more specific in this specific context. How confusing.

Re: Logical Induction

#62

Post by tbt »

fmap wrote: post #59
jpt4 wrote: post #45

Earlier quoted context omitted.

The expressiveness of the tower of universes limits to that of Peano arithmetic, correct? Otherwise, there would exist a universe k that contain theorems that could not be computably proven in universe k+1. On a separate matter, are there any principled meta-universal rules for incrementing the universe index? That is, if one suspects that one's current universe lacks proving power, is it possible to generate the axi…

Peano arithmetic, as in classical first-order logic with the peano axioms is a small subsystem of MLTT with natural numbers and no universes. If you come from a set theory background, then universes are really akin to Grothendieck universes, or large cardinal axioms. You start out with a powerful theory and then improve it by repeatedly adding statements of the form "and the theory so far is consistent", by giving an…

[ For some work formalizing a reflection principle in HOL, see https://intelligence.org/files/ProofProducingReflection.pdf ]

Re: Logical Induction

#63

Post by tbt »

fmap wrote: post #60
tbt wrote: post #50

Earlier quoted context omitted.

> This allows you to state and show meta theorems "for all (small) types", by quantifying over a universe. As you say, this isn't quite self-trust. Another natural move is to relax the criterion of self-trust away from "it proves itself consistent" (impossible by incompleteness) towards "it assigns high probability that it has good beliefs". (Formalizations of this are in the paper.) > At the moment I'm just confused…

So by now I've actually read the (abridged) paper and skimmed the full paper. And the paper has nothing to do with consistency problems, since they only consider boolean propositional logic... Assigning consistent probabilities in the limit is indeed a much more interesting problem anyway. Self-trust seems like a problem on paper, but the reality is that normal mathematics uses very few universes. Concretely, the pro…

>Self-trust seems like a problem on paper, but the reality is that normal mathematics uses very few universes.

Self-trust (broadly construed) is interesting to me because it seems relevant to designing goal-based agents that are "stable", in the sense that they trust that future versions of themselves will have accurate beliefs (and therefore don't have an incentive to mess around with their systems for forming beliefs). If we try to formalize this intuition with "beliefs" as theorems proven by a formal system, we run into reflection problems; having your theorem prover assert that it will keep outputting only true statements feels awfully close to asserting its own soundness. So even if your agent can perform all the usual mathematical reasoning it needs, it still can't do all the useful reasoning about itself (it would need another large cardinal... and then another...).

The self-trust property in the paper says that it's possible to "learn from experience" that your future self is probably going to have pretty good beliefs. Specifically, a logical inductor P_n learns (roughly speaking) that "if P_f(n) thinks Phi is likely, then Phi is likely", where f(n) can be a fast-growing computable function. That is, on day n, P_n believes a sort of "probabilistic soundness" condition for its future self P_f(n). This is weaker than full soundness in at least two ways, but it is fully "reflective" in the sense that P believes this of itself.

Re: Logical Induction

#64

Post by gallabytes »

jpt4 wrote: post #57
gallabytes wrote: post #51

Earlier quoted context omitted.

I find that perception fairly surprising, as for a very long time it felt like we did more red team than blue team. I do acknowledge that this has been changing recently, but only significantly in the context of building on the results in this paper.

Would you please direct me to an example of MIRI's Red Team efforts that isn't the recent "Malevolent AI" paper [0]? Adherence to the belief that UFAI is a threshold-grade existential risk seems to compel a "define first, delay implementation" strategy, lest any step forward be the irrevocable wrong one. [0] http://arxiv.org/abs/1605.02817

This makes me think the only thing we disagree on is the meaning of the words "red team" and "blue team" :)

When I say it feels like we spend a lot of time red teaming, that means I think we spend somewhere between 30 and 60% of research time trying to break things and see how they fail. This is fully compatible with not immediately implementing things - it's much less expensive to break something /before/ you build it.

Re: Logical Induction

#65

Post by Klaperman »

joshcohen wrote: post #22
ajkjk wrote: post #10

Earlier quoted context omitted.

This paper is a theoretical contribution, not a practical one, similar to Solomonoff Induction. Solomonoff Induction's contribution is essentially "there exists a formal mathematical process that inductive reasoning on evidence corresponds to" which, among other things, pretty much solves epistemological puzzles like the https://en.wikipedia.org/wiki/Raven_paradox from philosophy. Yeah, the actual performance of Solo…

Solomonoff induction is useful because without it there's no model of induction with infinite computational resources. "Logical induction" is not useful in the same way because without it we already have such a model: simply prove/disprove the propositions.

And what if the propositions we want to reason about are self-referencing or say something about the system itself in a Godelian way? You need probabilistic reasoning for that to actually work.

Also, "simply prove/disprove the propositions" requires infinite computational resources (we don't know how long the proofs will be or if there are any). Logical induction does not.

Re: Logical Induction

#66

Post by jpt4 »

gallabytes wrote: post #64
jpt4 wrote: post #57

Earlier quoted context omitted.

Would you please direct me to an example of MIRI's Red Team efforts that isn't the recent "Malevolent AI" paper [0]? Adherence to the belief that UFAI is a threshold-grade existential risk seems to compel a "define first, delay implementation" strategy, lest any step forward be the irrevocable wrong one. [0] http://arxiv.org/abs/1605.02817

This makes me think the only thing we disagree on is the meaning of the words "red team" and "blue team" :) When I say it feels like we spend a lot of time red teaming, that means I think we spend somewhere between 30 and 60% of research time trying to break things and see how they fail. This is fully compatible with not immediately implementing things - it's much less expensive to break something /before/ you build…

It is refreshing when only the maps, and not the objects, are under serious contention. I suspect I still might prefer walking a shade closer to the line dividing definitely intra and potentially extra boxed agents, but you are the ones actually in the arena - do keep up the interesting work.
Post reply on HN