8 ms·

Using neural networks to solve advanced mathematics equations

101 points by robinhouston 7y ago

dooglius 7y ago
Previous discussion: https://news.ycombinator.com/item?id=21084748 https://news.ycombinator.com/item?id=21084748 I think the point in the comments about Mathematica et al just being more careful about the domain is pretty damning of the claim the neural net beats them.
boyadjian 7y ago
Now, we can really talk about AI.
whatshisface 7y ago
Solving "advanced mathematics equations," as opposed to advanced English literature equations?
- dragonwriter 7y ago
  More likely as opposed to advanced chemical or logic or ... equations. “Mathematical” is a meaningful modifier, not a frivolous one, for “equation”.
xvilka 7y ago
There is CoqHammer[1] and ProverBot[2] for going even further - proving the theorems. [1] https://github.com/lukaszcz/coqhammer https://github.com/lukaszcz/coqhammer [2] https://github.com/UCSD-PL/proverbot9001 https://github.com/UCSD-PL/proverbot9001
haskellandchill 7y ago
> Facebook AI has built the first AI system that can solve advanced mathematics equations using symbolic reasoning Uh, this isn't true. Even their paper cites previous work. I guess it's PR speak. A little disappointing that it just guesses solutions and doesn't offer proofs.
mdswanson 7y ago
"First, we developed a process that effectively unpacks equations, laying them out in a branching, treelike structure..." Umm...like an expression tree, perhaps? https://www.geeksforgeeks.org/expression-tree/ https://www.geeksforgeeks.org/expression-tree/
- laxd 7y ago
  They call it an expression-tree syntax two paragraphs down.
  - mdswanson 7y ago
    Congratulations! They re-invented it: "...our expression-tree syntax..."
lvh 7y ago
It seems bananas to me that Mathematica and other existing CASes can't solve that first sample equation: it reads like a straightforward integration, taking just a parameter substitution and an inverse trig derivative (which I feel like everyone doing calculus knows by heart?). Maybe I should go do it on paper and I'm missing the hard part?
- nimish 7y ago
  The risch algorithm is not trivial to implement.
  - lvh 7y ago
    Sure, but this is Mathematica, the self-proclaimed leading mathematics package!
- pfedak 7y ago
  That surprised me too. I found that Mathematica could solve it if you give it the denominator as 1-u^2 for the eventual substitution. Perhaps it just doesn't try very hard to look for substitutions? I could believe it not giving a lot of "coverage" per time spent compared to more advanced techniques.
thanatropism 7y ago
I wonder if there is research on using deep learning for stuff like SAT solvers.
- brtanymore 7y ago
  SAT may be a game with rules too simple for DL approaches to outperform state-of-the-art traditional solvers right now, but SMT (Satisfiability modulo theories) is another story: https://papers.nips.cc/paper/8233-learning-to-solve-smt-formulas.pdf https://papers.nips.cc/paper/8233-learning-to-solve-smt-form...
m3kw9 7y ago
Would this be more like calculus where you plug in a range of numbers to get to a target?
gambler 7y ago
This paper makes so many convoluted and arbitrary decisions about what they are doing with the domain (i.e. how they're generating and measuring performance on their dataset), I don't think it should be considered legitimate publishable research until the model is checked in some sane manner. At this point in time AI research is so saturated with hype and BS, it needs some sort of adversarial process to be taken seriously.
carapace 7y ago
See also "Deep Algebra" (sorry no link handy at the moment) where they are trying to train networks to extract or generate new math from old; input is arxiv algebra papers (LaTeX, PDF) IIRC.
twotwotwo 7y ago
The potentially interesting thing here, to me, is using networks to short-circuit searches that could grow explosively with expression size, but then filter down to answers that can be shown correct. That's also a way to get some value out of a system that doesn't always produce the correct answer as its first guess. In some cases it may be easy to prove the correctness once you have the proposed answer, but in others the network might need to produce intermediate steps or some kind of 'argument' to let the CAS check correctness in reasonable time. Perhaps do that by instrumenting a CAS to output intermediate steps and train the network on that, not just problem/answer pairs. Broadly, humans who have seen a lot of problems solved can say "this looks like a situation where you could try X" and do X without going down all the blind alleys that a CAS might. So it doesn't seem implausible that automated learned models might also outperform the heuristics CASes have hard-coded in for making those kinds of guesses. (You can imagine closer coupling, e.g. a CAS that calls out to an NN to propose solutions to certain hard-to-solve-but-easy-to-check subproblems, or uses learned models to try to guess the right branch to go down in a solution process that already looks like searching a tree of possibilities. But the more you have to crack open the CAS, the less appealing the whole thing becomes.)
- 7373737373 7y ago
  I wonder how much of this intuition can be formalized, if, say, the number of deduction steps from a theorem to another can be provably reliably approximated before attempting its proof. https://math.stackexchange.com/questions/3299096/resource-metalogic-proving-that-a-theorem-can-not-be-deduced-from-given-axiom https://math.stackexchange.com/questions/3299096/resource-me... https://math.stackexchange.com/questions/3477810/estimating-meta-mathematical-properties-of-conjectures https://math.stackexchange.com/questions/3477810/estimating-...
sarosh 7y ago
Actual paper is at https://arxiv.org/pdf/1912.01412.pdf https://arxiv.org/pdf/1912.01412.pdf

101 points by robinhouston 7y ago

Previous discussion: https://news.ycombinator.com/item?id=21084748 https://news.ycombinator.com/item?id=21084748 I think the point in the comments about Mathematica et al just being more careful about the domain is pretty damning of the claim the neural net beats them.

boyadjian 7y ago

Now, we can really talk about AI.

whatshisface 7y ago

Solving "advanced mathematics equations," as opposed to advanced English literature equations?

dragonwriter 7y ago
More likely as opposed to advanced chemical or logic or ... equations. “Mathematical” is a meaningful modifier, not a frivolous one, for “equation”.

xvilka 7y ago

There is CoqHammer[1] and ProverBot[2] for going even further - proving the theorems. [1] https://github.com/lukaszcz/coqhammer https://github.com/lukaszcz/coqhammer [2] https://github.com/UCSD-PL/proverbot9001 https://github.com/UCSD-PL/proverbot9001

haskellandchill 7y ago

> Facebook AI has built the first AI system that can solve advanced mathematics equations using symbolic reasoning Uh, this isn't true. Even their paper cites previous work. I guess it's PR speak. A little disappointing that it just guesses solutions and doesn't offer proofs.

mdswanson 7y ago

"First, we developed a process that effectively unpacks equations, laying them out in a branching, treelike structure..." Umm...like an expression tree, perhaps? https://www.geeksforgeeks.org/expression-tree/ https://www.geeksforgeeks.org/expression-tree/

laxd 7y ago
They call it an expression-tree syntax two paragraphs down.
- mdswanson 7y ago
  Congratulations! They re-invented it: "...our expression-tree syntax..."

lvh 7y ago

It seems bananas to me that Mathematica and other existing CASes can't solve that first sample equation: it reads like a straightforward integration, taking just a parameter substitution and an inverse trig derivative (which I feel like everyone doing calculus knows by heart?). Maybe I should go do it on paper and I'm missing the hard part?

nimish 7y ago
The risch algorithm is not trivial to implement.
- lvh 7y ago
  Sure, but this is Mathematica, the self-proclaimed leading mathematics package!
pfedak 7y ago
That surprised me too. I found that Mathematica could solve it if you give it the denominator as 1-u^2 for the eventual substitution. Perhaps it just doesn't try very hard to look for substitutions? I could believe it not giving a lot of "coverage" per time spent compared to more advanced techniques.

thanatropism 7y ago

I wonder if there is research on using deep learning for stuff like SAT solvers.

brtanymore 7y ago
SAT may be a game with rules too simple for DL approaches to outperform state-of-the-art traditional solvers right now, but SMT (Satisfiability modulo theories) is another story: https://papers.nips.cc/paper/8233-learning-to-solve-smt-formulas.pdf https://papers.nips.cc/paper/8233-learning-to-solve-smt-form...

m3kw9 7y ago

Would this be more like calculus where you plug in a range of numbers to get to a target?

gambler 7y ago

This paper makes so many convoluted and arbitrary decisions about what they are doing with the domain (i.e. how they're generating and measuring performance on their dataset), I don't think it should be considered legitimate publishable research until the model is checked in some sane manner. At this point in time AI research is so saturated with hype and BS, it needs some sort of adversarial process to be taken seriously.

carapace 7y ago

See also "Deep Algebra" (sorry no link handy at the moment) where they are trying to train networks to extract or generate new math from old; input is arxiv algebra papers (LaTeX, PDF) IIRC.

twotwotwo 7y ago

The potentially interesting thing here, to me, is using networks to short-circuit searches that could grow explosively with expression size, but then filter down to answers that can be shown correct. That's also a way to get some value out of a system that doesn't always produce the correct answer as its first guess. In some cases it may be easy to prove the correctness once you have the proposed answer, but in others the network might need to produce intermediate steps or some kind of 'argument' to let the CAS check correctness in reasonable time. Perhaps do that by instrumenting a CAS to output intermediate steps and train the network on that, not just problem/answer pairs. Broadly, humans who have seen a lot of problems solved can say "this looks like a situation where you could try X" and do X without going down all the blind alleys that a CAS might. So it doesn't seem implausible that automated learned models might also outperform the heuristics CASes have hard-coded in for making those kinds of guesses. (You can imagine closer coupling, e.g. a CAS that calls out to an NN to propose solutions to certain hard-to-solve-but-easy-to-check subproblems, or uses learned models to try to guess the right branch to go down in a solution process that already looks like searching a tree of possibilities. But the more you have to crack open the CAS, the less appealing the whole thing becomes.)

7373737373 7y ago
I wonder how much of this intuition can be formalized, if, say, the number of deduction steps from a theorem to another can be provably reliably approximated before attempting its proof. https://math.stackexchange.com/questions/3299096/resource-metalogic-proving-that-a-theorem-can-not-be-deduced-from-given-axiom https://math.stackexchange.com/questions/3299096/resource-me... https://math.stackexchange.com/questions/3477810/estimating-meta-mathematical-properties-of-conjectures https://math.stackexchange.com/questions/3477810/estimating-...

sarosh 7y ago

Actual paper is at https://arxiv.org/pdf/1912.01412.pdf https://arxiv.org/pdf/1912.01412.pdf