Elamur Research⌕
☰
home / papers / 2020 / IsarStep: a Benchmark for High-level Mathematical Reasoning

IsarStep: a Benchmark for High-level Mathematical Reasoning

Paper · 2020 · Wenda Li, Lei Yu, Yuhuai Wu et al.

Summary

Most neural work on mathematical reasoning has targeted narrow, synthetic problems such as arithmetic or symbolic integration, which use very small vocabularies. IsarStep tests whether models can handle real proofs at undergraduate and research level. The authors mined the Archive of Formal Proofs (AFP) and the Isabelle/HOL standard library, which together hold about 204K machine-checked lemmas. Most of these proofs are written in a declarative style that reads much like human prose. From them the authors built a task: given the facts around a proof step, generate the missing intermediate proposition. Those facts are the premises leading into the step and the later result it supports, plus optional library lemmas found by Sledgehammer. Terms become token sequences, with types removed and free variables renamed systematically to keep the vocabulary small. The task is treated as seq2seq generation. The authors compare an attention-based RNN and a transformer with their new hierarchical transformer (HAT). HAT first encodes each proposition separately and then models how the propositions relate. The models solve about 15–25% of test problems, and HAT performs best. Analysis indicates they capture genuine relations between concepts. The benchmark is a step toward automatically sketching readable proofs and helping theorem provers search more efficiently.

Key points

  • The data comes from the AFP (143K lemmas) plus the Isabelle/HOL library, about 204K lemmas in total. Topics range from Gödel's incompleteness theorems and the Prime Number Theorem to cryptography and data structures.
  • Mining produced about 1.2M raw examples. After length filtering and deduplication, the split is 820K training, 5,000 validation and 5,000 test examples, with a vocabulary of 29,759 tokens.
  • Each example has five parts (F.1–F.5): the target proposition, the local facts used to derive it, a consequence derived from it, other supporting facts, and optional library lemmas as hints.
  • Normalising free variables cut the vocabulary by about one third without changing meaning. Removing unneeded parentheses further shortens the sequences.
  • In a Sledgehammer-based check on 4,908 test examples, HAT produced 1,125 exact matches. Few of these filled gaps that the prover could not already bridge, so the gains in automation were small. HAT also proposed some valid alternative steps, one of which exposed a redundant derivation in the Isabelle library.

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

🎓University of CambridgeCambridge · United Kingdom287 works · 125,174 citations🎓University of TorontoToronto · Canada121 works · 179,943 citations🏢Google DeepMindLondon · United Kingdom82 works · 84,829 citations

 Fields, topics and concepts

📚 Shelves 5The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 worksComputational Theory and Mathematics · 496 works

🧭 Topics 2Research subjects and languages the work is about.Reasoning · 1,948 worksEvaluation & benchmarks · 1,394 works

Cite

Cite as Wenda Li, Lei Yu, Yuhuai Wu and Lawrence C. Paulson. 2020. IsarStep: a Benchmark for High-level Mathematical Reasoning. arXiv:2006.09265.

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

@misc{li2020isarstep,
  title = {{IsarStep: a Benchmark for High-level Mathematical Reasoning}},
  author = {Wenda Li, Lei Yu, Yuhuai Wu and Lawrence C. Paulson},
  year = {2020},
  doi = {10.48550/arxiv.2006.09265},
  eprint = {2006.09265},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2006.09265}
}

References

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

  1. Alexander A. Alemi, François Chollet, Niklas Eén, Geoffrey Irving, Christian Szegedy, and Josef Urban. DeepMath - Deep Sequence Models for Premise Selection. In Proceedings of NeurIPS, 2016.
  2. Dzmitry Bahdanau, Kyunghyun Cho, and Yoshua Bengio. Neural machine translation by jointly learning to align and translate. In Proceedings of ICLR, 2015.
  3. Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In Proceedings of ICML, 2019. — HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  4. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C Paulson. Extending Sledgehammer with SMT solvers. In Proceedings of International Conference on Automated Deduction, 2011. find
  5. Chad E Brown, Bartosz Piotrowski, and Josef Urban. Learning to advise an equational prover. 2020a. URL http://aitp-conference.org/2020/abstract/paper_32.pdf. ↗
  6. Tom B Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, et al. Language models are few-shot learners. arXiv preprint arXiv:2005.14165, 2020b.
  7. François Charton, Amaury Hayat, and Guillaume Lample. Deep differential system stability - learning advanced computations from examples. CoRR, abs/2006.06462, 2020.
  8. Richard Evans, David Saxton, David Amos, Pushmeet Kohli, and Edward Grefenstette. Can neural networks understand logical entailment? In Proceedings of ICLR, 2018.
  9. Bernd Finkbeiner, Christopher Hahn, Markus N Rabe, and Frederik Schmitt. Teaching temporal logics to neural networks. arXiv preprint arXiv:2003.04218, 2020.
  10. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Initial experiments with statistical conjecturing over large formal corpora. In Joint Proceedings of the FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics, 2016. find
  11. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to Reason with HOL4 Tactics. In Proceedings of International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2017. find
  12. Jonas Gehring, Michael Auli, David Grangier, Denis Yarats, and Yann N. Dauphin. Convolutional sequence to sequence learning. In Proceedings of ICML, 2017.
  13. Zarathustra Goertzel and Josef Urban. Usefulness of lemmas via graph neural networks. URL http://aitp-conference.org/2019/abstract/AITP_2019_paper_32.pdf. Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. Journal of Formalized Reasoning, 3(2):153–245, 2010. ↗
  14. Sepp Hochreiter and Jürgen Schmidhuber. Long short-term memory. Neural computation, 9(8): 1735–1780, 1997. find
  15. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. GamePad: A Learning Environment for Theorem Proving. In Proceedings of ICLR, 2019.
  16. Lukasz Kaiser and Ilya Sutskever. Neural gpus learn algorithms. In Proceedings of ICLR, 2016. find
  17. Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A Machine Learning Dataset for Higher-order Logic Theorem Proving. In Proceedings of ICLR, 2017.
  18. Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In Proceedings of ICLR, 2020.
  19. Chin-Yew Lin. Rouge: A package for automatic evaluation of summaries. In Text summarization branches out, pp. 74–81, 2004.
  20. Wang Ling, Dani Yogatama, Chris Dyer, and Phil Blunsom. Program induction by rationale generation: Learning to solve and explain algebraic word problems. In Proceedings of ACL, 2017. find
  21. Yang Liu and Mirella Lapata. Hierarchical transformers for multi-document summarization. In Proceedings of ACL, 2019.
  22. Yutaka Nagashima. Simple dataset for proof method recommendation in isabelle/hol. In International Conference on Intelligent Computer Mathematics, 2020. find
  23. Yutaka Nagashima and Yilun He. Pamper: Proof method recommendation system for isabelle/hol. CoRR, 2018. URL http://arxiv.org/abs/1806.07239. ↗
  24. Yutaka Nagashima and Julian Parsert. Goal-oriented conjecturing for isabelle/hol, 2018. find
  25. Aditya Paliwal, Sarah Loos, Markus Rabe, Kshitij Bansal, and Christian Szegedy. Graph Representations for Higher-Order Logic and Theorem Proving, 2019. URL http://arxiv.org/abs/1905.10006. ↗
  26. Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. Bleu: a method for automatic evaluation of machine translation. In Proceedings of ACL, 2002.
  27. Lawrence C Paulson. Isabelle: A generic theorem prover, volume 828. Springer Science & Business Media, 1994. find
  28. Bartosz Piotrowski and Josef Urban. Guiding inferences in connection tableau by recurrent neural networks. In International Conference on Intelligent Computer Mathematics, pp. 309–314. Springer, 2020.
  29. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  30. Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757, 2020.
  31. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. OpenAI Blog, 1(8):9, 2019. find
  32. Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. Generating Correctness Proofs with Neural Networks, 2019. URL http://arxiv.org/abs/1907.07794. ↗
  33. David Saxton, Edward Grefenstette, Felix Hill, and Pushmeet Kohli. Analysing mathematical reasoning abilities of neural models. In Proceedings of ICLR, 2019.
  34. Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Christoph Benzmüller and Bruce Miller (eds.), Intelligent Computer Mathematics, 2020. find
  35. Andrew Trask, Felix Hill, Scott E. Reed, Jack W. Rae, Chris Dyer, and Phil Blunsom. Neural arithmetic logic units. In Proceedings of NeurIPS, 2018. find
  36. Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In Christoph Benzmüller and Bruce R. Miller (eds.), Intelligent Computer Mathematics, 2020.
  37. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Proceedings of NeurIPS, 2017.
  38. Mingzhe Wang and Jia Deng. Learning to Prove Theorems by Learning to Generate Theorems, 2020. URL https://arxiv.org/abs/2002.07019. ↗
  39. Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. Exploration of neural machine translation in autoformalization of mathematics in mizar. Proceedings of ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020.
  40. Makarius Wenzel. The Isabelle/Isar Implementation. https://isabelle.in.tum.de/dist/Isabelle2020/doc/isar-ref.pdf, 2020. [Online; accessed 31-May-2020]. ↗
  41. Freek Wiedijk. The seventeen provers of the world: Foreword by Dana S. Scott, volume 3600. Springer, 2006. find
  42. Yonghui Wu, Mike Schuster, Zhifeng Chen, Quoc V. Le, Mohammad Norouzi, Wolfgang Macherey, Maxim Krikun, Yuan Cao, Qin Gao, Klaus Macherey, Jeff Klingner, Apurva Shah, Melvin Johnson, Xiaobing Liu, Lukasz Kaiser, Stephan Gouws, Yoshikiyo Kato, Taku Kudo, Hideto Kazawa, Keith Stevens, George Kurian, N… find
  43. Yuhuai Wu, Albert Jiang, Jimmy Ba, and Roger Grosse. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. arXiv preprint arXiv:2007.02924, 2020.
  44. Table 3: Additional results. Top-1 Acc. Model Base +F.5 Conv2Conv 8.7 8.3 Kaiyu Yang and Jia Deng. Learning to Prove Theorems via Interacting with Proof Assistants. In Proceedings of ICML, 2019.
  45. Zichao Yang, Diyi Yang, Chris Dyer, Xiaodong He, Alexander J. Smola, and Eduard H. Hovy. Hierarchical attention networks for document classification. In Kevin Knight, Ani Nenkova, and Owen Rambow (eds.), Proceedings of NAACL HLT, 2016.
  46. Wojciech Zaremba and Ilya Sutskever. Learning to execute. arXiv preprint arXiv:1410.4615, 2014. find
  47. Xingxing Zhang, Furu Wei, and Ming Zhou. HIBERT: document level pre-training of hierarchical bidirectional transformers for document summarization. In Proceedings of ACL, 2019.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/li-2020-isarstep-benchmark-high-level-mathematical/