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

51–60 of 66 posts

Re: Logical Induction

#51

Post by gallabytes »

jpt4 wrote: post #48
jey wrote: post #39

Earlier quoted context omitted.

What is your definition of practical?

MIRI is entirely Blue Team - they work to create theoretical [0] safeguards on AI agents yet to be developed. I've long envisioned a counterpart Red Team that does nothing but build AIs that attempt to subvert these safety features, since the rest of the world of non Friendly AI [1] research is only unco-ordinated para-red behavior. [0] In the sense of "valid under these known precepts", not "speculative". [1] Non "F…

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.

Re: Logical Induction

#52

Post by joshcohen »

tbt wrote: post #42
joshcohen wrote: post #31

Earlier quoted context omitted.

I'm not an author but this property with respect to a universal 'semimeasure' holds in the limit as time goes to infinity, as do most stated properties of logical inductors. The fact that they're computable is academic.

This is right, but perhaps misleading; most of the properties are "asymptotic", meaning that they may take an extremely long time to hold, but they hold at finite times. For example, "provability induction" says that if you have a (polytime computable) sequence of sentences phi_n, all of which happen to be provable (possibly with fast-growing proof lengths), then P_n(phi_n) limits to 1. This means that on day n the l…

Although P_n can't be computed in anything like n steps.

Re: Logical Induction

#53

Post by chriswarbo »

tbt wrote: post #42
joshcohen wrote: post #31

Earlier quoted context omitted.

I'm not an author but this property with respect to a universal 'semimeasure' holds in the limit as time goes to infinity, as do most stated properties of logical inductors. The fact that they're computable is academic.

This is right, but perhaps misleading; most of the properties are "asymptotic", meaning that they may take an extremely long time to hold, but they hold at finite times. For example, "provability induction" says that if you have a (polytime computable) sequence of sentences phi_n, all of which happen to be provable (possibly with fast-growing proof lengths), then P_n(phi_n) limits to 1. This means that on day n the l…

The key is that the generator of such sequences has limited resources; once the inductor has learned the (implicit or explicit) program generating these sentences (perhaps by simulation, as in Solomonoff induction), it can apply that reasoning to the individual sentences; e.g. if it believes it's verified the correctness of the generator, that is enough justification to believe the sentences being produced.

Re: Logical Induction

#54

Post by tbt »

joshcohen wrote: post #52
tbt wrote: post #42

Earlier quoted context omitted.

This is right, but perhaps misleading; most of the properties are "asymptotic", meaning that they may take an extremely long time to hold, but they hold at finite times. For example, "provability induction" says that if you have a (polytime computable) sequence of sentences phi_n, all of which happen to be provable (possibly with fast-growing proof lengths), then P_n(phi_n) limits to 1. This means that on day n the l…

Although P_n can't be computed in anything like n steps.

Yeah. It's still surprising to me, though; P_n can predict extremely long-running computations, even ones with a much longer runtime than P_n, at least as well as any quickly computable "pattern". (The algorithm in the paper uses a (roughly) double-exponential-time algorithm to predict arbitrarily long-running programs, in a way that can't be improved upon by any polytime computable method.)

Re: Logical Induction

#55

Post by tbt »

chriswarbo wrote: post #53
tbt wrote: post #42

Earlier quoted context omitted.

This is right, but perhaps misleading; most of the properties are "asymptotic", meaning that they may take an extremely long time to hold, but they hold at finite times. For example, "provability induction" says that if you have a (polytime computable) sequence of sentences phi_n, all of which happen to be provable (possibly with fast-growing proof lengths), then P_n(phi_n) limits to 1. This means that on day n the l…

The key is that the generator of such sequences has limited resources; once the inductor has learned the (implicit or explicit) program generating these sentences (perhaps by simulation, as in Solomonoff induction), it can apply that reasoning to the individual sentences; e.g. if it believes it's verified the correctness of the generator, that is enough justification to believe the sentences being produced.

Yep, that's the idea :)

This is in the vein of "prediction using ensembles of experts" methods such as SI, with a twist that the experts are traders, not forecasters; they don't have to have opinions on everything the logical inductor has to predict, the traders just have to point out particular ways that the logical inductor is being silly (and then the logical inductor corrects those problems).

Re: Logical Induction

#56

Post by posterboy »

posterboy wrote: post #21
josh_fyi wrote: post #13

The article is basic mathematical research and is not intended to be implemented, but rather to guide further applied research. The deeper motivation for this article is to allow future Artificial General Intelligences to prove facts about themselves; specifically, the fact that the AGI, or a next-gen that it developers, has the same (safe) utility function that the designers originally specified. A formal system can…

> 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…

Come to think of it, intelligence by a different definition, almost a homonym, is concerned with information. That fits with my demand for zeroth order logical values.

Re: Logical Induction

#57

Post by jpt4 »

gallabytes wrote: post #51
jpt4 wrote: post #48

Earlier quoted context omitted.

MIRI is entirely Blue Team - they work to create theoretical [0] safeguards on AI agents yet to be developed. I've long envisioned a counterpart Red Team that does nothing but build AIs that attempt to subvert these safety features, since the rest of the world of non Friendly AI [1] research is only unco-ordinated para-red behavior. [0] In the sense of "valid under these known precepts", not "speculative". [1] Non "F…

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

Re: Logical Induction

#58

Post by YomiK »

the8472 wrote: post #18
szemet wrote: post #7

Earlier quoted context omitted.

Its too late, we already risk fortunes (and even lives) trusting in similar methods ;): https://en.wikipedia.org/wiki/Primality_test#Probabilistic_t... (Primality is also a logical (analytic) truth and we are satisfied with probabilistic proofs - of course only because the risk is known and controllable.)

That's not quite correct, most prime proving algorithms are non-deterministic in their computation, but they don't necessarily produce false positives (like miller-rabin does), algorithms that only produce false negatives also exist (e.g. ECPP)

Could you elaborate on ECPP false negatives? A properly working ECPP should never give false negatives, e.g. return "prime" for a composite. Since ECPP can give a certificate unlike AKS or APR-CL, the caller could do a relatively quick check of the math.

Some proof methods:

- BPSW. Deterministic, completely correct for all 64-bit values. Purely a compositeness test above, though no counterexamples known. This matches the false-positive idea -- above 64-bit it returns one of "definitely composite" or "probably prime."

- BLS 1975 methods. Relies on partial factoring N-1 and/or N+1 so unless the input is a special form, only practical to ~100 digits. No false results if the partial factoring can be done, and even gives a certificate of primality.

- APR-CL. Deterministic. No false results. Fast and practical up to ~5000 digits (one can debate where the impractical size line is). No certificate.

- AKS. Deterministic. No certificate. No false results. Very slow, so not generally used.

- ECPP. Non-deterministic (randomness is used internally), but no false results. Generates a certificate. Primo is practical up to ~30k digits (depends on your hardware and patience, but 10k digits on modern computers is quite practical). Open source implementations aren't as efficient, but still 1k+ digits is very reasonable. It is possible an implementation might be unable to proceed for various reasons and could return "gave up - no primality decision made" in addition to the choices "definitely composite" or "definitely prime (certificate included)". That's really a limitation of the implementation or the caller's patience.

Re: Logical Induction

#59

Post by fmap »

jpt4 wrote: post #45
fmap wrote: post #37

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. I'm not entirely sure what you mean by this (I haven't read the article yet, and I'm already familiar with Loeb's theorem). It's true that you cannot show that, say, second order arithmetic is consistent in the same system. In fact, every soundness proof (for a sufficiently strong logic) will have to be c…

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 internal model of "the theory so far".

There are type theories with universe variables, which essentially allow you to add an arbitrary (but finite) number of additional universes. The rules for this are straightforward, even though a consistency proof is of course only possible relative to type theory or set theory with more universes...

In set theory, one typically adds an axiom scheme that states something like "There is a Grothendieck universe containing this set". Iterating this gives you a similar tower of universes.

There are a lot more constructions that go beyond this and the funny thing is that as far as anyone knows they are all consistent. For instance, type theories with induction-recursion allow you to generate internal universes closed under certain operations while staying in the same universe. So one universe with induction-recursion allows you to show MLTT with an arbitrary finite number of universes consistent.

Re: Logical Induction

#60

Post by fmap »

tbt wrote: post #50
fmap wrote: post #37

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. I'm not entirely sure what you mean by this (I haven't read the article yet, and I'm already familiar with Loeb's theorem). It's true that you cannot show that, say, second order arithmetic is consistent in the same system. In fact, every soundness proof (for a sufficiently strong logic) will have to be c…

> 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 proof of the Feit-Thompson theorem in Coq, with all the related theories, uses 4 universes. If you have a system certified in type theory, then you can still reason about it. Possibly one universe higher, but that is not a problem (as far as anybody knows).

Post reply on HN