deep learning for symbolic mathematics

Stream: general

[Tim Daly]

Lample Guillaume and Charton, Francois "Deep Learning for Symbolic Mathematics" (https://arxiv.org/pdf/1912.01412.pdf

[Tim Daly]

I didn't think this was possible and I was wrong. Now the question is, can similar techniques apply to Lean? They did have the advantage that they could generate large datasets because they could generate a random equation, differentiate it, and then know that the integral exists. I'm not sure how to generate "random" proofs.

[Tim Daly]

Their technique of Integerate(Diff(f(x),x)) also generates a lot of random test cases (fuzzing) useful for debugging. So if there was a similar hack for Lean then one could build a fuzz tester for Lean.

The only thing I can think of is there is the idea of "generate all proofs of length N" (usually used for the idea of exhaustive search). I don't know how to generate proofs of length N though.

[Simon Cruanes]

If you consider the set of rules of some sequent calculus (like HOL's kernel), you can use them bottom-to-top as generators as if they were prolog rules, I think.
From

$\cfrac{\Gamma, A \vdash B}{\Gamma \vdash A \Rightarrow B}$

you can start with a formula $\varphi$ and unify it with

$A \Rightarrow B$

and recursively unify $A$ and $B$ with the conclusions of other rules?
I know it's doable at least for generating terms with ML-style polymorphic types, I've used that in the past for quickcheck stuff.

For Lean you'd run the refiner "in reverse", in a similar way.

[Tim Daly]

In the paper they create a tree structure by moving the "operator" to the prefix position (e.g. 2 + 3 becomes (+ 2 3). So A \Rightarrow B becomes (\Rightarrow A B) in their generator. It should be possible to create a generator using that tree-method.

[Tim Daly]

The next hack would be to have a set of tactics that were exactly the rules in Lean. Then, when you generate a theorem (in the forward direction by creating a proof tree) you can look at the theorem and apply the tactics to reconstruct the proof. Since you know the theorem is true, and you know the tactics cover the set of rules used to generate the proof, Lean should be able to (automatically?) prove the theorem.
Maybe. Possibly.

[Tim Daly]

Once you have a large enough training set then perhaps Lample and Charton can run their ML program on it and "learn" to prove.

[Bryan Gin-ge Chen]

There's an interesting discussion on the paper of Lample and Charton in this sage-devel thread: https://groups.google.com/forum/#!topic/sage-devel/eXMbHpG3_oY

It links to a "review" by Ernest Davis on the arxiv: https://arxiv.org/abs/1912.05752 and this blog post by Brent Baccala (featuring Axiom!): https://www.freesoft.org/blogs/soapbox/the-facebook-integral/

[Jason Rute]

As for the integration paper, I think it is fascinating, but as others have pointed out, one needs to take the results with a some skepticism. However, competing with highly engineered and optimized CAS systems will be a hard challenge. I think the results are encouraging and they could have applications in speeding up and extending CAS systems.

I think a more interesting application to this technique would be to find a mathematical domain (less studied than integration) where one direction of the problem is easy and the reverse direction is hard (but still someone with a lot of experience could often figure out the reverse answer from intuition, memory, and light reasoning), and verifying that the answer in the reverse direction is correct is fairly easy in practice. It is possible that techniques like this could have a huge benefit. However, I'm struggling to find good examples.

As for using this on theorem proving, that would fit my description above (maybe), but it also seems like a particular challenging problem to expect an end-to-end sequence-to-sequence model to just work on anything but trivial cases. (However, it might still be worth giving it a try!) On a more techincal level, tactic proofs are not unique. For example, by simp is the proof of a number of different goals. Even by refl is not unique (but is quite common). I haven't thought about it too much, but maybe some subset of the term language would suffice. Of course, one could also try this out in other proof languages besides Lean where proofs uniquely specify their theorems (or where synthetic proofs can at least be easily generated from rules/axioms). (Metamath, cut-free sequent calculi, hilbert-style deduction, tableau calculus)

Setting aside this exact method of Lample and Charton, I could also imagine generating synthetic proofs could be an important part of a synthetic method to train machine learning provers, especially combined with reinforcement learning. Already the DeepHOL/HOList work and this Metamath AI augment their training data with synthetically generated theorems/proofs. I could imagine an advanced system which has one agent whose goal is to generate realistic looking synthetic theorems/proofs which are then fed to another agent for training on them.

[Johan Commelin]

I think a more interesting application to this technique would be to find a mathematical domain (less studied than integration) where one direction of the problem is easy and the reverse direction is hard (but still someone with a lot of experience could often figure out the reverse answer from intuition, memory, and light reasoning), and verifying that the answer in the reverse direction is correct is fairly easy in practice. It is possible that techniques like this could have a huge benefit. However, I'm struggling to find good examples.

Factoring numbers or polynomials?

[Tim Daly]

Wow. I go away for a week and somebody finds Axiom in the wild. Sweet. I have been reviewing that paper and using their ideas for fuzz testing.

[Tim Daly]

@Jason Rute You might find Axiom's Computer Algebra Test Suite (http://axiom-developer.org/axiom-website/CATS/index.html) which I've been constructing from publications.

[Tim Daly]

Wow. I watched those videos showing Facebook vs Axiom vs Sage. What a masterful presentation!

Axiom's Risch algorithm is (I believe) the most complete implementation although there is still much to do. The algorithm was the work of Barry Trager and Manuel Bronstein.

The take-away for Lean is that there are 2 branches of computational mathematics, proof systems and computer algebra. The computer algebra branch is fairly deep in several areas. Axiom uses group theory as scaffold to build algorithms like Risch. Lean also uses group theory as an underlying structure. I hope it will be possible to unify these two branches of computational mathematics so one can compute with trusted algorithms.

[Tim Daly]

The second video on the Risch Algorithm is deeply related to Algebraic Geometry.

[Johan Commelin]

@Tim Daly I have no clue what you mean with "Lean also uses group theory as an underlying structure".