Theorem proving with modern ML

Vlad’s references

1. Neural Meta-Induction and Program Synthesis
   • arxiv
   • microsoft
2. DeepMath - continuous representations of symbolic expressions arxiv
3. Terpret- A language for program Induction arxiv
4. End to End differentiable proving arxiv
5. Alemi et al., “Deepmath - Deep sequence models for premise selection”. NIPS 2016. arxiv, research@google.
6. Kaliszyk, Chollet, Szegedy., “HolStep: A machine learning dataset for higher-order logic theorem proving”. ICLR 2017. arxiv,research@google
7. Alemi et al., “Deep variational information bottleneck”. ICLR 2017. arxiv
8. Loos et al., “Deep network guided proof search”. LPAR 2017. arxiv, research@google.
9. Learning to Discover Efficient Mathematical Identities arxiv

Game plan

• Skim over.
• Understand one theorem prover deeply (ex. HOL), interfacing with it.