4 ms·

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

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 cannot achieve this by simulating itself. A formal system cannot in general prove that it is reliable, i.e. that if it proves statement P then P is true. http://intelligence.org/files/lob-notes-IAFF.pdf http://intelligence.org/files/lob-notes-IAFF.pdf But with this article, the hope is that a formal system can show that the statement about itself is probably true.

bonoboTP 10y ago
But can it show that it's actually running this correct algorithm to determine whether the statement about itself is probably true? There is always an external context that runs the computation. A computation never exists in "abstract space", it always happens on a physical level. Any computation is only good if it runs in the context that it was designed for. What I mean is that the AI can never "know" if it's still following the "righteous goals", because a new environment may have grown around it, that "transforms" its inputs and outputs so that to the core machine it seems like nothing has changed, but actually its real-world effects have become very different. And at this point you could actually also say that this part of the environment has grown onto the AI machine and it now effectively has new goals that are incompatible with the ones designed into the core part of the machine. My point is, there is no isolated system, reasoning by itself in an isolated fashion. Subject and environment are not clearly divided.
- posterboy 10y ago
  > a new environment may have grown around it > at this point you could actually also say that this part of the environment has grown onto the AI machine No, you cannot, if the environment is part of the definition of the machine, as you put it, A computation never exists in "abstract space", because if the environment changed, you'd have a new machine and all bets are off. You had that right at first. Of course, that definition is unwieldy and we define interfaces as abstract and general as possible, to separate concerns. With involved machinery, that separation is not that clear cut, as their always two sides of the coin, to put it trivially.
- tbt 10y ago
  This is a good point. I think it'd be pretty interesting and useful to get a better grasp on when/whether/how a system can reason about itself as embedded in the world in a sane way.
posterboy 10y ago
> 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 article, the hope is that a formal system can show that the statement about itself is probably true. Probabilty is not good enough. The Bayesian Conspiracy sure is strong, but I'd prefer to stay with first order logic and finite state machines that are provably correct. > > The short answer is that this theorem illustrates the basic kind of self-reference involved when an algorithm considers its own output as part of the universe Isn't that what differential equations are for? I'm tired of the liars paradoxon. Intuitively, I've settled on the presumption that paradoxa always rest on wrong assumptions. I'm no mathematician, but I refuse the notion that I am inherently unable to be certain. That's why algorithms are by my preferred definition bound to be deterministic. I'd like to be able to tie this in with the Chomsky Hierarchy, albeit I am not that advanced. I'm no mathematician and I'm impressed by quines. I guess, the halting problem implies that quines cannot always be predicted. Heuristics help there and that's what stochastic is all about. Let me be clear. The paradoxon "this sentence is a lie" is neither a sentence, nor a lie. That's a question of definition. 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. The higher order logic and self reference is related to recursively enumerable grammars low in the Chomsky Hierarchy. Though, if ordered by magnitude, I'd call it higher. I hope, if the goal is natural language, we don't need to aim that high. If you want a computer that computes computers, though, go for it. > A formal system cannot achieve this by simulating itself. The type of self similarity used in quines or the liars paradox seems to play an important role in what we perceive as intelligent. Although, I stipulate, the intelligence involved is the ability to tell the difference between a misleading liars paradox and constructively provable quines. Of course, a machine that doesn't need verification from the supervising developer would be akin to a perpetuum mobile. It is easy to supervise the AGI's output by the less intelligent machines that have to do the output. The focus is on optimizing the processes, not the inability to assert safety guidelines. Edit: mixed up the order of the Chomsky Hierarchy.
fmap 10y ago
> 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 carried out in a stronger system. There is a standard way around this, which has existed for a long time. You stratify the system by introducing universes. E.g. in type theory, a universe is a type of (codes for) small types. This allows you to state and show meta theorems "for all (small) types", by quantifying over a universe. In the concrete example of Martin-Loef type theory (MLTT) you can show that MLTT with n+1 universes contains a model of MLTT with n universes. On the other hand, adding more universes seems to be harmless as far as anyone knows. Under the assumption that MLTT with a countably infinite number of universes is consistent and you restrict your formal system to only use a bounded number of universes, it is still possible to show that it is "reliable". It is "at least as reliable" as MLTT with countably many universes. I will read the article later and update this post if there is something compelling in the paper. At the moment I'm just confused what the problem is, and would really appreciate it if you could expand on this.
- jpt4 10y ago
  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 axioms for a more powerful universe?
  - fmap 10y ago
    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.
chadlavi 10y ago
"fear not humans, I am probably going to comply with Asimov's first law"

bonoboTP 10y ago

But can it show that it's actually running this correct algorithm to determine whether the statement about itself is probably true? There is always an external context that runs the computation. A computation never exists in "abstract space", it always happens on a physical level. Any computation is only good if it runs in the context that it was designed for. What I mean is that the AI can never "know" if it's still following the "righteous goals", because a new environment may have grown around it, that "transforms" its inputs and outputs so that to the core machine it seems like nothing has changed, but actually its real-world effects have become very different. And at this point you could actually also say that this part of the environment has grown onto the AI machine and it now effectively has new goals that are incompatible with the ones designed into the core part of the machine. My point is, there is no isolated system, reasoning by itself in an isolated fashion. Subject and environment are not clearly divided.

posterboy 10y ago
> a new environment may have grown around it > at this point you could actually also say that this part of the environment has grown onto the AI machine No, you cannot, if the environment is part of the definition of the machine, as you put it, A computation never exists in "abstract space", because if the environment changed, you'd have a new machine and all bets are off. You had that right at first. Of course, that definition is unwieldy and we define interfaces as abstract and general as possible, to separate concerns. With involved machinery, that separation is not that clear cut, as their always two sides of the coin, to put it trivially.
tbt 10y ago
This is a good point. I think it'd be pretty interesting and useful to get a better grasp on when/whether/how a system can reason about itself as embedded in the world in a sane way.

posterboy 10y ago

> 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 article, the hope is that a formal system can show that the statement about itself is probably true. Probabilty is not good enough. The Bayesian Conspiracy sure is strong, but I'd prefer to stay with first order logic and finite state machines that are provably correct. > > The short answer is that this theorem illustrates the basic kind of self-reference involved when an algorithm considers its own output as part of the universe Isn't that what differential equations are for? I'm tired of the liars paradoxon. Intuitively, I've settled on the presumption that paradoxa always rest on wrong assumptions. I'm no mathematician, but I refuse the notion that I am inherently unable to be certain. That's why algorithms are by my preferred definition bound to be deterministic. I'd like to be able to tie this in with the Chomsky Hierarchy, albeit I am not that advanced. I'm no mathematician and I'm impressed by quines. I guess, the halting problem implies that quines cannot always be predicted. Heuristics help there and that's what stochastic is all about. Let me be clear. The paradoxon "this sentence is a lie" is neither a sentence, nor a lie. That's a question of definition. 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. The higher order logic and self reference is related to recursively enumerable grammars low in the Chomsky Hierarchy. Though, if ordered by magnitude, I'd call it higher. I hope, if the goal is natural language, we don't need to aim that high. If you want a computer that computes computers, though, go for it. > A formal system cannot achieve this by simulating itself. The type of self similarity used in quines or the liars paradox seems to play an important role in what we perceive as intelligent. Although, I stipulate, the intelligence involved is the ability to tell the difference between a misleading liars paradox and constructively provable quines. Of course, a machine that doesn't need verification from the supervising developer would be akin to a perpetuum mobile. It is easy to supervise the AGI's output by the less intelligent machines that have to do the output. The focus is on optimizing the processes, not the inability to assert safety guidelines. Edit: mixed up the order of the Chomsky Hierarchy.

fmap 10y ago

> 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 carried out in a stronger system. There is a standard way around this, which has existed for a long time. You stratify the system by introducing universes. E.g. in type theory, a universe is a type of (codes for) small types. This allows you to state and show meta theorems "for all (small) types", by quantifying over a universe. In the concrete example of Martin-Loef type theory (MLTT) you can show that MLTT with n+1 universes contains a model of MLTT with n universes. On the other hand, adding more universes seems to be harmless as far as anyone knows. Under the assumption that MLTT with a countably infinite number of universes is consistent and you restrict your formal system to only use a bounded number of universes, it is still possible to show that it is "reliable". It is "at least as reliable" as MLTT with countably many universes. I will read the article later and update this post if there is something compelling in the paper. At the moment I'm just confused what the problem is, and would really appreciate it if you could expand on this.

jpt4 10y ago
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 axioms for a more powerful universe?
- fmap 10y ago
  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.

chadlavi 10y ago

"fear not humans, I am probably going to comply with Asimov's first law"