Here is a thread in paper references demonstrating that current deep learning, especially transformers are amazingly powerful for symbol manipulation already:
@GuillaumeLample, @f_charton
arxiv.org/abs/1912.01412
Solving hard integrals using deep transformers
🧵1/n
@GuillaumeLample, @f_charton
arxiv.org/abs/1912.01412
Solving hard integrals using deep transformers
🧵1/n
https://twitter.com/Plinz/status/1502337713315274760
A paper of my team at google, improving reasoning in large theories using contrastive learning for premise selection:
arxiv.org/abs/1606.04442
arxiv.org/abs/1606.04442
Another paper by Sarah Loos by our team on improving superposition based first order logic theorem provers using deep learning:
arxiv.org/abs/1701.06972
3/n
arxiv.org/abs/1701.06972
3/n
A paper by Dennis Lee et al (from our team) demonstrating that latent representation of formulas can be used to perform long chains of non-trivial reasoning purely using vectors:
arxiv.org/abs/1909.11851
arxiv.org/abs/1909.11851
One of the first papers that demonstrates the most tasks relevant for high level mathematics can be trained in an unsupervised manner from existing mathematical formulas, including conjecturing and finding missing proof steps:
arxiv.org/abs/2006.04757
arxiv.org/abs/2006.04757
Again, previously unimaginable, transformers can generate long satifying traces of LTL formulas, by Christopher Hahn et al
openreview.net/forum?id=dOcQK…
openreview.net/forum?id=dOcQK…
A complete HOL theorem prover based purely on RL and GNNs, solves over 60% of all of HOL Light library fully automatically.
This dataset contains a lot graduate level mathematics.
Some proofs are significantly more elegant than their human counterparts.
arxiv.org/abs/1905.10006
This dataset contains a lot graduate level mathematics.
Some proofs are significantly more elegant than their human counterparts.
arxiv.org/abs/1905.10006
Improving lean automated theorem proving by unsupervised training of transformers on intermediate proof terms:
arxiv.org/abs/2102.06203
arxiv.org/abs/2102.06203
Full-blown state-of-the-art first order logic theorem proving by DeepMind, trained using a lot of synthetic data and hindsight experience replay:
arxiv.org/abs/2103.03798
arxiv.org/abs/2103.03798
Solving mathematics problems given in natural language using GPT-transformers and a lot of manual prompt engineering:
arxiv.org/abs/2111.08267
arxiv.org/abs/2111.08267
• • •
Missing some Tweet in this thread? You can try to
force a refresh
