← Back to context

Comment by 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).

13 comments

JacobiX

Reply
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?

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

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…