5 ms·

computers already do math. language models just need to translate problems into code of some kind that can be run to get the answer. executive function/plannin

computers already do math. language models just need to translate problems into code of some kind that can be run to get the answer. executive function/planning is probably the biggest problem at this point for ai.

JacobiX 4y ago
I'm not so sure about that. Of course computers can do arithmetic operations, but this is not the same as solving math problems, proving theorems, etc. Even mathematical objects are approximated up to an approximation error in a computer (like a differentiable manifold or a real number).
- sharemywin 4y ago
  Online Integral Calculator Solve integrals with Wolfram|Alpha https://www.wolframalpha.com/calculators/integral-calculator/ https://www.wolframalpha.com/calculators/integral-calculator...
  - sva_ 4y ago
    Now try to make a computer prove that there are no natural numbers a,b,c; so that a^n + b^n = c^n for any n > 2.
    - sharemywin 4y ago
      I guess it depends on the outcome your worried about. Super intelligence or machines that replace the average office worker.
    - Sharlin 4y ago
      Shifting the goal posts a bit, aren't we?
- PaulHoule 4y ago
  There has been big progress in automated theorem proving lately https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving you just don't hear about it much because the technology is not so fashionable today. Also it is more clear what the limits are, I mean, Turing, Godel, Tarski and all of those apply to neural networks as well any other formal system but people mostly forget it. Knuth wrote a really fun volume of The Art of Computer Programming about advances in SAT solvers which are the foundation for theorem provers https://www.amazon.com/Art-Computer-Programming-Fascicle-Satisfiability/dp/0134397606 https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat... Everybody is aware that neural network techniques have improved drastically in performance, it's much more obscure that the toolbox of symbolic A.I. has improved greatly. Back in the 1980s production rules engines struggled to handle 10,000 rules, now Drools can handle 1,000,000+ rules with no problems.
  - sva_ 4y ago
    > There has been big progress in automated theorem proving lately It doesn't seem like there has been much progress for anything but FOL?
    - thwayunion 4y ago
      The wiki article on automated theorem proving is quite bad as an overview of the active field; it's more a historical article about the mid to late 20th century. Most of the interesting things in automated reasoning have happened since the naughts, and that article kind of stops in the 90s SMT solvers have gotten quite good over the past couple decades, there are tons of domain-specific tools (eg in software and hardware verification), tons of niche applied decidable or semi-decidable theories (eg various modal and description logics), a lot of progress on the proof assistant ("non-fully-automated theorem proving") paradigm, and so on.
    - PaulHoule 4y ago
      It's clear that commonsense reasoning needs to deal with modals, counterfactuals, defaults, temporal logic, etc. It's not hard to add some extensions to logic for a particular application but a very hard problem to develop a general purpose extended logic. I look at the logic-adjacent production rules systems which never really standardized some of the commonly necessary things such as agendas, priorities, defaults, etc.
- thwayunion 4y ago
  > Of course computers can do arithmetic operations, but this is not the same as solving math problems, proving theorems, etc. Computers can solve math problems and prove theorems; this remains a significant subfield of Computer Science with lots of industrial use cases. However, pure machine learning based approaches toward these problems remain subpar. > Even mathematical objects are approximated up to an approximation error in a computer (like a differentiable manifold or a real number). Only because it caught on (and in the case of non-computationally-intensive applications, for purely historical reasons). For example, Mathematica has Reals and even functionality for Reals that is literally impossible to implement for integers [1,2]. There are also precise characterizations of objects in differential geometry [3]. You could imagine applying LLMs to these types of programs a la Copilot, but when you do this you will find yourself agreeing with Paul Houle's observation that math is harder to fake than eg art, language, or even glue code for web apps. [1] https://reference.wolfram.com/language/ref/Reduce.html https://reference.wolfram.com/language/ref/Reduce.html [2] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [3] https://github.com/bollu/diffgeo https://github.com/bollu/diffgeo
  - the_af 4y ago
    > Computers can solve math problems and prove theorems But the specification of the problem must be done by a human, translating to a formalized system that the software can understand. And if there's a problem in the formal specification, it's mostly up to the human to notice and fix; the computer will happily output garbage or crash or enter an infinite loop. So it seems this translation, going from an exploration of the problem statement, usually in ambiguous terms, to a formal specification, and the awareness to possibly detect whether the answers make sense and the specs were right, is uniquely human.
- casey2 4y ago
  Counterexample: Shalosh B. Ekhad is a computer who is also a mathematician.
- IshKebab 4y ago
  Computers are much much better at all that stuff than almost everyone too. Try asking Wolfram Alpha to solve something. Computers have gotten really good at proving things in the last couple of decades and formal verification methods are becoming increasingly popular. I think sharemywin is probably on to something. It's going to be really hard for an AI to prove that e.g. x>0 && x+y <= 1 && y>1 is unsatisfiable, but it's trivial for an SMT solver. On the other hand it probably isn't that much of a leap to make an AI that can feed that problem into an SMT solver.
- Sharlin 4y ago
  Well, you don't need anything else than basic arithmetic to encode the entirety of, say, ZFC, enumerate every proposition in it, and halt iff you find a proof of whatever theorem you're after. It just might take a while…
PaulHoule 4y ago
That's not a bad approach, necessarily. There is a fairly simple program in https://www.amazon.com/Paradigms-Artificial-Intelligence-Programming-Studies/dp/1558601910 https://www.amazon.com/Paradigms-Artificial-Intelligence-Pro... that solves word problems using the methods of the old AI. The point is that is is efficient and effective to use real math operators and not expect to fit numbers through the mysterious bottleneck of neural encoding.
sharemywin 4y ago
The point I'm trying to make is LLMs don't need to do everything just be the glue to other systems.
- enord 4y ago
  Wait what? Glue as in extract high level semantic representations from _syntatic probabilities_ and pass on to appropriate domain specific tools? This is the glaring hole in LLMs, a paradoxical semantic incoherence despite impressive sentenial and gramatical coherence. As glue it is so thin as to be potable.
  - ricopags 4y ago
    Quoting this tweet[0]: "Here's a brief glimpse of our INCREDIBLE near future. GPT-3 armed with a Python interpreter can · do exact math · make API requests · answer in unprecedented ways" [0]https://twitter.com/sergeykarayev/status/1569377881440276481 https://twitter.com/sergeykarayev/status/1569377881440276481
    - enord 4y ago
      All that remains is a small matter of programming…
  - sharemywin 4y ago
    Language Models as Zero-Shot Planners: Extracting Actionable Knowledge for Embodied Agents https://wenlong.page/language-planner/ https://wenlong.page/language-planner/
  - sharemywin 4y ago
    you would still need an executive it would be more like a universal translator.
    - enord 4y ago
      Translate to what? The next likely string of characters? How would this executive even interact with it? Sibling comment of yours mentioned extracting low level steps from high level tasks but it needed another language model (no kidding!) to map to the «most likely» of the admissable actions. I mean, this shit is half baked even in theory.
zackmorris 4y ago
That's interesting, I hadn't made the connection between executive function and intelligence. I went through a burnout in 2019 that felt like having a stroke. My brain finally reached such a level of negative reinforcement after years of failure that it wouldn't let me work anymore. I'd go to do very simple tasks, everything from brushing my teath to writing a TODO list, and it was like the part of my brain that performed those tasks wasn't there anymore. Or at least, it no longer obeyed if it perceived a potential reward involved. It was like my motivation got reversed. I had to relearn how to do everything, despite knowing that no reward might come for a very long time, which took at least 6 months before I began recovering. The closest answer I have is that my brain healed through faith. I only bring it up because executive function may be associated with a subjective experience of meaning. If there's truly no point to anything, then it's hard to summon the motivation to string together a sequence of AI tasks into something more like AGI. I guess that's another way of saying that nihilism could be the final hurdle for AGI to overcome. It's like the human philosophical question of why there's something instead of nothing. Or why angels would choose to be incarnate on Earth to experience a life of suffering when it's so much easier to remain dissociated.
the_af 4y ago
> language models just need to translate problems into code of some kind that can be run to get the answer A huge "just"! Isn't this the magic step? Translating ambiguous symbols to meaning and combining them in meaningful ways is a big deal which, apparently, these AI models cannot do. They can just parrot things.
- gamegoblin 4y ago
  It’s already being done and will only get better: https://twitter.com/sergeykarayev/status/1569377881440276481 https://twitter.com/sergeykarayev/status/1569377881440276481
  - the_af 4y ago
    I suspect it's not solved, because solving this (beyond some trick/toy examples) is essentially solving General AI.
    - gamegoblin 4y ago
      It's unclear what you mean by "solved". Even a human can't turn every arbitrary problem into code to solve, but we still consider humans "generally intelligent". GPT3 can't turn as many problems into code as I can, but it can do some, and GPT4 (or whatever) will be able to do more, etc.
      - the_af 4y ago
        So is in your opinion General AI already working, only it cannot solve "as many problems"?
- nl 4y ago
  > Translating ambiguous symbols to meaning and combining them in meaningful ways is a big deal which, apparently, these AI models cannot do. Plenty of AI models do exactly this. Very clear examples include question answering models and code generation. In both cases novel, meaningful responses are generated. > They can just parrot things. That isn't true. While language models can parrot things it is generally special conditions that make them do it. Specifically, the conditional probability of the next character (or BPE or word depending on the model) has to be much higher than anything else which happens when the thing being parroted is unique text. If you ask most Americans or a language model what word comes next in this: fourscore and seven year.. they'll give the same answer, for the same reason.

JacobiX 4y ago

I'm not so sure about that. Of course computers can do arithmetic operations, but this is not the same as solving math problems, proving theorems, etc. Even mathematical objects are approximated up to an approximation error in a computer (like a differentiable manifold or a real number).

sharemywin 4y ago
Online Integral Calculator Solve integrals with Wolfram|Alpha https://www.wolframalpha.com/calculators/integral-calculator/ https://www.wolframalpha.com/calculators/integral-calculator...
- sva_ 4y ago
  Now try to make a computer prove that there are no natural numbers a,b,c; so that a^n + b^n = c^n for any n > 2.
  - sharemywin 4y ago
    I guess it depends on the outcome your worried about. Super intelligence or machines that replace the average office worker.
  - Sharlin 4y ago
    Shifting the goal posts a bit, aren't we?
PaulHoule 4y ago
There has been big progress in automated theorem proving lately https://en.wikipedia.org/wiki/Automated_theorem_proving https://en.wikipedia.org/wiki/Automated_theorem_proving you just don't hear about it much because the technology is not so fashionable today. Also it is more clear what the limits are, I mean, Turing, Godel, Tarski and all of those apply to neural networks as well any other formal system but people mostly forget it. Knuth wrote a really fun volume of The Art of Computer Programming about advances in SAT solvers which are the foundation for theorem provers https://www.amazon.com/Art-Computer-Programming-Fascicle-Satisfiability/dp/0134397606 https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat... Everybody is aware that neural network techniques have improved drastically in performance, it's much more obscure that the toolbox of symbolic A.I. has improved greatly. Back in the 1980s production rules engines struggled to handle 10,000 rules, now Drools can handle 1,000,000+ rules with no problems.
- sva_ 4y ago
  > There has been big progress in automated theorem proving lately It doesn't seem like there has been much progress for anything but FOL?
  - thwayunion 4y ago
    The wiki article on automated theorem proving is quite bad as an overview of the active field; it's more a historical article about the mid to late 20th century. Most of the interesting things in automated reasoning have happened since the naughts, and that article kind of stops in the 90s SMT solvers have gotten quite good over the past couple decades, there are tons of domain-specific tools (eg in software and hardware verification), tons of niche applied decidable or semi-decidable theories (eg various modal and description logics), a lot of progress on the proof assistant ("non-fully-automated theorem proving") paradigm, and so on.
  - PaulHoule 4y ago
    It's clear that commonsense reasoning needs to deal with modals, counterfactuals, defaults, temporal logic, etc. It's not hard to add some extensions to logic for a particular application but a very hard problem to develop a general purpose extended logic. I look at the logic-adjacent production rules systems which never really standardized some of the commonly necessary things such as agendas, priorities, defaults, etc.
thwayunion 4y ago
> Of course computers can do arithmetic operations, but this is not the same as solving math problems, proving theorems, etc. Computers can solve math problems and prove theorems; this remains a significant subfield of Computer Science with lots of industrial use cases. However, pure machine learning based approaches toward these problems remain subpar. > Even mathematical objects are approximated up to an approximation error in a computer (like a differentiable manifold or a real number). Only because it caught on (and in the case of non-computationally-intensive applications, for purely historical reasons). For example, Mathematica has Reals and even functionality for Reals that is literally impossible to implement for integers [1,2]. There are also precise characterizations of objects in differential geometry [3]. You could imagine applying LLMs to these types of programs a la Copilot, but when you do this you will find yourself agreeing with Paul Houle's observation that math is harder to fake than eg art, language, or even glue code for web apps. [1] https://reference.wolfram.com/language/ref/Reduce.html https://reference.wolfram.com/language/ref/Reduce.html [2] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... [3] https://github.com/bollu/diffgeo https://github.com/bollu/diffgeo
- the_af 4y ago
  > Computers can solve math problems and prove theorems But the specification of the problem must be done by a human, translating to a formalized system that the software can understand. And if there's a problem in the formal specification, it's mostly up to the human to notice and fix; the computer will happily output garbage or crash or enter an infinite loop. So it seems this translation, going from an exploration of the problem statement, usually in ambiguous terms, to a formal specification, and the awareness to possibly detect whether the answers make sense and the specs were right, is uniquely human.
casey2 4y ago
Counterexample: Shalosh B. Ekhad is a computer who is also a mathematician.
IshKebab 4y ago
Computers are much much better at all that stuff than almost everyone too. Try asking Wolfram Alpha to solve something. Computers have gotten really good at proving things in the last couple of decades and formal verification methods are becoming increasingly popular. I think sharemywin is probably on to something. It's going to be really hard for an AI to prove that e.g. x>0 && x+y <= 1 && y>1 is unsatisfiable, but it's trivial for an SMT solver. On the other hand it probably isn't that much of a leap to make an AI that can feed that problem into an SMT solver.
Sharlin 4y ago
Well, you don't need anything else than basic arithmetic to encode the entirety of, say, ZFC, enumerate every proposition in it, and halt iff you find a proof of whatever theorem you're after. It just might take a while…

PaulHoule 4y ago

That's not a bad approach, necessarily. There is a fairly simple program in https://www.amazon.com/Paradigms-Artificial-Intelligence-Programming-Studies/dp/1558601910 https://www.amazon.com/Paradigms-Artificial-Intelligence-Pro... that solves word problems using the methods of the old AI. The point is that is is efficient and effective to use real math operators and not expect to fit numbers through the mysterious bottleneck of neural encoding.

sharemywin 4y ago

The point I'm trying to make is LLMs don't need to do everything just be the glue to other systems.

enord 4y ago
Wait what? Glue as in extract high level semantic representations from _syntatic probabilities_ and pass on to appropriate domain specific tools? This is the glaring hole in LLMs, a paradoxical semantic incoherence despite impressive sentenial and gramatical coherence. As glue it is so thin as to be potable.
- ricopags 4y ago
  Quoting this tweet[0]: "Here's a brief glimpse of our INCREDIBLE near future. GPT-3 armed with a Python interpreter can · do exact math · make API requests · answer in unprecedented ways" [0]https://twitter.com/sergeykarayev/status/1569377881440276481 https://twitter.com/sergeykarayev/status/1569377881440276481
  - enord 4y ago
    All that remains is a small matter of programming…
- sharemywin 4y ago
  Language Models as Zero-Shot Planners: Extracting Actionable Knowledge for Embodied Agents https://wenlong.page/language-planner/ https://wenlong.page/language-planner/
- sharemywin 4y ago
  you would still need an executive it would be more like a universal translator.
  - enord 4y ago
    Translate to what? The next likely string of characters? How would this executive even interact with it? Sibling comment of yours mentioned extracting low level steps from high level tasks but it needed another language model (no kidding!) to map to the «most likely» of the admissable actions. I mean, this shit is half baked even in theory.

zackmorris 4y ago

That's interesting, I hadn't made the connection between executive function and intelligence. I went through a burnout in 2019 that felt like having a stroke. My brain finally reached such a level of negative reinforcement after years of failure that it wouldn't let me work anymore. I'd go to do very simple tasks, everything from brushing my teath to writing a TODO list, and it was like the part of my brain that performed those tasks wasn't there anymore. Or at least, it no longer obeyed if it perceived a potential reward involved. It was like my motivation got reversed. I had to relearn how to do everything, despite knowing that no reward might come for a very long time, which took at least 6 months before I began recovering. The closest answer I have is that my brain healed through faith. I only bring it up because executive function may be associated with a subjective experience of meaning. If there's truly no point to anything, then it's hard to summon the motivation to string together a sequence of AI tasks into something more like AGI. I guess that's another way of saying that nihilism could be the final hurdle for AGI to overcome. It's like the human philosophical question of why there's something instead of nothing. Or why angels would choose to be incarnate on Earth to experience a life of suffering when it's so much easier to remain dissociated.

the_af 4y ago

> language models just need to translate problems into code of some kind that can be run to get the answer A huge "just"! Isn't this the magic step? Translating ambiguous symbols to meaning and combining them in meaningful ways is a big deal which, apparently, these AI models cannot do. They can just parrot things.

gamegoblin 4y ago
It’s already being done and will only get better: https://twitter.com/sergeykarayev/status/1569377881440276481 https://twitter.com/sergeykarayev/status/1569377881440276481
- the_af 4y ago
  I suspect it's not solved, because solving this (beyond some trick/toy examples) is essentially solving General AI.
  - gamegoblin 4y ago
    It's unclear what you mean by "solved". Even a human can't turn every arbitrary problem into code to solve, but we still consider humans "generally intelligent". GPT3 can't turn as many problems into code as I can, but it can do some, and GPT4 (or whatever) will be able to do more, etc.
    - the_af 4y ago
      So is in your opinion General AI already working, only it cannot solve "as many problems"?
nl 4y ago
> Translating ambiguous symbols to meaning and combining them in meaningful ways is a big deal which, apparently, these AI models cannot do. Plenty of AI models do exactly this. Very clear examples include question answering models and code generation. In both cases novel, meaningful responses are generated. > They can just parrot things. That isn't true. While language models can parrot things it is generally special conditions that make them do it. Specifically, the conditional probability of the next character (or BPE or word depending on the model) has to be much higher than anything else which happens when the thing being parroted is unique text. If you ask most Americans or a language model what word comes next in this: fourscore and seven year.. they'll give the same answer, for the same reason.