Using neural networks to solve advanced mathematics equations

Previous discussion: 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.

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

There is CoqHammer[1] and ProverBot[2] for going even further - proving the theorems.

[1] https://github.com/lukaszcz/coqhammer

[2] https://github.com/UCSD-PL/proverbot9001

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.

> 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.

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?

"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/

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

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.

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

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

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

Now, we can really talk about AI.