13 ms·

Symbolic mathematics finally yields to neural networks

275 points by Zuider 6y ago

libeclipse 6y ago
> The Facebook researchers compared their method to only a few of Mathematica’s functions —“integrate” for integrals and “DSolve” for differential equations — but Mathematica users can access hundreds of other solving tools. > [...] it only included equations with one variable, and only those based on elementary functions. “It was a thin slice of possible expressions,” > The neural net wasn’t tested on messier functions often used in physics and finance, like error functions or Bessel functions. (The Facebook group said it could be, in future versions, with very simple modifications.) > Other critics have noted that the Facebook group’s neural net doesn’t really understand the math; it’s more of an exceptional guesser. > Still, they agree that the new approach will prove useful.
- libeclipse 6y ago
  I like this prospect: > Another unsolved problem where this approach shows promise is one of the most disturbing aspects of neural nets: No one really understands how they work. Training bits enter at one end and prediction bits emerge from the other, but what happens in between — the exact process that makes neural nets into such good guessers — remains a critical open question. > Symbolic math, on the other hand, is decidedly less mysterious. “We know how math works,” said Charton. “By using specific math problems as a test to see where machines succeed and where they fail, we can learn how neural nets work.”
  - neatze 6y ago
    > “By using specific math problems as a test to see where machines succeed and where they fail, we can learn how neural nets work.” XOR and Spiral benchmark was studied in neural networks since 70's.
- odyssey7 6y ago
  The criticisms read as good starting points for subsequent research.
- uoaei 6y ago
  > exceptional guesser Considering neural networks are inherently maximizing probabilities and statistical descriptions of data, this should come as no surprise. This work has not dissolved the dichotomy between rules-based and statistical methods, but rather transmuted the syntax of rules-based expressions into a representation that can be exploited by statistical machines in a way that makes "guessing" more fruitful. There are some examples near the end of the paper showing how the authors take an initially intractable expression and are able to simplify it with their approach so that Mathematica can actually perform the integral for them. It seems much more appropriate to market this method as a preprocessor for massive expressions to a more chewable size.
  - sdenton4 6y ago
    > exceptional guesser This IMO describes how mathematics itself moves forward... A matematician is an extremely well-trained 'guesser' who is also able to sink a lot of time into formal verification. The process is essentially: a) Find an interesting conjecture that you've got a strong guess to be true. b) Check for obvious (or less obvious) counterexamples, or conflicting theorems. c) Prove the thing is true. A large part of the art of being a working mathematician is in part (a): you need to make a really good guess. An ideal conjecture is correct AND proveable AND leads to other interesting results, or says interesting things about bigger problems. So what happens when we apply really good versions of current AI to this area? Picking out an 'interesting' conjecture is still Strong-AI-Complete: it requires lots of domain knowledge, and an understanding of what this particular conjecture would 'unlock.' But we could perhaps come up with good 'guessers' which quickly tell us whether a given idea might work out, perhaps saving a bunch of effort. Perhaps we could even get to the point of generating a proposed proof which can be fed to an automated proof checking system, allowing for inspection and modification by the human in the loop.
peterlk 6y ago
This is one of the most exciting things I've seen come out of AI research for my own interests. The way that they distributed the mathematical equations is called an abstract syntax tree (maybe they mentioned this, but I was excited-skimming), and is also how computer code is represented. It also happens that there is _a lot_ more computer code laying around in computer-readable format than high school and college math problems. With this, you get: metamorphic code, better optimizers, more abstract programming languages (maybe), and probably lots of other steps forward. If anyone is working on AI+programming languages, please send me a message. I'd love to work with others on this problem.
- keenmaster 6y ago
  "With this, you get: ... more abstract programming languages (maybe)." That would be great. If you could guess, how would you go about using symbolic math and neural nets to create a more abstract programming language?
  - MaxBarraclough 6y ago
    If you'll entertain my clueless guesswork: If it could be used to greatly accelerate SMT solving/constraint solving, perhaps it would be possible to run a formal model as if it were code, i.e. fast and scalable constraint-based programming. That's about as high-level as you can get, short of a requirements document. I'm not sure if that's the kind of symbolic mathematics that's being studied here, as they seem to be looking at mathematically interesting expressions, rather than boring-but-enormous constraints. Or, somewhat related, perhaps it could be used to help scale formal verification with languages like SPARK and ZZ.
    - orange3xchicken 6y ago
      In general, I think neural networks really struggle with np hard problems. Current state of the art is bottlenecked wrt to even subtle generalization. The strong baselines have been variations on the pointer-network architecture for some time now. Even though they can do reasonably well on restricted problems (e.g. instances of sat/traveling salesman with fixed # of nodes), they struggle to generalize to instances of the problem with variable # of nodes - not to mention varying the problem itself. Some popular approaches also incl. applications of Graph CNNs & reinforcement learning. Don't really have much more than a cursory idea of the current directions though. To me, more exciting is some kind of joint collaboration between modern ml systems & formal solvers.
brianberns 6y ago
It seems that the neural net just spits out an answer, rather than deriving it step-by-step like humans do. That's interesting, but would still get you an F on a real calculus test.
- deleted 6y ago
  [deleted]
- gamegoblin 6y ago
  One could view each layer of the neural net as doing "steps". They are rather opaque steps, though.
- _bxg1 6y ago
  I think the idea with this kind of thing is that ML can make pretty-good guesses really quickly, and then a formalized process can verify them (usually much more quickly than it could derive them). This hybrid model fits lots of different kinds of problems.
- svantana 6y ago
  I think it's able to verify that the solution is correct, which is more than a lot of students manage.
- microtherion 6y ago
  Yes, and this is particularly problematic IMHO in sequence-to-sequence translators, as were used here. When fed enough training data, they do an amazing job at aping their training, but they are prone to spout utter nonsense in edge cases, and they don't really (to my knowledge) have any indication that they should have less confidence in one result than in the other. So best case this system gives black box answers that may or may not hold up in verification. That does not seem to be a very useful way to do mathematical research.
- kccqzy 6y ago
  Mathematica doesn't give you a step-by-step derivation for its integration either (although Wolfram Alpha sometimes does). That doesn't bother most people using the software.
_0ffh 6y ago
To me, the article somewhat misses the point of what's interesting here. Using ASTs to represent equations, or even whole programs has plenty of precedents in ML/AI. I'd have liked to know how exactly they translate these trees to a representation suitable for an ANN. Fortunately, the paper seems to be easy to find and access (it's [1], I guess). [1] https://arxiv.org/abs/1912.01412 https://arxiv.org/abs/1912.01412
- n-m-j 6y ago
  From your linked article, it seems they just use the trees to generate prefix notation.
- orange3xchicken 6y ago
  It looks like they go from tree -> sequence via prefix notation. I'm curious why Lample decided on this seq2seq approach when it seems that there might be models which could be more naturally applied to the tree structure directly [1, 2] [1] https://arxiv.org/abs/1902.07282 https://arxiv.org/abs/1902.07282 (an AST translation system) [2] https://arxiv.org/abs/1609.02907 https://arxiv.org/abs/1609.02907 (GCNN)
  - shmageggy 6y ago
    For the same reason people use huge transformers for sentences in natural language (which are also tree structured): they scale really well. If you have enough data, huge transformers have huge capacity. If you notice, this paper is entirely about how to cleverly generate a massive dataset. There is no novelty in the model -- they just use a standard approach described in two paragraphs.
augustt 6y ago
Discussion about the paper a while back: https://news.ycombinator.com/item?id=21084748 https://news.ycombinator.com/item?id=21084748. Conclusion seemed to be that the comparison against Mathematica was unfair since Mathematica's execution time was capped at 30s.
- hyperbovine 6y ago
  Interesting, since in my experience Mathematica's execution time is also lower-bounded by 30s.
- thomasahle 6y ago
  I don't think that was why it was considered unfair. The problem was rather that they tested on the same distribution the model had just seen 80 million examples from.
clircle 6y ago
What would a confidence interval for this type of prediction look like?
- bglazer 6y ago
  A confidence interval is a sort of meaningless notion in this case. You can just do the derivative of the algorithm's answer, and see if you get back an expression that is equivalent to the input. If you did, then the answer is correct.
  - clircle 6y ago
    I don't believe a model (neural network or otherwise) is capable of knowing that its predictions are correct.
neatze 6y ago
From article: “You need to be confident that it’s going to work all the time, and not just on some chosen problems” by mathematician Frédéric Gibou If I understand correctly, mathematical solutions can be verified, while neural network solutions would be very hard, if not impossible to verify in reasonable time.
- caleb-allen 6y ago
  It seems to me that this just kicks the can down the road--from calculation to verification.
  - ah- 6y ago
    Sometimes verification is much easier than calculation.
- jfkebwjsbx 6y ago
  It depends on the problem. For integration, you can just derive. For infinitely many other problems... verification is way harder.
  - empath75 6y ago
    is it usually the case that derivatives are easier to compute than integrals?
    - danbruc 6y ago
      The general algorithm for calculating integrals [1] is rather complex and I guess not suitable for humans so that calculating integrals sometimes looks much more like a black art then calculating derivatives does. On the other hand one could argue that there are algorithms for doing both and so there is no real difference. [1] https://en.wikipedia.org/wiki/Risch_algorithm https://en.wikipedia.org/wiki/Risch_algorithm
    - abstrakraft 6y ago
      Yes. Most of the time, the reason is that there is a general form for computing derivatives of products ((xy)' = x'y + xy') and composite functions (chain rule) while no such general rules exist for integrals.
samuel2 6y ago
How about using http://us.metamath.org/ http://us.metamath.org/ as a db for math theorems / definitions and do some heavy data mining there?
- raphlinus 6y ago
  There's some work on this already, including Holophrasm and work by OpenAI on proof shortening. These efforts are linked from the Metamath wiki: https://github.com/metamath/set.mm/wiki/Automated-proving https://github.com/metamath/set.mm/wiki/Automated-proving
  - samuel2 6y ago
    very cool, thanks for sharing
    - dwheeler 6y ago
      OpenAI has managed to derive a number of Metamath proofs, some of which are smaller than the human-created proofs, using machine learning. Here is a gource visualization of metamath proofs overtime in the set.mm database: https://m.youtube.com/watch?v=LVGSeDjWzUo https://m.youtube.com/watch?v=LVGSeDjWzUo Note that near the end, one of the contributors is OpenAI, who is not a human contributor.
globular-toast 6y ago
Symbolic mathematics (or computer algebra as it is more commonly known as) was one the original driving forces for AI. Differentiation turned out to be quite easy once things like ASTs and other data structures were developed to represent polynomials and other elementary functions. Integration is way more difficult and while AI research made great inroads the problem was eventually solved by algebraic methods. But the full algorithm (the Risch algorithm) is about 100 pages long and has never been fully implemented. The Axiom computer algebra system is the closest AFAIK, but the premature loss of Manuel Bronstein set it back a bit (that system is fascinating as well, it's a literate program in Lisp). The AI approaches always had one great problem: if they can't find an integral you still have no idea whether an integral exists or not. The Risch algorithm, on the other hand, can tell you for sure if an (elementary) integral doesn't exist. Axiom is fully capable of saying "no", but can't always tell you what the integral is if it does exist. Using an AST to represent expressions isn't novel, by the way. I implemented such a system as an undergrad computer science student (I also implemented complete integration of rational functions).
nano_o 6y ago
You might find the Sledgehammer tool for Isabelle quite interesting. It has been using machine learning techniques to find proofs automatically since at least 2013. It uses previous proof to learn how to select facts to send to off-the-shelf automated provers in order to discharge a goal. See e.g. http://isabelle.in.tum.de/~blanchet/mash2.pdf http://isabelle.in.tum.de/~blanchet/mash2.pdf On issue I have with it, and that automated proof tools based on ML are going to have to solve, is that it's quite unpredictable. Even if it finds stunning proofs from time to time, it is hard to use an unpredictable tool efficiently.
microtherion 6y ago
Here's a somewhat more technical critique of the approach (and of the evaluation cases the authors used): https://arxiv.org/pdf/1912.05752.pdf https://arxiv.org/pdf/1912.05752.pdf
- newpycai 6y ago
  > It is important to emphasize thatthe construction of LC is entirely dependent on the pre-existingsymbolic processors developed over the last 50 years by experts in symbolic mathematics.Moreover,as things now stand, extending LC to fill in some of its gaps (e.g. the simplification problemsdescribed in section 3) would make it even less of a stand-alone system and more dependent onconventional symbolic processors. There is no reason whatever to suppose that NN-based systemswill supercede symbolic mathematics systems any time in the foreseeable future. That's the gem of the review.
- newpycai 6y ago
  And this paragraph > It goes without saying that LC has no understanding of the significance of an integral or a derivativeor even a function or a number. In fact, occasionally, it outputs a solution that is not even a well-formed expression. LC is like the worst possible student in a calculus class: it doesn’t understandthe concepts, it doesn’t learned the rules, it has no idea what is the significance of what it is doing,but it has looked at 80 million examples and gotten a feeling of what integrands and their integralslook like.
zengid 6y ago
This looks really interesting! Although, I'm not sure if this was "first". I know of another approach tried by Hinton and Sutskever in their paper "Using matrices to model symbolic relationships" [0]. I don't see a date, but I remember Hinton mentioning it in a talk from a few years ago.. [0] https://www.cs.toronto.edu/~hinton/absps/ilyamre.pdf https://www.cs.toronto.edu/~hinton/absps/ilyamre.pdf
KKKKkkkk1 6y ago
So what's the earliest known AI solver for calculus textbook problems? I bet it goes all the way to the 1950s. This quote seems to be massively misleading: But it’s clear that the team has answered the decades-old question — can AI do symbolic math? — in the affirmative. “Their models are well established. The algorithms are well established. They postulate the problem in a clever way,” said Wojciech Zaremba, co-founder of the AI research group OpenAI. “They did succeed in coming up with neural networks that could solve problems that were beyond the scope of the rule-following machine system,” McClelland said. “Which is very exciting.”
- rst 6y ago
  Grace Hopper was experimenting with symbolic differentiation of functions in her A-2 compiler in the 1950s, and she may well not have been the first. My reference for this is her paper in the proceedings of a 1957 British conference on "Mechanisation of Thought Processes" -- if you set up an account at archive.org, they may let you page through it here: https://archive.org/details/mechanisationoft02nati/page/n9/mode/2up https://archive.org/details/mechanisationoft02nati/page/n9/m...
  - mkl 6y ago
    Not AI, though (or almost every computer program would be "AI"). Differentiation can be done with simple deterministic rule following.
    - rst 6y ago
      Earliest reference I'm aware of for integration is James Slagle's MIT Ph.D. thesis work, from 1961. https://dspace.mit.edu/handle/1721.1/11997 https://dspace.mit.edu/handle/1721.1/11997
      - deleted 6y ago
        [deleted]
todd8 6y ago
About 50 years ago I was fascinated to see a program that could do symbolic integration. Now, programs like Mathematica can do much harder, more complex integrals. Professor Patrick Winston pointed out that most of the AI programs we were going to look at in his class (chess, natural language, 3D vision in block world, etc.) ended up, like integration, as simple code plus a database of facts. Back then, there was general optimism about the future of AI. No one anticipated how slow progress would be while the capabilities of the hardware grew a million-fold. The work referenced in the article is interesting. It appears to be another small step in advancing AI. It's a small, but difficult, step like almost every other advance in AI, and I admire the work done by those working in this field. The problems of solving simple differential equations and symbolic integration at the first year calculus level are not really advanced math. Humans solve these problems with a relatively small bag of tricks that transform a symbolic integral into a simpler form. A program can do the same thing with an even more detailed database of transforms that can be attempted at each point in the search tree until a simple solution is reached. The article claims that the new program can solve difficult integrals. This is interesting because hard to solve integrals are often associated with real physical phenomena. See for example the triple integrals of W. F. van Peype which arose while he was studying magnetism in different materials. These, relatively, plain looking definite integrals stumped some of the world's most famous mathematicians. See [1] and/or [2] for their interesting history. [1] Paul J. Nahin, Inside Interesting Integrals, Springer, 2015. Section 6.5, The Watson/van Peype Triple Integrals. [2] I.J. Zucker, 70+ Years of the Watson Integrals, http://www.inp.nsk.su/~silagadz/Watson_Integral.pdf http://www.inp.nsk.su/~silagadz/Watson_Integral.pdf
- jiggawatts 6y ago
  Even that first integral is a doozy! Mathematica spent minutes on it and spat out an answer that looks much more complex than the one in the paper: Integrate[Pi * Csc[x/2]^2 * EllipticK[(-Cos[x]) * Csc[x/2]^4], {x, 0, Pi}]/Pi^3 It can't even evaluate the answer numerically, it just freezes for minutes! Edit: about 10 minutes later it spat out 1.393203930, so it can solve the integral, but not easily. Update: This paper reminds me why I vehemently hate modern mathematical notation, with subscripts and superscripts can mean anything at all and everyone's idea of "convention" is different. On the second page there's an algebraic expression for the solution, which at first glance seems to be: 4/Pi^2 * EllipticK[Sqrt[1/2 - Sqrt[1 - w^(-2)]/2]]^2 But this evaluates to 1.76351 not 1.39320 as given in the paper. The "K^2" in the paper is not the "complete elliptic integral of the first kind" squared, it's some other function that squares its input somehow. Or something. But that begs the question of why formulate this in terms of a function of a square root squared!? Helpfully, they provide the definition in terms of the hypergeometric function a bit lower down, but that appears to be wrong as well, providing yet another result if evaluated numerically.
nullc 6y ago
Just need to build a tool that predicts the next version of a program from an earlier version and suggests improvements (ideally bug fixes). Then you have http://www.scp-wiki.net/scp-914 http://www.scp-wiki.net/scp-914 for programs.
enricozb 6y ago
Since ML outputs are usually "fuzzy", how does one check that the output is actually correct when using a technique like this in the field?
paulus_magnus2 6y ago
It would be really interesting to see code simplification via neural network. While working in enterprise I see plenty of code that after some massaging collapses into a much simpler form (for the programmer) and equivalent for the computer. (fix typo)

275 points by Zuider 6y ago

> The Facebook researchers compared their method to only a few of Mathematica’s functions —“integrate” for integrals and “DSolve” for differential equations — but Mathematica users can access hundreds of other solving tools. > [...] it only included equations with one variable, and only those based on elementary functions. “It was a thin slice of possible expressions,” > The neural net wasn’t tested on messier functions often used in physics and finance, like error functions or Bessel functions. (The Facebook group said it could be, in future versions, with very simple modifications.) > Other critics have noted that the Facebook group’s neural net doesn’t really understand the math; it’s more of an exceptional guesser. > Still, they agree that the new approach will prove useful.

libeclipse 6y ago
I like this prospect: > Another unsolved problem where this approach shows promise is one of the most disturbing aspects of neural nets: No one really understands how they work. Training bits enter at one end and prediction bits emerge from the other, but what happens in between — the exact process that makes neural nets into such good guessers — remains a critical open question. > Symbolic math, on the other hand, is decidedly less mysterious. “We know how math works,” said Charton. “By using specific math problems as a test to see where machines succeed and where they fail, we can learn how neural nets work.”
- neatze 6y ago
  > “By using specific math problems as a test to see where machines succeed and where they fail, we can learn how neural nets work.” XOR and Spiral benchmark was studied in neural networks since 70's.
odyssey7 6y ago
The criticisms read as good starting points for subsequent research.
uoaei 6y ago
> exceptional guesser Considering neural networks are inherently maximizing probabilities and statistical descriptions of data, this should come as no surprise. This work has not dissolved the dichotomy between rules-based and statistical methods, but rather transmuted the syntax of rules-based expressions into a representation that can be exploited by statistical machines in a way that makes "guessing" more fruitful. There are some examples near the end of the paper showing how the authors take an initially intractable expression and are able to simplify it with their approach so that Mathematica can actually perform the integral for them. It seems much more appropriate to market this method as a preprocessor for massive expressions to a more chewable size.
- sdenton4 6y ago
  > exceptional guesser This IMO describes how mathematics itself moves forward... A matematician is an extremely well-trained 'guesser' who is also able to sink a lot of time into formal verification. The process is essentially: a) Find an interesting conjecture that you've got a strong guess to be true. b) Check for obvious (or less obvious) counterexamples, or conflicting theorems. c) Prove the thing is true. A large part of the art of being a working mathematician is in part (a): you need to make a really good guess. An ideal conjecture is correct AND proveable AND leads to other interesting results, or says interesting things about bigger problems. So what happens when we apply really good versions of current AI to this area? Picking out an 'interesting' conjecture is still Strong-AI-Complete: it requires lots of domain knowledge, and an understanding of what this particular conjecture would 'unlock.' But we could perhaps come up with good 'guessers' which quickly tell us whether a given idea might work out, perhaps saving a bunch of effort. Perhaps we could even get to the point of generating a proposed proof which can be fed to an automated proof checking system, allowing for inspection and modification by the human in the loop.

peterlk 6y ago

This is one of the most exciting things I've seen come out of AI research for my own interests. The way that they distributed the mathematical equations is called an abstract syntax tree (maybe they mentioned this, but I was excited-skimming), and is also how computer code is represented. It also happens that there is _a lot_ more computer code laying around in computer-readable format than high school and college math problems. With this, you get: metamorphic code, better optimizers, more abstract programming languages (maybe), and probably lots of other steps forward. If anyone is working on AI+programming languages, please send me a message. I'd love to work with others on this problem.

keenmaster 6y ago
"With this, you get: ... more abstract programming languages (maybe)." That would be great. If you could guess, how would you go about using symbolic math and neural nets to create a more abstract programming language?
- MaxBarraclough 6y ago
  If you'll entertain my clueless guesswork: If it could be used to greatly accelerate SMT solving/constraint solving, perhaps it would be possible to run a formal model as if it were code, i.e. fast and scalable constraint-based programming. That's about as high-level as you can get, short of a requirements document. I'm not sure if that's the kind of symbolic mathematics that's being studied here, as they seem to be looking at mathematically interesting expressions, rather than boring-but-enormous constraints. Or, somewhat related, perhaps it could be used to help scale formal verification with languages like SPARK and ZZ.
  - orange3xchicken 6y ago
    In general, I think neural networks really struggle with np hard problems. Current state of the art is bottlenecked wrt to even subtle generalization. The strong baselines have been variations on the pointer-network architecture for some time now. Even though they can do reasonably well on restricted problems (e.g. instances of sat/traveling salesman with fixed # of nodes), they struggle to generalize to instances of the problem with variable # of nodes - not to mention varying the problem itself. Some popular approaches also incl. applications of Graph CNNs & reinforcement learning. Don't really have much more than a cursory idea of the current directions though. To me, more exciting is some kind of joint collaboration between modern ml systems & formal solvers.

brianberns 6y ago

It seems that the neural net just spits out an answer, rather than deriving it step-by-step like humans do. That's interesting, but would still get you an F on a real calculus test.

deleted 6y ago
[deleted]
gamegoblin 6y ago
One could view each layer of the neural net as doing "steps". They are rather opaque steps, though.
_bxg1 6y ago
I think the idea with this kind of thing is that ML can make pretty-good guesses really quickly, and then a formalized process can verify them (usually much more quickly than it could derive them). This hybrid model fits lots of different kinds of problems.
svantana 6y ago
I think it's able to verify that the solution is correct, which is more than a lot of students manage.
microtherion 6y ago
Yes, and this is particularly problematic IMHO in sequence-to-sequence translators, as were used here. When fed enough training data, they do an amazing job at aping their training, but they are prone to spout utter nonsense in edge cases, and they don't really (to my knowledge) have any indication that they should have less confidence in one result than in the other. So best case this system gives black box answers that may or may not hold up in verification. That does not seem to be a very useful way to do mathematical research.
kccqzy 6y ago
Mathematica doesn't give you a step-by-step derivation for its integration either (although Wolfram Alpha sometimes does). That doesn't bother most people using the software.

_0ffh 6y ago

To me, the article somewhat misses the point of what's interesting here. Using ASTs to represent equations, or even whole programs has plenty of precedents in ML/AI. I'd have liked to know how exactly they translate these trees to a representation suitable for an ANN. Fortunately, the paper seems to be easy to find and access (it's [1], I guess). [1] https://arxiv.org/abs/1912.01412 https://arxiv.org/abs/1912.01412

n-m-j 6y ago
From your linked article, it seems they just use the trees to generate prefix notation.
orange3xchicken 6y ago
It looks like they go from tree -> sequence via prefix notation. I'm curious why Lample decided on this seq2seq approach when it seems that there might be models which could be more naturally applied to the tree structure directly [1, 2] [1] https://arxiv.org/abs/1902.07282 https://arxiv.org/abs/1902.07282 (an AST translation system) [2] https://arxiv.org/abs/1609.02907 https://arxiv.org/abs/1609.02907 (GCNN)
- shmageggy 6y ago
  For the same reason people use huge transformers for sentences in natural language (which are also tree structured): they scale really well. If you have enough data, huge transformers have huge capacity. If you notice, this paper is entirely about how to cleverly generate a massive dataset. There is no novelty in the model -- they just use a standard approach described in two paragraphs.

augustt 6y ago

Discussion about the paper a while back: https://news.ycombinator.com/item?id=21084748 https://news.ycombinator.com/item?id=21084748. Conclusion seemed to be that the comparison against Mathematica was unfair since Mathematica's execution time was capped at 30s.

hyperbovine 6y ago
Interesting, since in my experience Mathematica's execution time is also lower-bounded by 30s.
thomasahle 6y ago
I don't think that was why it was considered unfair. The problem was rather that they tested on the same distribution the model had just seen 80 million examples from.

clircle 6y ago

What would a confidence interval for this type of prediction look like?

bglazer 6y ago
A confidence interval is a sort of meaningless notion in this case. You can just do the derivative of the algorithm's answer, and see if you get back an expression that is equivalent to the input. If you did, then the answer is correct.
- clircle 6y ago
  I don't believe a model (neural network or otherwise) is capable of knowing that its predictions are correct.

neatze 6y ago

From article: “You need to be confident that it’s going to work all the time, and not just on some chosen problems” by mathematician Frédéric Gibou If I understand correctly, mathematical solutions can be verified, while neural network solutions would be very hard, if not impossible to verify in reasonable time.

caleb-allen 6y ago
It seems to me that this just kicks the can down the road--from calculation to verification.
- ah- 6y ago
  Sometimes verification is much easier than calculation.
jfkebwjsbx 6y ago
It depends on the problem. For integration, you can just derive. For infinitely many other problems... verification is way harder.
- empath75 6y ago
  is it usually the case that derivatives are easier to compute than integrals?
  - danbruc 6y ago
    The general algorithm for calculating integrals [1] is rather complex and I guess not suitable for humans so that calculating integrals sometimes looks much more like a black art then calculating derivatives does. On the other hand one could argue that there are algorithms for doing both and so there is no real difference. [1] https://en.wikipedia.org/wiki/Risch_algorithm https://en.wikipedia.org/wiki/Risch_algorithm
  - abstrakraft 6y ago
    Yes. Most of the time, the reason is that there is a general form for computing derivatives of products ((xy)' = x'y + xy') and composite functions (chain rule) while no such general rules exist for integrals.

samuel2 6y ago

How about using http://us.metamath.org/ http://us.metamath.org/ as a db for math theorems / definitions and do some heavy data mining there?

raphlinus 6y ago
There's some work on this already, including Holophrasm and work by OpenAI on proof shortening. These efforts are linked from the Metamath wiki: https://github.com/metamath/set.mm/wiki/Automated-proving https://github.com/metamath/set.mm/wiki/Automated-proving
- samuel2 6y ago
  very cool, thanks for sharing
  - dwheeler 6y ago
    OpenAI has managed to derive a number of Metamath proofs, some of which are smaller than the human-created proofs, using machine learning. Here is a gource visualization of metamath proofs overtime in the set.mm database: https://m.youtube.com/watch?v=LVGSeDjWzUo https://m.youtube.com/watch?v=LVGSeDjWzUo Note that near the end, one of the contributors is OpenAI, who is not a human contributor.

globular-toast 6y ago

Symbolic mathematics (or computer algebra as it is more commonly known as) was one the original driving forces for AI. Differentiation turned out to be quite easy once things like ASTs and other data structures were developed to represent polynomials and other elementary functions. Integration is way more difficult and while AI research made great inroads the problem was eventually solved by algebraic methods. But the full algorithm (the Risch algorithm) is about 100 pages long and has never been fully implemented. The Axiom computer algebra system is the closest AFAIK, but the premature loss of Manuel Bronstein set it back a bit (that system is fascinating as well, it's a literate program in Lisp). The AI approaches always had one great problem: if they can't find an integral you still have no idea whether an integral exists or not. The Risch algorithm, on the other hand, can tell you for sure if an (elementary) integral doesn't exist. Axiom is fully capable of saying "no", but can't always tell you what the integral is if it does exist. Using an AST to represent expressions isn't novel, by the way. I implemented such a system as an undergrad computer science student (I also implemented complete integration of rational functions).

nano_o 6y ago

You might find the Sledgehammer tool for Isabelle quite interesting. It has been using machine learning techniques to find proofs automatically since at least 2013. It uses previous proof to learn how to select facts to send to off-the-shelf automated provers in order to discharge a goal. See e.g. http://isabelle.in.tum.de/~blanchet/mash2.pdf http://isabelle.in.tum.de/~blanchet/mash2.pdf On issue I have with it, and that automated proof tools based on ML are going to have to solve, is that it's quite unpredictable. Even if it finds stunning proofs from time to time, it is hard to use an unpredictable tool efficiently.

microtherion 6y ago

Here's a somewhat more technical critique of the approach (and of the evaluation cases the authors used): https://arxiv.org/pdf/1912.05752.pdf https://arxiv.org/pdf/1912.05752.pdf

newpycai 6y ago
> It is important to emphasize thatthe construction of LC is entirely dependent on the pre-existingsymbolic processors developed over the last 50 years by experts in symbolic mathematics.Moreover,as things now stand, extending LC to fill in some of its gaps (e.g. the simplification problemsdescribed in section 3) would make it even less of a stand-alone system and more dependent onconventional symbolic processors. There is no reason whatever to suppose that NN-based systemswill supercede symbolic mathematics systems any time in the foreseeable future. That's the gem of the review.
newpycai 6y ago
And this paragraph > It goes without saying that LC has no understanding of the significance of an integral or a derivativeor even a function or a number. In fact, occasionally, it outputs a solution that is not even a well-formed expression. LC is like the worst possible student in a calculus class: it doesn’t understandthe concepts, it doesn’t learned the rules, it has no idea what is the significance of what it is doing,but it has looked at 80 million examples and gotten a feeling of what integrands and their integralslook like.

zengid 6y ago

This looks really interesting! Although, I'm not sure if this was "first". I know of another approach tried by Hinton and Sutskever in their paper "Using matrices to model symbolic relationships" [0]. I don't see a date, but I remember Hinton mentioning it in a talk from a few years ago.. [0] https://www.cs.toronto.edu/~hinton/absps/ilyamre.pdf https://www.cs.toronto.edu/~hinton/absps/ilyamre.pdf

KKKKkkkk1 6y ago

So what's the earliest known AI solver for calculus textbook problems? I bet it goes all the way to the 1950s. This quote seems to be massively misleading: But it’s clear that the team has answered the decades-old question — can AI do symbolic math? — in the affirmative. “Their models are well established. The algorithms are well established. They postulate the problem in a clever way,” said Wojciech Zaremba, co-founder of the AI research group OpenAI. “They did succeed in coming up with neural networks that could solve problems that were beyond the scope of the rule-following machine system,” McClelland said. “Which is very exciting.”

rst 6y ago
Grace Hopper was experimenting with symbolic differentiation of functions in her A-2 compiler in the 1950s, and she may well not have been the first. My reference for this is her paper in the proceedings of a 1957 British conference on "Mechanisation of Thought Processes" -- if you set up an account at archive.org, they may let you page through it here: https://archive.org/details/mechanisationoft02nati/page/n9/mode/2up https://archive.org/details/mechanisationoft02nati/page/n9/m...
- mkl 6y ago
  Not AI, though (or almost every computer program would be "AI"). Differentiation can be done with simple deterministic rule following.
  - rst 6y ago
    Earliest reference I'm aware of for integration is James Slagle's MIT Ph.D. thesis work, from 1961. https://dspace.mit.edu/handle/1721.1/11997 https://dspace.mit.edu/handle/1721.1/11997
    - deleted 6y ago
      [deleted]

todd8 6y ago

About 50 years ago I was fascinated to see a program that could do symbolic integration. Now, programs like Mathematica can do much harder, more complex integrals. Professor Patrick Winston pointed out that most of the AI programs we were going to look at in his class (chess, natural language, 3D vision in block world, etc.) ended up, like integration, as simple code plus a database of facts. Back then, there was general optimism about the future of AI. No one anticipated how slow progress would be while the capabilities of the hardware grew a million-fold. The work referenced in the article is interesting. It appears to be another small step in advancing AI. It's a small, but difficult, step like almost every other advance in AI, and I admire the work done by those working in this field. The problems of solving simple differential equations and symbolic integration at the first year calculus level are not really advanced math. Humans solve these problems with a relatively small bag of tricks that transform a symbolic integral into a simpler form. A program can do the same thing with an even more detailed database of transforms that can be attempted at each point in the search tree until a simple solution is reached. The article claims that the new program can solve difficult integrals. This is interesting because hard to solve integrals are often associated with real physical phenomena. See for example the triple integrals of W. F. van Peype which arose while he was studying magnetism in different materials. These, relatively, plain looking definite integrals stumped some of the world's most famous mathematicians. See [1] and/or [2] for their interesting history. [1] Paul J. Nahin, Inside Interesting Integrals, Springer, 2015. Section 6.5, The Watson/van Peype Triple Integrals. [2] I.J. Zucker, 70+ Years of the Watson Integrals, http://www.inp.nsk.su/~silagadz/Watson_Integral.pdf http://www.inp.nsk.su/~silagadz/Watson_Integral.pdf

jiggawatts 6y ago
Even that first integral is a doozy! Mathematica spent minutes on it and spat out an answer that looks much more complex than the one in the paper: Integrate[Pi * Csc[x/2]^2 * EllipticK[(-Cos[x]) * Csc[x/2]^4], {x, 0, Pi}]/Pi^3 It can't even evaluate the answer numerically, it just freezes for minutes! Edit: about 10 minutes later it spat out 1.393203930, so it can solve the integral, but not easily. Update: This paper reminds me why I vehemently hate modern mathematical notation, with subscripts and superscripts can mean anything at all and everyone's idea of "convention" is different. On the second page there's an algebraic expression for the solution, which at first glance seems to be: 4/Pi^2 * EllipticK[Sqrt[1/2 - Sqrt[1 - w^(-2)]/2]]^2 But this evaluates to 1.76351 not 1.39320 as given in the paper. The "K^2" in the paper is not the "complete elliptic integral of the first kind" squared, it's some other function that squares its input somehow. Or something. But that begs the question of why formulate this in terms of a function of a square root squared!? Helpfully, they provide the definition in terms of the hypergeometric function a bit lower down, but that appears to be wrong as well, providing yet another result if evaluated numerically.

nullc 6y ago

Just need to build a tool that predicts the next version of a program from an earlier version and suggests improvements (ideally bug fixes). Then you have http://www.scp-wiki.net/scp-914 http://www.scp-wiki.net/scp-914 for programs.

enricozb 6y ago

Since ML outputs are usually "fuzzy", how does one check that the output is actually correct when using a technique like this in the field?

paulus_magnus2 6y ago

It would be really interesting to see code simplification via neural network. While working in enterprise I see plenty of code that after some massaging collapses into a much simpler form (for the programmer) and equivalent for the computer. (fix typo)