← Back to context

Comment by sharemywin

4 years ago

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.

35 comments

sharemywin

Reply
zackmorris  4 years 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.

sharemywin  4 years ago

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

the_af  4 years 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.

  • nl  4 years 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.

    • the_af  4 years ago

      So is in your opinion General AI solved? Because reliably turning symbols into meaning, outside narrow or special cases, is General AI.

      In my opinion, it's not solved. GPT-3 is not General AI, it's a more clever mechanism for parroting back text it cannot truly understand. Comparisons to ways humans confuse themselves are a red herring in my opinion: the old ELIZA program could reply like a very confused or trollish human would, but nobody would argue ELIZA was a general AI.

      It's just that GPT is a fascinating and more convincing illusion than ELIZA. Unlike ELIZA, it can also be used for meaningful purposes.

      5 replies →

JacobiX  4 years 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).

  • thwayunion  4 years 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

    [2] https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_...

    [3] https://github.com/bollu/diffgeo

    • the_af  4 years 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.

  • PaulHoule  4 years ago

    There has been big progress in automated theorem proving lately

    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-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_  4 years 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?

      2 replies →

  • IshKebab  4 years 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  4 years 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…