--- title: "Mathematical Reasoning via Self-supervised Skip-tree Training" description: "They propose skip-tree training, a variant of skip-sequence pretraining that respects the syntax tree of… 39 references, cited by 30 papers here." authors: ["Markus N. Rabe", "Dennis Lee", "Kshitij Bansal", "Christian Szegedy"] year: 2020 venue: "arXiv:2006.04757" source: "https://arxiv.org/abs/2006.04757" doi: "10.48550/arxiv.2006.04757" arxiv: "2006.04757" licence: "arXiv — non-exclusive licence to distribute" licence_url: "https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html" summary_licence: "Elamur Cosmic License" canonical: "https://research.elamur.ai/free/en/papers/rabe-2020-mathematical-reasoning-self-supervised-skip/" --- [Elamur Research](https://md.research.elamur.ai/free/en/) · [this page in HTML](https://research.elamur.ai/free/en/papers/rabe-2020-mathematical-reasoning-self-supervised-skip/) [home](https://md.research.elamur.ai/free/en/) / [papers](https://md.research.elamur.ai/free/en/papers/) / [2020](https://md.research.elamur.ai/free/en/papers/2020/page/6/) / Mathematical Reasoning via Self-supervised Skip-tree Training # Mathematical Reasoning via Self-supervised Skip-tree Training **Authors:** [Markus N. Rabe](https://md.research.elamur.ai/free/en/authors/markus-n-rabe/), [Dennis Lee](https://md.research.elamur.ai/free/en/authors/dennis-lee/), [Kshitij Bansal](https://md.research.elamur.ai/free/en/authors/kshitij-bansal/) and [Christian Szegedy](https://md.research.elamur.ai/free/en/authors/christian-szegedy/) · **Year:** 2020 · **Venue:** arXiv:2006.04757 · **Licence:** [arXiv — non-exclusive licence to distribute](https://arxiv.org/licenses/nonexclusive-distrib/1.0/license.html) **Links:** [Publisher's page](https://arxiv.org/abs/2006.04757) · [PDF](https://arxiv.org/pdf/2006.04757v3) · [DOI 10.48550/arxiv.2006.04757](https://doi.org/10.48550/arxiv.2006.04757) · [arXiv 2006.04757](https://arxiv.org/abs/2006.04757) · [OpenAlex](https://openalex.org/W3126568801) **Citations:** 24 citations (OpenAlex, 2026-10-14) · [30](https://md.research.elamur.ai/free/en/papers/rabe-2020-mathematical-reasoning-self-supervised-skip/cited-by/) in our library, of the 149,439 papers whose bibliographies we read ## Summary The paper asks whether a Transformer can acquire logical reasoning in formal mathematics from self-supervised language modeling alone, without labeled reasoning data or task-specific fine-tuning. The authors use the HOList corpus of HOL Light theorems and intermediate proof goals, written as S-expressions. They propose skip-tree training, a variant of skip-sequence pretraining that respects the syntax tree of formulas. One whole subexpression is replaced by a \ token for the model to reconstruct, and a few other subexpressions are hidden with \ tokens to make the task harder. The models are evaluated directly, with no fine-tuning, on new reasoning tasks: type inference, proposing missing assumptions, completing equalities, and free-form conjecturing. Skip-tree models clearly beat skip-sequence baselines. Because the domain is formal, predictions that differ from the ground truth can still be checked with the DeepHOL prover. Many of these predictions turn out to be provable and even helpful in other proofs. This suggests that language-model pretraining could support automated theorem proving and the generation of new conjectures. ## Key points - **Data:** The "core" and "complex" parts of HOList contain 18,943 theorems, 637 definitions and 603,950 proof steps. Only the training split (proofs of 11,655 theorems) is used for training, and evaluation tasks come from validation theorems only. - **Setup:** The encoder input is capped at 1024 tokens and the decoder output at 512. Besides the \ target, k = 2 extra subexpressions are masked, with every occurrence replaced by \. - **Provability (Table 3, uniform / weighted skip-tree, provable / provable-and-new):** - Assumptions: about 32% provable, about 26–27% provable and new. - Equalities: about 18–20% provable, about 12% provable and new. - Free-form conjecturing: 82.32% and 97.75% provable, but only 12.70% and 0.59% new. - All of these are lower bounds, since DeepHOL proves only about 58% of validation theorems. - **Usefulness:** Provable conjectures were added to the theorem database and tested in DeepHOL reinforcement learning runs, with over 200,000 proofs per run. The share used as a premise was: - 3,445 of 3,857 from the assumptions task - 979 of 3,440 from the equalities task - 49 of 130 from free-form conjecturing - **Notable conjecture:** The vector identity b = a + c ⇒ a = b − c was used 1,728 times. Humans had only ever stated it as a local lemma, so it filled a gap in the theorem database. *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 - [Google](https://md.research.elamur.ai/free/en/companies/google/) — Company, Mountain View, United States · 533 works · 443,885 citations - [University of California, Berkeley](https://md.research.elamur.ai/free/en/universities/university-of-california-berkeley/) — University, Berkeley, United States · 243 works · 251,774 citations 📚 Shelves (5): [🖥️ Computer Science](https://md.research.elamur.ai/free/en/shelves/computer-science/) · 19,503 works · [🤖 Artificial Intelligence](https://md.research.elamur.ai/free/en/shelves/computer-science/artificial-intelligence/) · 18,805 works · [🎭 Arts and Humanities](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/) · 17,959 works · [🗣️ Language and Linguistics](https://md.research.elamur.ai/free/en/shelves/arts-and-humanities/language-and-linguistics/) · 17,789 works · [🧮 Computational Theory and Mathematics](https://md.research.elamur.ai/free/en/shelves/computer-science/computational-theory-and-mathematics/) · 496 works 🧭 Topics (2): [🧠 Language models & pretraining](https://md.research.elamur.ai/free/en/topics/language-models/) · 4,145 works · [🧮 Reasoning](https://md.research.elamur.ai/free/en/topics/reasoning/) · 1,948 works ## Cite Cite as: Markus N. Rabe, Dennis Lee, Kshitij Bansal and Christian Szegedy. 2020. Mathematical Reasoning via Self-supervised Skip-tree Training. arXiv:2006.04757. The paper itself, not this page. BibTeX from the library's record of the work. ```bibtex @misc{rabe2020mathematical, title = {{Mathematical Reasoning via Self-supervised Skip-tree Training}}, author = {Markus N. Rabe, Dennis Lee, Kshitij Bansal and Christian Szegedy}, year = {2020}, doi = {10.48550/arxiv.2006.04757}, eprint = {2006.04757}, archivePrefix = {arXiv}, url = {https://doi.org/10.48550/arxiv.2006.04757} } ``` - [← previous Harnessing the linguistic signal to predict scalar inferences](https://md.research.elamur.ai/free/en/papers/schuster-2020-harnessing-linguistic-signal-predict-scalar/) - [next → A Graph-based Model for Joint Chinese Word Segmentation and Dependency Parsing](https://md.research.elamur.ai/free/en/papers/yan-2020-graph-based-model-joint-chinese/) - [↑ back to papers of 2020](https://md.research.elamur.ai/free/en/papers/2020/page/6/) ## References 39 references, 21 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet. 1. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. [Attention is all you need](https://md.research.elamur.ai/free/en/papers/vaswani-2017-attention-all-need/). In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett, editors, Advances in Ne… 2. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. In OpenAI Blog, 2018. URL [https://d4mucfpksywv.cloudfront.net/better-language-models/language_models_are_unsupervised_multitask_learners.pdf](https://d4mucfpksywv.cloudfront.net/better-language-models/language_models_are_unsupervised_multitask_learners.pdf). [↗](https://d4mucfpksywv.cloudfront.net/better-language-models/language_models_are_unsupervised_multitask_learners.pdf) 3. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. [BERT: Pre-training of deep bidirectional transformers for language understanding](https://md.research.elamur.ai/free/en/papers/devlin-2019-bert-pre-training-deep-bidirectional/). In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volum… 4. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter,… — [Language Models are Few-Shot Learners](https://md.research.elamur.ai/free/en/papers/brown-2020-language-models-few-shot-learners/) 5. Kshitij Bansal, Sarah M Loos, Markus N Rabe, Christian Szegedy, and Stewart Wilcox. [HOList: An environment for machine learning of higher-order theorem proving](https://md.research.elamur.ai/free/en/papers/bansal-2019-holist-environment-machine-learning-higher/). In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9… 6. PMLR, 2019. URL [http://proceedings.mlr.press/v97/bansal19a/bansal19a.pdf](http://proceedings.mlr.press/v97/bansal19a/bansal19a.pdf). [↗](http://proceedings.mlr.press/v97/bansal19a/bansal19a.pdf) 7. John Harrison. HOL Light: A tutorial introduction. In Mandayam K. Srivas and Albert John Camilleri, editors, Formal Methods in Computer-Aided Design, First International Conference, FMCAD ’96, Palo Alto, California, USA, November 6-8, 1996, Proceedings, volume 1166 of Lecture Notes in Computer Scien… [find](https://scholar.google.com/scholar?q=John+Harrison%2E+HOL+Light%3A+A+tutorial+introduction%2E+In+Mandayam+K%2E+Srivas+and+Albert+John+Camilleri%2C+editors%2C+Formal+Methods+in+Computer%2DAided+Design%2C+First+International+Conference%2C+FMCAD+%E2%80%9996%2C+Palo+Al) 8. Springer, 1996. URL https://doi.org/10.1007/BFb0031795. — [doi:10.1007/bfb0031795](https://doi.org/10.1007/bfb0031795) [↗](https://doi.org/10.1007/BFb0031795) 9. Jingqing Zhang, Yao Zhao, Mohammad Saleh, and Peter J. Liu. [PEGASUS: pre-training with extracted gap-sentences for abstractive summarization](https://md.research.elamur.ai/free/en/papers/zhang-2019-pegasus-pre-training-extracted-gap/). CoRR, abs/1912.08777, 2019. URL http://arxiv.org/abs/1912.08777. [↗](http://arxiv.org/abs/1912.08777) 10. Kaitao Song, Xu Tan, Tao Qin, Jianfeng Lu, and Tie-Yan Liu. [MASS: masked sequence to sequence pre-training for language generation](https://md.research.elamur.ai/free/en/papers/song-2019-mass-masked-sequence-sequence-pre/). In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, Ca… 11. PMLR, 2019. URL [http://proceedings.mlr.press/v97/song19d.html](http://proceedings.mlr.press/v97/song19d.html). [↗](http://proceedings.mlr.press/v97/song19d.html) 12. Li Dong, Nan Yang, Wenhui Wang, Furu Wei, Xiaodong Liu, Yu Wang, Jianfeng Gao, Ming Zhou, and Hsiao-Wuen Hon. [Unified language model pre-training for natural language understanding and generation](https://md.research.elamur.ai/free/en/papers/dong-2019-unified-language-model-pre-training/). In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman… 13. Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J. Liu. [Exploring the limits of transfer learning with a unified text-to-text transformer](https://md.research.elamur.ai/free/en/papers/raffel-2019-exploring-limits-transfer-learning-unified/). CoRR, abs/1910.10683, 2019. URL http://arxiv.org/abs/1910.10683. [↗](http://arxiv.org/abs/1910.10683) 14. Alexis Conneau and Guillaume Lample. Cross-lingual language model pretraining. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Proces… [find](https://scholar.google.com/scholar?q=Alexis+Conneau+and+Guillaume+Lample%2E+Cross%2Dlingual+language+model+pretraining%2E+In+Hanna+M%2E+Wallach%2C+Hugo+Larochelle%2C+Alina+Beygelzimer%2C+Florence+d%E2%80%99Alch%C3%A9%2DBuc%2C+Emily+B%2E+Fox%2C+and+Roman+Garnett%2C+editors%2C+) 15. Mandar Joshi, Danqi Chen, Yinhan Liu, Daniel S. Weld, Luke Zettlemoyer, and Omer Levy. [Spanbert: Improving pre-training by representing and predicting spans](https://md.research.elamur.ai/free/en/papers/joshi-2019-spanbert-improving-pre-training-representing/). Transactions of the Association for Computational Linguistics, 8:64–77, 2020. doi: 10.1162/tacl\\_a\\_00300. URL https://doi. org/10.1162/tacl_a… 16. Chin-Yew Lin. [ROUGE: A package for automatic evaluation of summaries](https://md.research.elamur.ai/free/en/papers/lin-2004-rouge-package-automatic-evaluation-summaries/). In Text Summarization Branches Out, pages 74–81, Barcelona, Spain, July 2004. Association for Computational Linguistics. URL [https://www.aclweb.org/anthology/W04-1013](https://www.aclweb.org/anthology/W04-1013). [↗](https://www.aclweb.org/anthology/W04-1013) 17. Cezary Kaliszyk and Josef Urban. [Learning-assisted automated reasoning with flyspeck](https://md.research.elamur.ai/free/en/papers/kaliszyk-2012-learning-assisted-automated-reasoning-flyspeck/). Journal of Automated Reasoning, 53(2):173–213, 2014. 18. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. TacticToe: Learning to reason with HOL4 tactics. 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 EPiC Se… [find](https://scholar.google.com/scholar?q=Thibault+Gauthier%2C+Cezary+Kaliszyk%2C+and+Josef+Urban%2E+TacticToe%3A+Learning+to+reason+with+HOL4+tactics%2E+In+Thomas+Eiter+and+David+Sands%2C+editors%2C+LPAR%2D21%2C+21st+International+Conference+on+Logic+for+Prog) 19. EasyChair, 2017. URL [https://easychair.org/publications/volume/LPAR-21](https://easychair.org/publications/volume/LPAR-21). [↗](https://easychair.org/publications/volume/LPAR-21) 20. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. [GamePad: A learning environment for theorem proving](https://md.research.elamur.ai/free/en/papers/huang-2018-gamepad-learning-environment-theorem-proving/). In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. 21. OpenReview.net, 2019. URL [https://openreview.net/forum?id=r1xwKoR9Y7](https://openreview.net/forum?id=r1xwKoR9Y7). [↗](https://openreview.net/forum?id=r1xwKoR9Y7) 22. Kaiyu Yang and Jia Deng. [Learning to prove theorems via interacting with proof assistants](https://md.research.elamur.ai/free/en/papers/yang-2019-learning-prove-theorems-interacting-proof/). 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… 23. PMLR, 2019. URL [http://proceedings.mlr.press/v97/yang19a/yang19a.pdf](http://proceedings.mlr.press/v97/yang19a/yang19a.pdf). [↗](http://proceedings.mlr.press/v97/yang19a/yang19a.pdf) 24. Alex Sanchez-Stern, Yousef Alhessi, Lawrence Saul, and Sorin Lerner. [Generating correctness proofs with neural networks](https://md.research.elamur.ai/free/en/papers/stern-2019-generating-correctness-proofs-neural-networks/). CoRR, abs/1907.07794, 2019. URL http://arxiv.org/abs/1907.07794. [↗](http://arxiv.org/abs/1907.07794) 25. Guillaume Lample and François Charton. [Deep learning for symbolic mathematics](https://md.research.elamur.ai/free/en/papers/lample-2019-deep-learning-symbolic-mathematics/). In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. 26. OpenReview.net, 2020. URL [https://openreview.net/forum?id=Ske31kBtPr](https://openreview.net/forum?id=Ske31kBtPr). [↗](https://openreview.net/forum?id=Ske31kBtPr) 27. Bernd Finkbeiner, Christopher Hahn, Markus N. Rabe, and Frederik Schmitt. [Teaching temporal logics to neural networks](https://md.research.elamur.ai/free/en/papers/hahn-2020-teaching-temporal-logics-neural-networks/). CoRR, abs/2003.04218, 2020. URL https://arxiv.org/abs/2003.04218. [↗](https://arxiv.org/abs/2003.04218) 28. Bartosz Piotrowski, Josef Urban, Chad E Brown, and Cezary Kaliszyk. Can neural networks learn symbolic rewriting? In Conference on Artificial Intelligence and Theorem Proving, 2019. [find](https://scholar.google.com/scholar?q=Bartosz+Piotrowski%2C+Josef+Urban%2C+Chad+E+Brown%2C+and+Cezary+Kaliszyk%2E+Can+neural+networks+learn+symbolic+rewriting%3F+In+Conference+on+Artificial+Intelligence+and+Theorem+Proving%2C+2019%2E) 29. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. [First experiments with neural translation of informal to formal mathematics](https://md.research.elamur.ai/free/en/papers/wang-2018-first-experiments-neural-translation-informal/). In International Conference on Intelligent Computer Mathematics, pages 255–270, 2018. 30. Qingxiang Wang, Chad Brown, Cezary Kaliszyk, and Josef Urban. [Exploration of neural machine translation in autoformalization of mathematics in Mizar](https://md.research.elamur.ai/free/en/papers/wang-2019-exploration-neural-machine-translation-autoformalization/). In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 85–98, 2020. 31. Guillaume Lample, Alexis Conneau, Ludovic Denoyer, and Marc’Aurelio Ranzato. [Unsupervised machine translation using monolingual corpora only](https://md.research.elamur.ai/free/en/papers/lample-2017-unsupervised-machine-translation-using-monolingual/). In International Conference on Learning Representations, 2018. 32. Josef Urban and Jan Jakubův. [First neural conjecturing datasets and experiments](https://md.research.elamur.ai/free/en/papers/urban-2020-first-neural-conjecturing-datasets-experiments/). In Conference on Intelligent Computer Mathematics, 2020. 33. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Initial experiments with statistical conjecturing over large formal corpora. In CICM 2016 - Work in Progress Proceedings 1785, pages 219–228, 2016. [find](https://scholar.google.com/scholar?q=Thibault+Gauthier%2C+Cezary+Kaliszyk%2C+and+Josef+Urban%2E+Initial+experiments+with+statistical+conjecturing+over+large+formal+corpora%2E+In+CICM+2016+%2D+Work+in+Progress+Proceedings+1785%2C+pages+219%E2%80%93228%2C+2016%2E) 34. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Modelling high-level mathematical reasoning in mechanised declarative proofs. In arXiv 2006.[09265, 2020](https://md.research.elamur.ai/free/en/papers/li-2020-isarstep-benchmark-high-level-mathematical/). 35. Vighnesh Leonardo Shiv and Chris Quirk. Novel positional encodings to enable tree-based transformers. In Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d’Alché-Buc, Emily B. Fox, and Roman Garnett, editors, Advances in Neural Information Processing Systems 32: Annual Conference on Ne… [find](https://scholar.google.com/scholar?q=Vighnesh+Leonardo+Shiv+and+Chris+Quirk%2E+Novel+positional+encodings+to+enable+tree%2Dbased+transformers%2E+In+Hanna+M%2E+Wallach%2C+Hugo+Larochelle%2C+Alina+Beygelzimer%2C+Florence+d%E2%80%99Alch%C3%A9%2DBuc%2C+Emily+B%2E+Fox%2C+and+R) 36. Vincent J. Hellendoorn, Charles Sutton, Rishabh Singh, Petros Maniatis, and David Bieber. Global relational models of source code. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. [find](https://scholar.google.com/scholar?q=Vincent+J%2E+Hellendoorn%2C+Charles+Sutton%2C+Rishabh+Singh%2C+Petros+Maniatis%2C+and+David+Bieber%2E+Global+relational+models+of+source+code%2E+In+8th+International+Conference+on+Learning+Representations%2C+ICLR+202) 37. OpenReview.net, 2020. URL [https://openreview.net/forum?id=B1lnbRNtwr](https://openreview.net/forum?id=B1lnbRNtwr). [↗](https://openreview.net/forum?id=B1lnbRNtwr) 38. Paul Cairns. Informalising formal mathematics: Searching the mizar library with latent semantics. In International Conference on Mathematical Knowledge Management, pages 58–72. Springer, 2004. [find](https://scholar.google.com/scholar?q=Paul+Cairns%2E+Informalising+formal+mathematics%3A+Searching+the+mizar+library+with+latent+semantics%2E+In+International+Conference+on+Mathematical+Knowledge+Management%2C+pages+58%E2%80%9372%2E+Springer%2C+2004%2E) 39. Josef Urban. Mptp–motivation, implementation, first experiments. Journal of Automated Reasoning, 33(3-4):319–339, 2004. [find](https://scholar.google.com/scholar?q=Josef+Urban%2E+Mptp%E2%80%93motivation%2C+implementation%2C+first+experiments%2E+Journal+of+Automated+Reasoning%2C+33%283%2D4%29%3A319%E2%80%93339%2C+2004%2E) *Updated 3 November 2026*