Did someone train a LLM on the set.mm

[Marcel Richter]

I had a lot of fun training transformers on some toy data, and now i am thinking what to do next. I was surprised how fast even small transformers lern long multiplication. 

Anyone know if someone trained a GTP on set.mm yet.

set.mm is only ~40mb, i guess that is not enough to avoid overfitting really fast. Anyone produced some procedural generated metamath code?

I belive a well trained model could be of great help as some kind of methamath copilote.

Have a nice day :D

[Amaury Hayat]

Hi Marcel,

There were actually several papers based on Transformers for Metamath. You can probably check these two and the reference therein and it will give you a good idea of what was done and what can be achieved (up to last year) :)

https://arxiv.org/abs/2009.03393

https://arxiv.org/abs/2205.11491

For transformers learning more or less complicated specific maths notions (ODE, stability of ODEs, equilibrium in graphs, linear algebra, etc.) you can check for instance https://arxiv.org/abs/1912.01412 (learning to solve ODEs), https://arxiv.org/abs/2006.06462 (learning to predict advance properties such as stability, controllability, etc.),  https://arxiv.org/abs/2112.03588 (learning to find equilibrium in graphs), https://arxiv.org/abs/2112.01898 (learning linear algebra). There are probably many other references but these can give you a good start and their models and dataset are public.

Best,

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1fe3d510-bd01-4097-8d04-6d4baac1f696n%40googlegroups.com.

[David A. Wheeler]

The set.mm repo has a small set of Wiki pages.
I've been putting notes about automated proving, especially AI/ML, here:
https://github.com/metamath/set.mm/wiki/Automated-proving

I hope to someday work on AI/ML for creating Metamath proofs, but I haven't
had a chance to do it. I encourage anyone interested to give it a try, I think it's
*extremely* promising.

--- David A. Wheeler

> To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAP92Bfkp3sWACxYbBnK%2Bz9Ah%3DOt4fw8cvewU2VnJKgSr99STeQ%40mail.gmail.com.