Elamur Research⌕
☰
home / papers / 2020 / Learning to Prove Theorems by Learning to Generate Theorems

Learning to Prove Theorems by Learning to Generate Theorems

Paper · 2020 · Mingzhe Wang and Jia Deng

Summary

Neural theorem provers usually learn by imitating human-written formal proofs. Such data is scarce because formalizing mathematics requires rare expertise and a lot of time. Wang and Deng address this bottleneck by adding machine-made training examples. They introduce MetaGen, a learnable generator for the Metamath language. It builds new theorems by applying substitution steps to existing ones, so every output comes with a guaranteed-correct proof. To make the synthetic data resemble human mathematics, the generator is trained in one of two ways. When human proofs are available, it learns to replay their steps in the forward direction. When only theorem statements exist, it uses reinforcement learning, with a GAN-style discriminator rating how human-like each generated theorem looks. The synthetic proofs then train Holophrasm, a neural Metamath prover. On the iset.mm and set.mm knowledge bases, provers using the extra data consistently prove more test theorems than provers trained on human proofs alone. This suggests that generated data can partly replace costly manual formalization.

Key points

  • Up to 1M unique synthetic theorems were generated for iset.mm. For set.mm, the authors generated 300K (no human proofs), 1M (10% of human proofs) and 10M (full human proof set) theorems.
  • With 10% of human proofs on set.mm, adding synthetic data proves 472 theorems. Doubling the human proofs instead proves 476.
  • The authors' GPU re-implementation of Holophrasm proves 557 theorems with all human proofs. Removing "trivial" proof steps from the relevance-network training data raises the count from 574 to 600.
  • Learned generators beat both the random baseline MetaGen-Rand and a tf-idf/language-model ablation. They improve the relevance metrics (top-k, MRR) and the substitution-network metrics.
  • The best prover solves 22.06% of set.mm test theorems, versus 29.22% reported by Polu & Sutskever (2020). The authors note the setups differ: 27,218 proofs versus about 38k, and a 5-minute time limit per run.

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

🎓Princeton UniversityPrinceton · United States137 works · 53,849 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

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

Cite

Cite as Mingzhe Wang and Jia Deng. 2020. Learning to Prove Theorems by Learning to Generate Theorems. arXiv:2002.07019.

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

@misc{wang2020learning,
  title = {{Learning to Prove Theorems by Learning to Generate Theorems}},
  author = {Mingzhe Wang and Jia Deng},
  year = {2020},
  doi = {10.48550/arxiv.2002.07019},
  eprint = {2002.07019},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2002.07019}
}

References

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

  1. Balunovic, M., Bielik, P., and Vechev, M. Learning to solve smt formulas. In Advances in Neural Information Processing Systems, pp. 10317–10328, 2018. find
  2. Bansal, K., Loos, S., Rabe, M., Szegedy, C., and Wilcox, S. Holist: An environment for machine learning of higher order logic theorem proving. In International Conference on Machine Learning, pp. 454–463, 2019a. — HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  3. Bansal, K., Loos, S. M., Rabe, M. N., and Szegedy, C. Learning to reason in large theories without imitation. arXiv preprint arXiv:1905.10501, 2019b.
  4. Bertot, Y. and Castéran, P. Coq’art: the calculus of inductive constructions, 2004. find
  5. Chvalovskỳ, K., Gauthier, T., and Urban, J. First experiments with data driven conjecturing. 4th Conference on Artificial Intelligence and Theorem Proving, 2019. find
  6. Colton, S. Automated theory formation in pure mathematics. Springer Science & Business Media, 2012. find
  7. Darvas, Á., Hähnle, R., and Sands, D. A theorem proving approach to analysis of secure information flow. In International Conference on Security in Pervasive Computing, pp. 193–209. Springer, 2005. find
  8. Durugkar, I. and Stone, P. Adversarial goal generation for intrinsic motivation. In Thirty-Second AAAI Conference on Artificial Intelligence, 2018. find
  9. Fawzi, A., Malinowski, M., Fawzi, H., and Fawzi, O. Learning dynamic polynomial proofs. In Advances in Neural Information Processing Systems, pp. 4181–4190, 2019. find
  10. Florensa, C., Held, D., Geng, X., and Abbeel, P. Automatic goal generation for reinforcement learning agents. In Dy, J. and Krause, A. (eds.), Proceedings of the 35th International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp. 1515–1528, Stockholmsmässan,…
  11. Gauthier, T., Kaliszyk, C., and Urban, J. Tactictoe: Learning to reason with hol4 tactics. arXiv preprint arXiv:1804.00595, 2018. find
  12. Goodfellow, I., Pouget-Abadie, J., Mirza, M., Xu, B., Warde-Farley, D., Ozair, S., Courville, A., and Bengio, Y. Generative adversarial nets. In Advances in neural information processing systems, pp. 2672–2680, 2014.
  13. Gu, R., Shao, Z., Chen, H., Wu, X. N., Kim, J., Sjöberg, V., and Costanzo, D. Certikos: An extensible architecture for building certified concurrent {OS} kernels. In 12th {USENIX} Symposium on Operating Systems Design and Implementation ({OSDI} 16), pp. 653–669, 2016. find
  14. Harrison, J. HOL Light: An overview. In Berghofer, S., Nipkow, T., Urban, C., and Wenzel, M. (eds.), Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science, pp. 60–66, Munich, Germany, 2009. Springer-V… find
  15. Huang, D. On learning to prove. arXiv preprint arXiv:1904.11099, 2019. — [arXiv:1904.11099](https://arxiv.org/abs/1904.11099) find
  16. Irving, G., Szegedy, C., Alemi, A. A., Eén, N., Chollet, F., and Urban, J. Deepmath-deep sequence models for premise selection. In Advances in Neural Information Processing Systems, pp. 2235– 2243, 2016.
  17. Jakubův, J. and Urban, J. arXiv:1904.01677, 2019. — [arXiv:1904.01677](https://arxiv.org/abs/1904.01677) find
  18. Hammering mizar by learning clause guidance. Kaliszyk, C. and Urban, J. Learning-assisted theorem proving with millions of lemmas. Journal of symbolic computation, 69:109–128, 2015. find
  19. Kaliszyk, C., Urban, J., and Vyskočil, J. Machine learner for automated reasoning 0.4 and 0.5. arXiv preprint arXiv:1402.2359, 2014. — [arXiv:1402.2359](https://arxiv.org/abs/1402.2359) find
  20. Kaliszyk, C., Urban, J., and Vyskočil, J. Lemmatization for stronger reasoning in large theories. In International Symposium on Frontiers of Combining Systems, pp. 341–356. Springer, 2015. find
  21. Kaliszyk, C., Urban, J., Michalewski, H., and Olšák, M. Reinforcement learning of theorem proving. In Advances in Neural Information Processing Systems, pp. 8822–8833, 2018.
  22. Kern, C. and Greenstreet, M. R. Formal verification in hardware design: a survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), 4(2):123–193, 1999. find
  23. Kingma, D. P. and Ba, J. arXiv:1412.6980, 2014.
  24. Adam: A method for stochastic optimization. Kocsis, L. and Szepesvári, C. Bandit based monte-carlo planning. In European conference on machine learning, pp. 282–293. Springer, 2006. find
  25. Lee, D., Szegedy, C., Rabe, M. N., Loos, S. M., and Bansal, K. Mathematical reasoning in latent space. arXiv preprint arXiv:1909.11851, 2019.
  26. Loos, S., Irving, G., Szegedy, C., and Kaliszyk, C. Deep network guided proof search. arXiv preprint arXiv:1701.06972, 2017.
  27. Megill, N. and Wheeler, D. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina, 2019. http://us.metamath.org/downloads/metamath.pdf. ↗
  28. Paliwal, A., Loos, S., Rabe, M., Bansal, K., and Szegedy, C. Graph representations for higher-order logic and theorem proving. arXiv preprint arXiv:1905.10006, 2019.
  29. Piotrowski, B. and Urban, J. Atpboost: Learning premise selection in binary setting with atp feedback. In International Joint Conference on Automated Reasoning, pp. 566–574. Springer, 2018. find
  30. Polu, S. and Sutskever, I. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  31. Schulz, S. E–a brainiac theorem prover. Ai Communications, 15(2, 3):111–126, 2002. find
  32. Slind, K. and Norrish, M. A brief overview of hol4. In International Conference on Theorem Proving in Higher Order Logics, pp. 28–32. Springer, 2008. find
  33. Sukhbaatar, S., Lin, Z., Kostrikov, I., Synnaeve, G., Szlam, A., and Fergus, R. Intrinsic motivation and automatic curricula via asymmetric self-play. arXiv preprint arXiv:1703.05407, 2017. find
  34. Sukhbaatar, S., Denton, E., Szlam, A., and Fergus, R. Learning goal embeddings via self-play for hierarchical reinforcement learning. arXiv preprint arXiv:1811.09083, 2018. — [arXiv:1811.09083](https://arxiv.org/abs/1811.09083) find
  35. Urban, J. Mptp–motivation, implementation, first experiments. Journal of Automated Reasoning, 33 (3-4):319–339, 2004. find
  36. Urban, J. and Jakubův, J. First neural conjecturing datasets and experiments. arXiv preprint arXiv:2005.14664, 2020.
  37. Urban, J., Sutcliffe, G., Pudlák, P., and Vyskočil, J. Malarea sg1-machine learner for automated reasoning with semantic guidance. In International Joint Conference on Automated Reasoning, pp. 441–456. Springer, 2008. arXiv preprint arXiv preprint Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J.…
  38. Whalen, D. Holophrasm: a neural automated theorem prover for higher-order logic. arXiv preprint arXiv:1608.02644, 2016.
  39. Wiedijk, F. Formal proof sketches. In International Workshop on Types for Proofs and Programs, pp. 378–393. Springer, 2003. find
  40. Wiedijk, F. Formalizing 100 theorems. http://www.cs.ru.nl/~freek/100/, 2019. ↗
  41. Williams, R. J. Simple statistical gradient-following algorithms for connectionist reinforcement learning. Machine learning, 8(3-4):229–256, 1992. find
  42. Yang, K. and Deng, J. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning, 2019.
  43. Zombori, Z., Csiszárik, A., Michalewski, H., Kaliszyk, C., and Urban, J. Towards finding longer proofs. arXiv preprint arXiv:1905.13100, 2019.

Updated

↑ back to top

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