5 ms·

Intelligence as a Halting Oracle

21 points by yters 8y ago

yters 8y ago
For those interested in the mathematical proof: https://news.ycombinator.com/item?id=18377525 https://news.ycombinator.com/item?id=18377525
- LolWolf 8y ago
  Interesting cycle you've constructed, there.
- yters 8y ago
  Here's the direct link to the proof: https://www.am-nat.org/site/law-of-information-non-growth/ https://www.am-nat.org/site/law-of-information-non-growth/
ScottBurson 8y ago
Right. The interesting thing to me about this is its application to proving theorems, especially about programs. Historically, most people interested in having machines prove theorems have looked for algorithms — "proof procedures", the mathematicians call them, and of course they like to prove theorems about these procedures, such as that they're sound (never generate an incorrect proof) and complete (can prove any true theorem). Both of these sound like desirable properties, and for restricted domains such as first-order logic, it's possible to have both; but first-order logic is inadequate for reasoning about programs. For this task, we need higher-order logic, to prove invariants by induction, and Turing's proof arguably shows that there can be no sound and complete proof procedure for higher-order logic. We have to give up something, and of course that something is completeness; we can't part with soundness, because incorrect proofs are not useful. So we have to accept incompleteness, but obviously we want our program-property prover to be able to prove as much as possible. How do we approach that? I don't think we can make much progress approaching it mathematically; I think we have to approach it as an AI problem. That means figuring out how humans manage to be "partial oracles" and doing the same thing as much as we can. It means heuristics, it means pattern matching, it means machine learning.
- lisper 8y ago
  Or it means constraining your domain and only accepting those programs about which the properties you care about can be proved. Or it means accepting the risk that your system might break.
  - ScottBurson 8y ago
    Or it means accepting that your prover will need occasional hints from a human expert. I think this will always be true, when we're doing software verification. Another way to look at the problem, then, is: how do we reduce the need for manual intervention to a minimum?
- yters 8y ago
  This is a great idea. I'm working on this sort of thing using active learning.
lisper 8y ago
I find this argument very unconvincing. The reason code has bugs is precisely because humans are NOT good halting oracles. We're not even good self-assessors of our own oracular capabilities because we not only write buggy code, but we're often surprised by the bugs in the code we write.
- yters 8y ago
  That would indicate humans are partial halting oracles.
  - lisper 8y ago
    No. A partial oracle never gives a wrong answer, it's just allowed to say "I don't know."
    - yters 8y ago
      All a partial oracle has to do is be able to correctly answer an undecidable set of problems and then it can no longer be replicated by a Turing machine. It can be wrong on an infinite number of problems and still fit this requirement.
      - dragonwriter 8y ago
        No, a partial oracle by definition gives correct results for some subset of questions in the domain of interest, and no answer for other questions in the domain. It never gives wrong answers. (Now, if you can define the scope of questions for which a procedure gives wrong answers such that you can identify them in advance, you can convert it to a partial or full oracle by applying a process around the base procedure that flips the answer for those question (for a binary domain, like halting) or converts them to “don't know” (for non-binary domains.)
        yters 8y ago
        Well, if it's a definition thing, we can define a "splurg" which can give correct answers for an undecidable subset, and arbitrary answers, some wrong some right, for everything else. A "splurg" cannot be a TM, but it is also not a complete oracle.
dooglius 8y ago
This appears to be crank garbage, which is unfortunately not hard to run into when reading online about computability and related topics. Anything not computable by a Turing Machine is almost certainly not physically realizable (Church-Turing thesis), and if it were it would surely involve esoteric physics like black holes, not anything readily available to human brains.
- chowells 8y ago
  I wonder if the author realizes Turing machines can be partial halting oracles. SAT/SMT solvers do that job pretty well over most of the same problem space as humans. And any technique humans invent can be added to a solver to use as well.
  - dooglius 8y ago
    Well, the definition given specifically says stronger than Turing Machines, what you're describing is more what I hoped the article would be about, making certain theoretical oracle machine algorithms partially realizable by putting a human in the loop, to e.g. come up with lower bounds on Chaitin's constant.
    - yters 8y ago
      This is what I'm working on, a human in the loop approach to Solomonoff induction.
- dragonwriter 8y ago
  > and if it were it would surely involve esoteric physics like black holes, not anything readily available to human brains. To be fair, until we know in detail how brains work, we can't eliminate the possibility that esoteric physics are key to the their operation; we only rule that out with an adequate model that does not invoke such physics.
  - ummonk 8y ago
    We know the physics of how brains work (i.e. the physics of neurons). So yes, we can rule out any such exotic physics.
empath75 8y ago
> If we only have a partial halting oracle, we still get a speed up by eliminating the non-halting programs that can be identified by our partial oracle. This is wrong on so many levels that the entire rest of the essay becomes nonsense.
- tree_of_item 8y ago
  Why is it wrong? If the oracle can only identify a certain class of nonterminating programs, you still get a speed up by doing so.
  - empath75 8y ago
    If you told me you wanted to count through all the natural numbers but we’re going to skip the evens, how much time would you save.
    - yters 8y ago
      In the article's scenario there are a finite number of Turing machines to check in order to find one that matches the specification. So, eliminating some of them will lead to a speed up.
- yters 8y ago
  You may want to check out the proof for further information. https://news.ycombinator.com/item?id=18377525 https://news.ycombinator.com/item?id=18377525
  - yters 8y ago
    Direct link: https://www.am-nat.org/site/law-of-information-non-growth/ https://www.am-nat.org/site/law-of-information-non-growth/
eigenspace 8y ago
As most readers have surmised, this is indeed a fallacious grasp for some reason to think the human beings are metaphysically special. See also yters' post https://mindmatters.today/2018/09/meaningful-information-vs-artificial-intelligence/ https://mindmatters.today/2018/09/meaningful-information-vs-... The argument presented relies on the idea that humans can create 'mutual information' about the world which has been shown to be impossible. However, the relies on assuming that we actually create mutual information. Instead, consider the fact that Bayesian processes with enough observations can approximate mutual information arbitrarily well. Now it seems that Yters' entire argument falls apart because the most reasonable explaination for how the human brain operates come down to Bayesian processes. Does it sound more reasonable to you that the human brain is a magical 'partial halting oracle' violating the very laws of physics, or that the human brain uses Bayesian reasoning to build up predictions about the world which are only well founded statistically?
- yters 8y ago
  This accompanying proof I put together shows halting oracles can create mutual information: https://www.am-nat.org/site/law-of-information-non-growth/ https://www.am-nat.org/site/law-of-information-non-growth/ So if humans are partial halting oracles, then they can create mutual information. The HN discussion page: https://news.ycombinator.com/item?id=18377525 https://news.ycombinator.com/item?id=18377525
  - eigenspace 8y ago
    Yes but the whole point is that nobody believes that humans are partial halting oracles, and there is a simpler, more believable explanation that doesn’t require that claim. I have a hard time seeing your argument as anything other than 'motivated reasoning' attempting to justify to your religious/metaphysical beliefs.
    - yters 8y ago
      I'd be interested in this alternate claim. You mentioned something about Bayesian updates. Ironically, I see this the other way around. I think people are having a hard time accepting the possibility that humans are partial halting oracles because of their bias against anything that seems religious, even if it makes more sense.

21 points by yters 8y ago

For those interested in the mathematical proof: https://news.ycombinator.com/item?id=18377525 https://news.ycombinator.com/item?id=18377525

LolWolf 8y ago
Interesting cycle you've constructed, there.
yters 8y ago
Here's the direct link to the proof: https://www.am-nat.org/site/law-of-information-non-growth/ https://www.am-nat.org/site/law-of-information-non-growth/

ScottBurson 8y ago

Right. The interesting thing to me about this is its application to proving theorems, especially about programs. Historically, most people interested in having machines prove theorems have looked for algorithms — "proof procedures", the mathematicians call them, and of course they like to prove theorems about these procedures, such as that they're sound (never generate an incorrect proof) and complete (can prove any true theorem). Both of these sound like desirable properties, and for restricted domains such as first-order logic, it's possible to have both; but first-order logic is inadequate for reasoning about programs. For this task, we need higher-order logic, to prove invariants by induction, and Turing's proof arguably shows that there can be no sound and complete proof procedure for higher-order logic. We have to give up something, and of course that something is completeness; we can't part with soundness, because incorrect proofs are not useful. So we have to accept incompleteness, but obviously we want our program-property prover to be able to prove as much as possible. How do we approach that? I don't think we can make much progress approaching it mathematically; I think we have to approach it as an AI problem. That means figuring out how humans manage to be "partial oracles" and doing the same thing as much as we can. It means heuristics, it means pattern matching, it means machine learning.

lisper 8y ago
Or it means constraining your domain and only accepting those programs about which the properties you care about can be proved. Or it means accepting the risk that your system might break.
- ScottBurson 8y ago
  Or it means accepting that your prover will need occasional hints from a human expert. I think this will always be true, when we're doing software verification. Another way to look at the problem, then, is: how do we reduce the need for manual intervention to a minimum?
yters 8y ago
This is a great idea. I'm working on this sort of thing using active learning.

lisper 8y ago

I find this argument very unconvincing. The reason code has bugs is precisely because humans are NOT good halting oracles. We're not even good self-assessors of our own oracular capabilities because we not only write buggy code, but we're often surprised by the bugs in the code we write.

yters 8y ago
That would indicate humans are partial halting oracles.
- lisper 8y ago
  No. A partial oracle never gives a wrong answer, it's just allowed to say "I don't know."
  - yters 8y ago
    All a partial oracle has to do is be able to correctly answer an undecidable set of problems and then it can no longer be replicated by a Turing machine. It can be wrong on an infinite number of problems and still fit this requirement.
    - dragonwriter 8y ago
      No, a partial oracle by definition gives correct results for some subset of questions in the domain of interest, and no answer for other questions in the domain. It never gives wrong answers. (Now, if you can define the scope of questions for which a procedure gives wrong answers such that you can identify them in advance, you can convert it to a partial or full oracle by applying a process around the base procedure that flips the answer for those question (for a binary domain, like halting) or converts them to “don't know” (for non-binary domains.)
      - yters 8y ago
        Well, if it's a definition thing, we can define a "splurg" which can give correct answers for an undecidable subset, and arbitrary answers, some wrong some right, for everything else. A "splurg" cannot be a TM, but it is also not a complete oracle.

dooglius 8y ago

This appears to be crank garbage, which is unfortunately not hard to run into when reading online about computability and related topics. Anything not computable by a Turing Machine is almost certainly not physically realizable (Church-Turing thesis), and if it were it would surely involve esoteric physics like black holes, not anything readily available to human brains.

chowells 8y ago
I wonder if the author realizes Turing machines can be partial halting oracles. SAT/SMT solvers do that job pretty well over most of the same problem space as humans. And any technique humans invent can be added to a solver to use as well.
- dooglius 8y ago
  Well, the definition given specifically says stronger than Turing Machines, what you're describing is more what I hoped the article would be about, making certain theoretical oracle machine algorithms partially realizable by putting a human in the loop, to e.g. come up with lower bounds on Chaitin's constant.
  - yters 8y ago
    This is what I'm working on, a human in the loop approach to Solomonoff induction.
dragonwriter 8y ago
> and if it were it would surely involve esoteric physics like black holes, not anything readily available to human brains. To be fair, until we know in detail how brains work, we can't eliminate the possibility that esoteric physics are key to the their operation; we only rule that out with an adequate model that does not invoke such physics.
- ummonk 8y ago
  We know the physics of how brains work (i.e. the physics of neurons). So yes, we can rule out any such exotic physics.

empath75 8y ago

> If we only have a partial halting oracle, we still get a speed up by eliminating the non-halting programs that can be identified by our partial oracle. This is wrong on so many levels that the entire rest of the essay becomes nonsense.

tree_of_item 8y ago
Why is it wrong? If the oracle can only identify a certain class of nonterminating programs, you still get a speed up by doing so.
- empath75 8y ago
  If you told me you wanted to count through all the natural numbers but we’re going to skip the evens, how much time would you save.
  - yters 8y ago
    In the article's scenario there are a finite number of Turing machines to check in order to find one that matches the specification. So, eliminating some of them will lead to a speed up.
yters 8y ago
You may want to check out the proof for further information. https://news.ycombinator.com/item?id=18377525 https://news.ycombinator.com/item?id=18377525
- yters 8y ago
  Direct link: https://www.am-nat.org/site/law-of-information-non-growth/ https://www.am-nat.org/site/law-of-information-non-growth/

eigenspace 8y ago

As most readers have surmised, this is indeed a fallacious grasp for some reason to think the human beings are metaphysically special. See also yters' post https://mindmatters.today/2018/09/meaningful-information-vs-artificial-intelligence/ https://mindmatters.today/2018/09/meaningful-information-vs-... The argument presented relies on the idea that humans can create 'mutual information' about the world which has been shown to be impossible. However, the relies on assuming that we actually create mutual information. Instead, consider the fact that Bayesian processes with enough observations can approximate mutual information arbitrarily well. Now it seems that Yters' entire argument falls apart because the most reasonable explaination for how the human brain operates come down to Bayesian processes. Does it sound more reasonable to you that the human brain is a magical 'partial halting oracle' violating the very laws of physics, or that the human brain uses Bayesian reasoning to build up predictions about the world which are only well founded statistically?

yters 8y ago
This accompanying proof I put together shows halting oracles can create mutual information: https://www.am-nat.org/site/law-of-information-non-growth/ https://www.am-nat.org/site/law-of-information-non-growth/ So if humans are partial halting oracles, then they can create mutual information. The HN discussion page: https://news.ycombinator.com/item?id=18377525 https://news.ycombinator.com/item?id=18377525
- eigenspace 8y ago
  Yes but the whole point is that nobody believes that humans are partial halting oracles, and there is a simpler, more believable explanation that doesn’t require that claim. I have a hard time seeing your argument as anything other than 'motivated reasoning' attempting to justify to your religious/metaphysical beliefs.
  - yters 8y ago
    I'd be interested in this alternate claim. You mentioned something about Bayesian updates. Ironically, I see this the other way around. I think people are having a hard time accepting the possibility that humans are partial halting oracles because of their bias against anything that seems religious, even if it makes more sense.