Elamur Research⌕
☰
home / papers / 2020 / Learning to Prove from Synthetic Theorems

Learning to Prove from Synthetic Theorems

Paper · 2020 · Eser Aygün, Zafarali Ahmed, Ankit Anand et al.

Summary

Deep learning for automated theorem proving is held back by the scarcity of human-written theorems and proofs. Aygün et al. (DeepMind) show that a prover can be trained without any human theorems or proofs. Their "forward proposer" (FwdP) starts from a domain's axioms, picks random resolution steps restricted to linear resolution, and turns the final derived clause into a conjecture that is guaranteed to be valid. A minimal saturation prover then attempts these synthetic problems. It uses clause weight as its cost function and θ-subsumption to remove redundant clauses. Each clause produced during a successful proof is labelled as used or unused in that proof. These labels train MLP and GNN models, which then serve as the prover's learned cost function. On human-written TPTP problems, the provers trained only on synthetic data solve a substantial share. In most axiom sets they beat counterparts trained on TPTP itself, and they generate fewer clauses during search. The work suggests a way to move theorem proving from scarce data to abundant data.

Key points

  • Ten equality-free axiom sets were taken from TPTP: FLD1–2, GEO6–9, GRP5, KRS1, NUM9 and SET1. They were filtered to at most 1000 axiom clauses and at least ten associated theorems.
  • The forward proposer was run for ten steps on each axiom set, producing 25,000 theorems for training and 1000 for validation. Unused clauses far outnumbered used ones, so they were subsampled to balance the classes.
  • The models predict whether a clause will appear in the final proof. They take two inputs: the candidate clause and the initial clause set, which acts as the goal.
  • Both the MLP and the GNN cost functions transfer to human-written TPTP theorems, and most axiom sets show gains over models trained on TPTP.
  • The approach has two limitations. The proposer cannot produce theorems whose conclusion needs more than one clause, and random generation yields mostly easy theorems. The authors suggest jointly training the proposer and prover with reinforcement learning and curriculum learning.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🏢GoogleMountain View · United States533 works · 443,885 citations

 Fields, topics and concepts

📚 Shelves 2The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Eser Aygün, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot, Laurent Orseau, Doina Precup and Shibl Mourad. 2020. Learning to Prove from Synthetic Theorems. arXiv:2006.11259.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2006.11259 · arXiv 2006.11259

@misc{aygun2020learning,
  title = {{Learning to Prove from Synthetic Theorems}},
  author = {Eser Aygün, Zafarali Ahmed, Ankit Anand, Vlad Firoiu, Xavier Glorot, Laurent Orseau, Doina Precup and Shibl Mourad},
  year = {2020},
  doi = {10.48550/arxiv.2006.11259},
  eprint = {2006.11259},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2006.11259}
}

References

35 references, 19 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Jimmy Lei Ba, Jamie Ryan Kiros, and Geoffrey E Hinton. Layer normalization. arXiv preprint arXiv:1607.06450, 2016.
  2. Peter Battaglia, Razvan Pascanu, Matthew Lai, Danilo Jimenez Rezende, et al. Interaction networks for learning about objects, relations and physics. In Advances in neural information processing systems, pages 4502–4510, 2016. find
  3. Koen Claessen, Reiner Hähnle, and Johan Mårtensson. Verification of hardware systems with first-order logic. In Proceedings of the CADE-18 Workshop-Problem and Problem Sets for ATP, number 02/10, 2002. find
  4. Maxwell Crouse, Spencer Whitehead, Ibrahim Abdelaziz, Bassem Makni, Cristina Cornelio, Pavan Kapanipathi, Edwin Pell, Kavitha Srinivas, Veronika Thost, Michael Witbrock, and Achille Fokoue. A deep reinforcement learning based approach to learning transferable proof guidance strategies. CoRR, abs/191… — [arXiv:1911.02065](https://arxiv.org/abs/1911.02065) find
  5. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: pre-training of deep bidirectional transformers for language understanding. In Jill Burstein, Christy Doran, and Thamar Solorio, editors, Proceedings of the 2019 Conference of the North American Chapter of the Association for Co…
  6. Melvin Fitting. First-order logic and automated theorem proving. Springer Science & Business Media, 2012. find
  7. Xavier Glorot, Ankit Anand, Eser Aygün, Shibl Mourad, Pushmeet Kohli, and Doina Precup. Learning representations of logical formulae using graph neural networks. 2019. find
  8. Reiner Hähnle. Tableaux and related methods. Handbook of automated reasoning, 1(101-176):4, 2001. find
  9. Kaiming He, Xiangyu Zhang, Shaoqing Ren, and Jian Sun. Deep residual learning for image recognition. In 2016 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2016, Las Vegas, NV, USA, June 27-30, 2016, pages 770–778.
  10. IEEE Computer Society, 2016. find
  11. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. Gamepad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019.
  12. Jan Jakubuv and Josef Urban. ENIGMA: efficient learning-based inference guiding machine. In Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings, volume 10383 of Lecture Notes in Computer Science, pages 292–302.
  13. Cezary Kaliszyk and Josef Urban. Mizar 40 for mizar 40. J. Autom. Reason., 55(3):245–256, October 2015.
  14. Cezary Kaliszyk, Francois Chollet, and Christian Szegedy. HolStep: a Machine Learning Dataset for Higher-Order Logic Theorem Proving. In International Conference on Learning Representations, ICLR, 2017.
  15. Cezary Kaliszyk, Josef Urban, Henryk Michalewski, and Miroslav Olšák. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems, pages 8822–8833, 2018.
  16. Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. arXiv preprint arXiv:1412.6980, 2014.
  17. Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020.
  18. Char-Tung Lee. A completeness theorem and computer program for finding theorems derivable from given axioms. PhD thesis, Department of Electrical Engineering and Computer Science, University of California, 1967. find
  19. Douglas B Lenat. Automated theory formation in mathematics. In IJCAI, volume 77, pages 833–842, 1977. find
  20. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In Thomas Eiter and David Sands, editors, LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPi…
  21. Norman D. Megill and David. A. Wheerler. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us.metamath.org/downloads/metamath.pdf. ↗
  22. Stephen Merity, Caiming Xiong, James Bradbury, and Richard Socher. Pointer sentinel mixture models. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings.
  23. Vinod Nair and Geoffrey E Hinton. Rectified linear units improve restricted boltzmann machines. In Proceedings of the 27th international conference on machine learning (ICML-10), pages 807–814, 2010. find
  24. Allen Newell and Herbert Simon. The logic theory machine–a complex information processing system. IRE Transactions on information theory, 2(3):61–79, 1956. — The logic theory machine: A complex information processing system
  25. G. D. Plotkin. A note on inductive generalization. In Machine Intelligence 5, pages 153–163. American Elsevier, 1970. find
  26. Alexandre Riazanov and Andrei Voronkov. The design and implementation of vampire. AI communications, 15(2, 3):91–110, 2002. find
  27. J. A. Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23–41, January 1965. find
  28. Olga Russakovsky, Jia Deng, Hao Su, Jonathan Krause, Sanjeev Satheesh, Sean Ma, Zhiheng Huang, Andrej Karpathy, Aditya Khosla, Michael Bernstein, Alexander C. Berg, and Li Fei-Fei. ImageNet Large Scale Visual Recognition Challenge. International Journal of Computer Vision (IJCV), 115(3):211–252, 201…
  29. Stephan Schulz, Simon Cruanes, and Petar Vukmirović. Faster, higher, stronger: E 2.3. In Pacal Fontaine, editor, Proc. of the 27th CADE, Natal, Brasil, number 11716 in LNAI, pages 495–507. Springer, 2019.
  30. David Silver, Aja Huang, Chris J. Maddison, Arthur Guez, Laurent Sifre, George van den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Vedavyas Panneershelvam, Marc Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, Ilya Sutskever, Timothy P. Lillicrap, Madeleine Leach, Koray… find
  31. G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017. find
  32. Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems. CoRR, abs/2002.07019, 2020.
  33. Johan Wittocx, Maarten Mariën, and Marc Denecker. Approximate reasoning in first-order logic theories. In KR, pages 103–112, 2008. find
  34. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings o…
  35. Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Towards finding longer proofs. CoRR, abs/1905.13100, 2019.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/aygun-2020-learning-prove-synthetic-theorems/