6 ms·

As someone unfamiliar with the results you describe, why can’t a machine do better than a human? A smart human is better at writing proofs than a dumb one. If w

As someone unfamiliar with the results you describe, why can’t a machine do better than a human? A smart human is better at writing proofs than a dumb one. If we had a highly advanced general artificial intelligence, why couldn’t it generate better results than the smart humans?

westurner 6y ago
Or is automated proof search impossible for humans as well? Arguably, humans require more energy per operation. So, presumably such an argument hinges upon what types of operations are performed in conducting automated proof search?
- qayxc 6y ago
  What would "automated proof search" even mean in the context of being performed by a human being? The context here is that certain problems cannot be solved by an algorithm, which doesn't necessarily translate into "cannot be performed by a machine". It only means that there cannot be any Turing machine capable of solving them, no matter what "operations" it represents.
  - westurner 6y ago
    The task (in terms of constructor theory) is: Find the functions that sufficiently approximate the observations and record their reproducible derivations. Either the (unreferenced) study was actually arguing that "automated proof search" can't be done at all, or that human neural computation is categorically non-algorothmic. Grid search of all combinations of bits that correspond to [symbolic] classical or quantum models. Or better: evolutionary algorithms and/or neural nets.
    - qayxc 6y ago
      Roger Penrose argues that human neural computation is indeed non-algorithmic in nature (see his book "The Emperor's New Mind"; 1989) and speculates that quantum processes are involved. I don't quite understand the role of neural nets in that context, though. Those just classical computations in the end and should be bound by the same limits that every other algorithms are, shouldn't they?
      - westurner 6y ago
        That human cognition is quantum in nature - that e.g. entanglement is necessary - may be unfalsifiable. Neuromorphic engineering has expanded since the 1980s. https://en.wikipedia.org/wiki/Neuromorphic_engineering https://en.wikipedia.org/wiki/Neuromorphic_engineering Quantum computing is the best known method for simulating chemical reactions and thereby possibly also neurochemical reactions. But, Is quantum computing necessary to functionally emulate human cognition? It may be that a different computation medium can accomplish the same tasks without emulating all of the complexity of the brain. If the brain is only classical and some people are using their brains to perform quantum computations, there may be something there. Quantum cognition: https://en.wikipedia.org/wiki/Quantum_cognition https://en.wikipedia.org/wiki/Quantum_cognition
        westurner 6y ago
        Quantum memristors are still elusive. From "Quantum Memristors in Frequency-Entangled Optical Fields" (2020) https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7079656/ https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7079656/ : > Apart from the advantages of using these devices for computation [12] (such as energy efficiency [13], compared to transistor-based computers), memristors can be also used in machine learning schemes [14,15]. The relevance of the memristor lies in its ubiquitous presence in models which describe natural processes, especially those involving biological systems. For example, memristors inherently describe voltage-dependent ion-channel conductances in the axon membrane in neurons, present in the Hodgkin–Huxley model [16,17]. > Due to the inherent linearity of quantum mechanics, it is not straightforward to describe a dissipative non-linear memory element, such as the memristor, in the quantum realm, since nonlinearities usually lead to the violation of fundamental quantum principles, such as no-cloning theorem. Nonetheless, the challenge was already constructively addressed in Ref. [18]. This consists of a harmonic oscillator coupled to a dissipative environment, where the coupling is changed based on the results of a weak measurement scheme with classical feedback. As a result of the development of quantum platforms in recent years, and their improvement in controllability and scalability, different constructions of a quantum memristor in such platforms have been presented. There is a proposal for implementing it in superconducting circuits [7], exploiting memory effects that naturally arise in Josephson junctions. The second proposal is based on integrated photonics [19]: a Mach–Zehnder interferometer can behave as a beam splitter with a tunable reflectivity by introducing a phase in one of the beams, which can be manipulated to study the system as a quantum memristor subject to different quantum state inputs. Quantum harmonic oscillators have also found application in modeling financial markets. Quantum harmonic oscillator: https://en.wikipedia.org/wiki/Quantum_harmonic_oscillator https://en.wikipedia.org/wiki/Quantum_harmonic_oscillator
  - kd0amg 6y ago
    The idea that humans are physical systems with Turing-computable behavior would mean that any problem not solvable by Turing machines is also not solvable by humans. That is, there are programs whose halting behavior no human will ever determine, theorems of Peano arithmetic whose proof no human will ever find, etc., no matter how much humans work at it.
    - qayxc 6y ago
      > The idea that humans are physical systems with Turing-computable behavior would mean that any problem not solvable by Turing machines is also not solvable by humans. But there are real-world instances that contradict this hypothesis already. Humans don't exhibit Turing-computable behaviour because they did indeed solve problems that aren't solvable by Turing Machines. I can give a very concrete example as well. Consider the following program (in Python for simplicity's sake): def nat(x): yield x yield from nat(x+1) for a in nat(2): for b in nat(2): for c in nat(2): if a*a*a + b*b*b == c*c*c: print(f"{a}^3 * {b}^3 = {c}^3") exit() There is no Turing Machine capable of proving that this program won't halt (technically it will, due to practical limitations). Yet it has has been proven centuries ago that the above program won't halt. The mathematicians couldn't have used a Turing Machine-compliant computation, so something else must be involved. Now this of course doesn't mean that humans are generally capable of solving every problem that's not solvable by an algorithm, but it means that they can solve problems that algorithms can't solve.
      - kd0amg 6y ago
        > There is no Turing Machine capable of proving that this program won't halt Yes, there is. There's a machine which does nothing but print that exact proof. You seem to have conflated solving an instance of a problem with solving the entire problem. Turing's theorem states that no one Turing machine will get the answer right for every instance of the halting problem, but for any instance that one specific machine gets wrong, there's another machine that also gets that instance right (in addition to everything else the original machine gets right).
ShinTakuya 6y ago
I don't know what result they were referring to, but I've often heard it said that AI of current types so never be capable of the same types of cognition that we can do. That's not to say we can't create a different type of AI, but at the moment that's just science fiction and will need some major advances in technology.
qayxc 6y ago
It has been shown numerous times that there are limits to automated proof generation. One such result was that certain problems are undecidable, which means that any automated approach would be prone to become "stuck" and never terminate. Another results showed that the complexity of general automated proof generation is exponential in nature. Both these results mean, that it's impossible to tell whether a computation just takes a very long time (say years) or whether the problem is indeed undecidable (in which case the program would never halt.) A human on the hand, is very well capable of solving the Halting Problem and can discern whether a problem is undecidable [1]. This is of course a corner case, but it goes to show that there are indeed limits to automated theorem proving. A human would therefore - in principle - always need to proof that a problem is decidable in the first place before passing it to an ATP. [1] https://en.wikipedia.org/wiki/List_of_undecidable_problems https://en.wikipedia.org/wiki/List_of_undecidable_problems
- sudosysgen 6y ago
  Humans are not able to solve the halting problem. The halting problem isn't a question of if you can decide that some programs will not halt, but that you can decide if all programs would halt. Which humans can not do.
  - qayxc 6y ago
    No - that's simply not true. The Halting Problem states that there is no Turing Machine (i.e. program) capable of deciding whether a given program will halt. And yes, humans are very well capable of solving that, because humans can in fact proof whether any program halts. This doesn't mean every human can or that it has been done for every program, but it means that humans are - in general - able capable of deciding this, while algorithms (programs) can't.
    - tsimionescu 6y ago
      The Church-Turing thesis claims (and is believed to be right) that a Turing machine can solve (compute) any problem that can be solved (is computable). For now at least, we don't know of any counter-example to the Church-Turing thesis. Humans are certainly not able to tell whether a program in general will halt for any input it recieves. If you believe otherwise, please tell me whether the following program halts: Foo(): if P = NP: return true else: Foo()

westurner 6y ago

Or is automated proof search impossible for humans as well? Arguably, humans require more energy per operation. So, presumably such an argument hinges upon what types of operations are performed in conducting automated proof search?

qayxc 6y ago
What would "automated proof search" even mean in the context of being performed by a human being? The context here is that certain problems cannot be solved by an algorithm, which doesn't necessarily translate into "cannot be performed by a machine". It only means that there cannot be any Turing machine capable of solving them, no matter what "operations" it represents.
- westurner 6y ago
  The task (in terms of constructor theory) is: Find the functions that sufficiently approximate the observations and record their reproducible derivations. Either the (unreferenced) study was actually arguing that "automated proof search" can't be done at all, or that human neural computation is categorically non-algorothmic. Grid search of all combinations of bits that correspond to [symbolic] classical or quantum models. Or better: evolutionary algorithms and/or neural nets.
  - qayxc 6y ago
    Roger Penrose argues that human neural computation is indeed non-algorithmic in nature (see his book "The Emperor's New Mind"; 1989) and speculates that quantum processes are involved. I don't quite understand the role of neural nets in that context, though. Those just classical computations in the end and should be bound by the same limits that every other algorithms are, shouldn't they?
    - westurner 6y ago
      That human cognition is quantum in nature - that e.g. entanglement is necessary - may be unfalsifiable. Neuromorphic engineering has expanded since the 1980s. https://en.wikipedia.org/wiki/Neuromorphic_engineering https://en.wikipedia.org/wiki/Neuromorphic_engineering Quantum computing is the best known method for simulating chemical reactions and thereby possibly also neurochemical reactions. But, Is quantum computing necessary to functionally emulate human cognition? It may be that a different computation medium can accomplish the same tasks without emulating all of the complexity of the brain. If the brain is only classical and some people are using their brains to perform quantum computations, there may be something there. Quantum cognition: https://en.wikipedia.org/wiki/Quantum_cognition https://en.wikipedia.org/wiki/Quantum_cognition
      - westurner 6y ago
        Quantum memristors are still elusive. From "Quantum Memristors in Frequency-Entangled Optical Fields" (2020) https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7079656/ https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7079656/ : > Apart from the advantages of using these devices for computation [12] (such as energy efficiency [13], compared to transistor-based computers), memristors can be also used in machine learning schemes [14,15]. The relevance of the memristor lies in its ubiquitous presence in models which describe natural processes, especially those involving biological systems. For example, memristors inherently describe voltage-dependent ion-channel conductances in the axon membrane in neurons, present in the Hodgkin–Huxley model [16,17]. > Due to the inherent linearity of quantum mechanics, it is not straightforward to describe a dissipative non-linear memory element, such as the memristor, in the quantum realm, since nonlinearities usually lead to the violation of fundamental quantum principles, such as no-cloning theorem. Nonetheless, the challenge was already constructively addressed in Ref. [18]. This consists of a harmonic oscillator coupled to a dissipative environment, where the coupling is changed based on the results of a weak measurement scheme with classical feedback. As a result of the development of quantum platforms in recent years, and their improvement in controllability and scalability, different constructions of a quantum memristor in such platforms have been presented. There is a proposal for implementing it in superconducting circuits [7], exploiting memory effects that naturally arise in Josephson junctions. The second proposal is based on integrated photonics [19]: a Mach–Zehnder interferometer can behave as a beam splitter with a tunable reflectivity by introducing a phase in one of the beams, which can be manipulated to study the system as a quantum memristor subject to different quantum state inputs. Quantum harmonic oscillators have also found application in modeling financial markets. Quantum harmonic oscillator: https://en.wikipedia.org/wiki/Quantum_harmonic_oscillator https://en.wikipedia.org/wiki/Quantum_harmonic_oscillator
- kd0amg 6y ago
  The idea that humans are physical systems with Turing-computable behavior would mean that any problem not solvable by Turing machines is also not solvable by humans. That is, there are programs whose halting behavior no human will ever determine, theorems of Peano arithmetic whose proof no human will ever find, etc., no matter how much humans work at it.
  - qayxc 6y ago
    > The idea that humans are physical systems with Turing-computable behavior would mean that any problem not solvable by Turing machines is also not solvable by humans. But there are real-world instances that contradict this hypothesis already. Humans don't exhibit Turing-computable behaviour because they did indeed solve problems that aren't solvable by Turing Machines. I can give a very concrete example as well. Consider the following program (in Python for simplicity's sake): def nat(x): yield x yield from nat(x+1) for a in nat(2): for b in nat(2): for c in nat(2): if a*a*a + b*b*b == c*c*c: print(f"{a}^3 * {b}^3 = {c}^3") exit() There is no Turing Machine capable of proving that this program won't halt (technically it will, due to practical limitations). Yet it has has been proven centuries ago that the above program won't halt. The mathematicians couldn't have used a Turing Machine-compliant computation, so something else must be involved. Now this of course doesn't mean that humans are generally capable of solving every problem that's not solvable by an algorithm, but it means that they can solve problems that algorithms can't solve.
    - kd0amg 6y ago
      > There is no Turing Machine capable of proving that this program won't halt Yes, there is. There's a machine which does nothing but print that exact proof. You seem to have conflated solving an instance of a problem with solving the entire problem. Turing's theorem states that no one Turing machine will get the answer right for every instance of the halting problem, but for any instance that one specific machine gets wrong, there's another machine that also gets that instance right (in addition to everything else the original machine gets right).

ShinTakuya 6y ago

I don't know what result they were referring to, but I've often heard it said that AI of current types so never be capable of the same types of cognition that we can do. That's not to say we can't create a different type of AI, but at the moment that's just science fiction and will need some major advances in technology.

qayxc 6y ago

It has been shown numerous times that there are limits to automated proof generation. One such result was that certain problems are undecidable, which means that any automated approach would be prone to become "stuck" and never terminate. Another results showed that the complexity of general automated proof generation is exponential in nature. Both these results mean, that it's impossible to tell whether a computation just takes a very long time (say years) or whether the problem is indeed undecidable (in which case the program would never halt.) A human on the hand, is very well capable of solving the Halting Problem and can discern whether a problem is undecidable [1]. This is of course a corner case, but it goes to show that there are indeed limits to automated theorem proving. A human would therefore - in principle - always need to proof that a problem is decidable in the first place before passing it to an ATP. [1] https://en.wikipedia.org/wiki/List_of_undecidable_problems https://en.wikipedia.org/wiki/List_of_undecidable_problems

sudosysgen 6y ago
Humans are not able to solve the halting problem. The halting problem isn't a question of if you can decide that some programs will not halt, but that you can decide if all programs would halt. Which humans can not do.
- qayxc 6y ago
  No - that's simply not true. The Halting Problem states that there is no Turing Machine (i.e. program) capable of deciding whether a given program will halt. And yes, humans are very well capable of solving that, because humans can in fact proof whether any program halts. This doesn't mean every human can or that it has been done for every program, but it means that humans are - in general - able capable of deciding this, while algorithms (programs) can't.
  - tsimionescu 6y ago
    The Church-Turing thesis claims (and is believed to be right) that a Turing machine can solve (compute) any problem that can be solved (is computable). For now at least, we don't know of any counter-example to the Church-Turing thesis. Humans are certainly not able to tell whether a program in general will halt for any input it recieves. If you believe otherwise, please tell me whether the following program halts: Foo(): if P = NP: return true else: Foo()