Elamur Research⌕
☰
home / papers / 2021 / LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning

LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning

Paper · 2021 · Yuhuai Wu, Markus Rabe, Wenda Li et al.

Summary

The paper asks whether the inductive bias needed for mathematical reasoning can be taught to a generic transformer through data rather than through specialized architectures. The authors draw on Charles Peirce's three primitives of reasoning: deduction, induction, and abduction. In Peirce's framing, these correspond to inferring a Result, a Rule, or a Case from the other two. The authors build one synthetic task for each primitive. The tasks deliberately contain no mathematical content, so a model can only pick up reasoning patterns from them.

Transformers are briefly pretrained on these tasks (LIME) and then fine-tuned on four formal-mathematics benchmarks. Only the inner layers are transferred. Input embeddings and the output layer are dropped, so one pretrained model can serve tasks with entirely different vocabularies.

LIME-pretrained models clearly beat transformers trained from scratch on all four benchmarks. The pretraining costs only a small share of the downstream training compute. This matters because formal mathematics has little data available for large-scale pretraining. It also shows that pretraining can help by instilling biases, not just by supplying knowledge.

Key points

  • The benchmarks are IsarStep, HOList Skip-tree, MetaMathStep, and LeanStep. Top-1 accuracy on IsarStep rose from 20.4% to 26.9% (LIME Mix), and on LeanStep from 15.5% to 29.8%.
  • Pretraining takes roughly two hours on one GPU. By comparison, GPT-f-style language-model pretraining dominates the total compute budget.
  • Loading the vocabulary embeddings and output weights as well gave about the same result on IsarStep (26.7% top-1). This supports the claim that what transfers is inductive bias rather than token-level knowledge.
  • Pretraining on MetaMathStep cost about 40× more than LIME Mix and helped IsarStep less. WMT translation pretraining actually hurt performance.
  • LIME Abduct gave LSTMs only small gains (5.5→6.9% top-1; with attention, 12.3→13.4%), compared with 20.4→26.7% for transformers. The authors attribute this gap to the flexibility of self-attention. The generator code is available at github.com/tonywu95/LIME.

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🎓University of CambridgeCambridge · United Kingdom287 works · 125,174 citations🎓University of TorontoToronto · Canada121 works · 179,943 citations🔬Vector InstituteToronto · Canada41 works · 5,820 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 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Yuhuai Wu, Markus Rabe, Wenda Li, Jimmy Ba, Roger Grosse and Christian Szegedy. 2021. LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning. arXiv:2101.06223.

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

@misc{wu2021lime,
  title = {{LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning}},
  author = {Yuhuai Wu, Markus Rabe, Wenda Li, Jimmy Ba, Roger Grosse and Christian Szegedy},
  year = {2021},
  doi = {10.48550/arxiv.2101.06223},
  eprint = {2101.06223},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2101.06223}
}

References

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

  1. Bansal, K., Loos, S. M., Rabe, M. N., Szegedy, C., and Wilcox, S. HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In 36th International Conference on Machine Learning, ICML 2019, Long Beach, California, USA, June 9-15, 2019. URL http://proceedings.mlr.press/ v97/ba… ↗
  2. Bansal, K., Szegedy, C., Rabe, M. N., Loos, S. M., and Toman, V. Learning to Reason in Large Theories without Imitation. arXiv preprint arXiv:1905.10501, 2019.
  3. Bellucci, F. and Pietarinen, A.-V. Charles Sanders Peirce: Logic. In The Internet Encyclopedia of Philosophy, 2015. URL https://iep.utm.edu/peir-log/. ↗
  4. Brown, T. B., Mann, B., Ryder, N., Subbiah, M., Kaplan, J., Dhariwal, P., Neelakantan, A., Shyam, P., Sastry, G., Askell, A., Agarwal, S., Herbert-Voss, A., Krueger, G., Henighan, T., Child, R., Ramesh, A., Ziegler, D. M., Wu, J., Winter, C., Hesse, C., Chen, M., Sigler, E., Litwin, M., Gray, S., Ch… — Language Models are Few-Shot Learners
  5. Buzzard, K., Hughes, C., Lau, K., Livingston, A., Mir, R. F., and Morrison, S. Schemes in lean. arXiv preprint arXiv:2101.02602, 2019. — [arXiv:2101.02602](https://arxiv.org/abs/2101.02602) find
  6. Buzzard, K., Commelin, J., and Massot, P. Formalising perfectoid spaces. In Blanchette, J. and Hritcu, C. (eds.), Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pp. 299–312.
  7. ACM, 2020. doi: 10. 1145/3372885.3373830. URL https://doi.org/ 10.1145/3372885.3373830. — Formalising perfectoid spaces
  8. Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, pp. 378–388. find
  9. Springer, 2015. doi: 10.1007/978-3-319-21401-6\\_26. URL https://doi.org/10.1007/978-3-319-21401-6_26. — [doi:10.1007/978-3-319-21401-6\\_26](https://doi.org/10.1007/978-3-319-21401-6_26) ↗
  10. Devlin, J., Chang, M., Lee, K., and Toutanova, K. BERT: pre-training of deep bidirectional transformers for language understanding. In Burstein, J., Doran, C., and Solorio, T. (eds.), Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: H…
  11. Dong, L., Yang, N., Wang, W., Wei, F., Liu, X., Wang, Y., Gao, J., Zhou, M., and Hon, H. Unified Language Model Pre-training for Natural Language Understanding and Generation. In Advances in Neural Information Processing Systems, NeurIPS 2019, Vancouver, BC, Canada, December 8-14, 2019, pp. 13063–13…
  12. Evans, R., Saxton, D., Amos, D., Kohli, P., and Grefenstette, E. Can Neural Networks Understand Logical Entailment? In International Conference on Learning Representations, 2018. URL https://openreview.net/forum? id=SkZxCk-0Z. ↗
  13. Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., and Norrish, M. TacticToe: Learning to Prove with Tactics. Journal of Automated Reasoning, pp. 1–30, 2020.
  14. Hahn, C., Schmitt, F., Kreber, J. U., Rabe, M. N., and Finkbeiner, B. Transformers Generalize to the Semantics of Logics. arXiv preprint arXiv:2003.04218, 2020.
  15. Han, J. M. Enhancing SAT solvers with glue variable predictions. arXiv preprint arXiv:2007.02559, 2020. find
  16. Han, J. M. and van Doorn, F. A formal proof of the inde-Conneau, A. and Lample, G. Cross-lingual Language pendence of the continuum hypothesis. In Blanchette, J. Model Pretraining. In Advances in Neural Informa-and Hritcu, C. (eds.), Proceedings of the 9th ACM SIG-tion Processing Systems, NeurIPS 20… find
  17. ACM, 2020. doi: 10. 8928-cross-lingual-language-model-pretraining. 1145/3372885.3373826. URL https://doi.org/ Crouse, M., Abdelaziz, I., Cornelio, C., Thost, V., Wu, L., 10.1145/3372885.3373826. Forbus, K., and Fokoue, A. Improving Graph Neural Net-Han, J. M., Rute, J., Wu, Y., Ayers, E. W., and Pol… — [doi:10.1145/3372885.3373826](https://doi.org/10.1145/3372885.3373826) find
  18. Hellendoorn, V. J., Sutton, C., Singh, R., Maniatis, P., and Bieber, D. Global relational models of source code. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020. find
  19. OpenReview.net, 2020. URL https://openreview.net/forum?id=B1lnbRNtwr. ↗
  20. Hochreiter, S. and Schmidhuber, J. Long Short-Term Memory. Neural computation, 9(8):1735–1780, 1997. find
  21. Huang, D., Dhariwal, P., Song, D., and Sutskever, I. GamePad: A learning environment for theorem proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019.
  22. OpenReview.net, 2019. URL https://openreview.net/forum?id=r1xwKoR9Y7. ↗
  23. Joshi, M., Chen, D., Liu, Y., Weld, D. S., Zettlemoyer, L., and Levy, O. Spanbert: Improving pre-training by representing and predicting spans. 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_00300. ↗
  24. Kingma, D. P. and Ba, J. Adam: A method for stochastic optimization. In Bengio, Y. and LeCun, Y. (eds.), 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, 2015. URL http://arxiv.org/abs/1412.6980. ↗
  25. Lample, G. and Charton, F. Deep learning for 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. ↗
  27. LeCun, Y., Haffner, P., Bottou, L., and Bengio, Y. Object recognition with gradient-based learning. In Shape, Contour and Grouping in Computer Vision, pp. 319, Berlin, Heidelberg, 1999. Springer-Verlag. ISBN 3540667229. find
  28. Lederman, G., Rabe, M., Seshia, S., and Lee, E. A. Learning heuristics for quantified boolean formulas through reinforcement learning. In International Conference on Learning Representations, 2020. find
  29. Li, W., Yu, L., Wu, Y., and Paulson, L. C. Isarstep: a benchmark for high-level mathematical reasoning. In International Conference on Learning Representations, 2021. URL https://openreview.net/forum? id=Pzj6fzU6wkj. ↗
  30. Liu, Y., Ott, M., Goyal, N., Du, J., Joshi, M., Chen, D., Levy, O., Lewis, M., Zettlemoyer, L., and Stoyanov, V. Roberta: A robustly optimized BERT pretraining approach. CoRR, abs/1907.11692, 2019. URL http://arxiv.org/ abs/1907.11692. ↗
  31. Luong, T., Pham, H., and Manning, C. D. Effective approaches to attention-based neural machine translation. In Màrquez, L., Callison-Burch, C., Su, J., Pighin, D., and Marton, Y. (eds.), Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, EMNLP 2015, Lisbon, Portu…
  32. ACM, 2020. doi: 10. 1145/3372885.3373824. URL https://doi.org/ 10.1145/3372885.3373824. — The Lean mathematical library
  33. McCoy, R. T., Grant, E., Smolensky, P., Griffiths, T., and Linzen, T. Universal linguistic inductive biases via meta-learning. Proceedings of CogSci, abs/2006.16324, 2020. — [arXiv:2006.16324](https://arxiv.org/abs/2006.16324) find
  34. Ott, M., Edunov, S., Baevski, A., Fan, A., Gross, S., Ng, N., Grangier, D., and Auli, M. fairseq: A fast, extensible toolkit for sequence modeling. In Ammar, W., Louis, A., and Mostafazadeh, N. (eds.), Proceedings of the 2019 Conference of the North American Chapter of the Association for Computatio…
  35. Paliwal, A., Loos, S. M., Rabe, M. N., Bansal, K., and Szegedy, C. Graph representations for higher-order logic and theorem proving. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020,…
  36. AAAI Press, 2020. URL https://aaai.org/ ojs/index.php/AAAI/article/view/5689. ↗
  37. Papadimitriou, I. and Jurafsky, D. Learning Music Helps You Read: Using transfer to study linguistic structure in language models. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pp. 6829–6839, Online, November 2020. Association for Computational Li… find
  38. Peirce, C. S. Reasoning and the logic of things: The Cambridge conferences lectures of 1898. find
  39. Harvard University Press, 1992. find
  40. Piotrowski, B. and Urban, J. Guiding Inferences in Connection Tableau by Recurrent Neural Networks. In Benzmüller, C. and Miller, B. (eds.), Intelligent Computer Mathematics, pp. 309–314, Cham, 2020. Springer International Publishing. ISBN 978-3-030-53518-6.
  41. Polu, S. and Sutskever, I. Generative Language Modeling for Automated Theorem Proving. CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009. 03393. ↗
  42. Rabe, M. N., Lee, D., Bansal, K., and Szegedy, C. Mathematical Reasoning via Self-supervised Skip-tree Training. In International Conference on Learning Representations, 2021. URL https://openreview.net/forum? id=YmqAnY0CMEy. ↗
  43. Radford, A., Wu, J., Child, R., Luan, D., Amodei, D., and Sutskever, I. 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. ↗
  44. Raffel, C., Shazeer, N., Roberts, A., Lee, K., Narang, S., Matena, M., Zhou, Y., Li, W., and Liu, P. J. Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer. J. Mach. Learn. Res., 21:140:1– 140:67, 2020. URL http://jmlr.org/papers/ v21/20-074.html. ↗
  45. Saxton, D., Grefenstette, E., Hill, F., and Kohli, P. Analysing mathematical reasoning abilities of neural models. In Proceedings of International Conference on Learning Representations (ICLR), 2019.
  46. Scarselli, F., Gori, M., Tsoi, A. C., Hagenbuchner, M., and Monfardini, G. The graph neural network model. IEEE Transactions on Neural Networks, 20(1):61–80, 2008. find
  47. Schlag, I., Smolensky, P., Fernandez, R., Jojic, N., Schmidhuber, J., and Gao, J. Enhancing the transformer with explicit relational encoding for math problem solving. CoRR, abs/1910.06611, 2019. URL http://arxiv.org/abs/1910.06611. — [arXiv:1910.06611](https://arxiv.org/abs/1910.06611) ↗
  48. Scholze, P. Liquid tensor experiment. https://xenaproject.wordpress.com/2020/ 12/05/liquid-tensor-experiment/, 2020. Formalization available at https://github.com/ leanprover-community/lean-liquid. ↗
  49. Selsam, D. and Bjørner, N. Guiding High-Performance SAT solvers with Unsat-Core Predictions. In International Conference on Theory and Applications of Satisfiability Testing, pp. 336–353. Springer, 2019.
  50. Selsam, D., Lamm, M., Bünz, B., Liang, P., de Moura, L., and Dill, D. L. Learning a SAT solver from single-bit supervision. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019.
  51. OpenReview.net, 2019. URL https://openreview.net/forum?id=HJMC_iA5tm. ↗
  52. Song, K., Tan, X., Qin, T., Lu, J., and Liu, T. MASS: masked sequence to sequence pre-training for language generation. In 36th International Conference on Machine Learning, ICML 2019, Long Beach, California, USA, June 9-15, 2019, 2019. URL http://proceedings.mlr.press/v97/song19d.html. ↗
  53. Szegedy, C., Vanhoucke, V., Ioffe, S., Shlens, J., and Wojna, Z. Rethinking the inception architecture for computer vision. In Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 2818–2826, 2016. find
  54. Urban, J. and Jakubův, J. First Neural Conjecturing Datasets and Experiments. In Benzmüller, C. and Miller, B. (eds.), Intelligent Computer Mathematics, pp. 315–323, Cham, 2020. Springer International Publishing. ISBN 978-3-030-53518-6.
  55. Vaezipoor, P., Lederman, G., Wu, Y., Maddison, C. J., Grosse, R. B., Lee, E. A., Seshia, S. A., and Bacchus, F. Learning Branching Heuristics for Propositional Model Counting. In AAAI 2021, 2021. find
  56. Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A. N., Kaiser, L., and Polosukhin, I. Attention is All you Need. In Proceedings of Advances in Neural Information Processing Systems (NeurIPS), 2017.
  57. Wang, M., Tang, Y., Wang, J., and Deng, J. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems, pp. 2786–2796, 2017.
  58. Wang, Q., Brown, C., Kaliszyk, C., and Urban, J. Exploration of neural machine translation in autoformalization of mathematics in mizar. Proceedings of ACM SIG-PLAN International Conference on Certified Programs and Proofs, 2020.
  59. Warstadt, A. and Bowman, S. R. Can neural networks acquire a structural bias from raw linguistic data? Proceedings of CogSci, 2020. find
  60. Wu, Y., Jiang, A., Ba, J., and Grosse, R. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. In International Conference on Learning Representations, 2021. URL https://openreview.net/forum?id=O6LPudowNQm. ↗
  61. Xu, K., Li, J., Zhang, M., Du, S. S., Kawarabayashi, K.-i., and Jegelka, S. What can neural networks reason about? In ICLR 2020, 2020. find
  62. Yang, K. and Deng, J. Learning to Prove Theorems via Interacting with Proof Assistants. In Proceedings of International Conference on Machine Learning (ICML), 2019.
  63. Yang, Z., Dai, Z., Yang, Y., Carbonell, J., Salakhutdinov, R. R., and Le, Q. V. Xlnet: Generalized autoregressive pretraining for language understanding. In Advances in Neural Information Processing Systems, NeurIPS 2019, Vancouver, BC, Canada, December 8-14, 2019, 2019.
  64. Zhang, J., Zhao, Y., Saleh, M., and Liu, P. J. PEGASUS: pre-training with extracted gap-sentences for abstractive summarization. In 37th International Conference on Machine Learning, ICML 2020, Vienna, Austria, 2020, volume 119.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wu-2021-lime-learning-inductive-bias-primitives/