Elamur Research⌕
☰
home / papers / 2020 / INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving

INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving

Paper · 2020 · Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba et al.

Summary

Learning-based theorem provers struggle with two issues: formal proof corpora are small, and useful target theorems often differ substantially from those seen in training. The authors present INT, a synthetic benchmark of algebraic equalities and inequalities built from ordered field axioms. Its generator starts from a trivial statement and repeatedly transforms it according to a chosen sequence of axioms. This produces an unbounded supply of theorems with non-trivial proofs. Because the problem distribution can be adjusted along six axes, researchers can test specific kinds of out-of-distribution generalization. INT also includes a lightweight proof assistant with two interfaces: a sequence-based one that resembles LEAN's rewrite style, and a graph-based one that treats proving as manipulation of computation graphs. In baseline experiments, transformer agents usually achieved higher test success than GNN agents, even though their gaps between in-distribution and out-of-distribution performance were larger. Adding MCTS at test time improved the proving of unseen theorems. The work matters because it provides a controlled, low-cost testbed for studying generalization in learned theorem provers.

Key points

  • The generator morphs a core logic statement step by step, following an axiom order, and collects premises along the way. Each step yields a valid implication chain, so proofs are guaranteed to be long rather than trivially short.
  • The assistant averaged 1.28 ms per proof step, compared with 7.96 ms in HOL Light, a speedup of about 6.2× measured over 10,000 steps. Its trusted core is under 200 lines of code.
  • Baselines included transformers and GNNs. Transformers did better within the training distribution and in most absolute test scores, while GNNs degraded less when the test distribution shifted.
  • GPT-f (Polu & Sutskever, 2020) reused the INT generation method. Adding 1% synthetic theorems to its training data led to 2.3% more completed proofs on Metamath.
  • Code and generator: github.com/albertqjiang/INT

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 TorontoToronto · Canada121 works · 179,943 citations🎓University of OxfordOxford · United Kingdom138 works · 161,448 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 2Research subjects and languages the work is about.Reasoning · 1,948 worksEvaluation & benchmarks · 1,394 works

Cite

Cite as Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba and Roger Grosse. 2020. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. arXiv:2007.02924.

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

@misc{wu2020int,
  title = {{INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving}},
  author = {Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba and Roger Grosse},
  year = {2020},
  doi = {10.48550/arxiv.2007.02924},
  eprint = {2007.02924},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2007.02924}
}

References

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

  1. 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 Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference on Machine Learning, ICML… — HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  2. PMLR, 2019. URL http://proceedings.mlr.press/v97/bansal19a.html. ↗
  3. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Yann Coscoy, David Delahaye, Daniel de Rauglaudre, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, et al. The Coq proof assistant reference manual. INRIA, version, 6(11), 1999. find
  4. James P. Bridge, Sean B. Holden, and Lawrence C. Paulson. Machine learning for first-order theorem proving. Journal of automated reasoning, 53(2):141–172, 2014. find
  5. Hongshen Chen, Xiaorui Liu, Dawei Yin, and Jiliang Tang. A survey on dialogue systems: Recent advances and new frontiers. Acm Sigkdd Explorations Newsletter, 19(2):25–35, 2017. find
  6. Karel Chvalovskỳ, Thibault Gauthier, and Josef Urban. First experiments with data driven conjecturing. AITP 2019, 2019. URL http://aitp-conference.org/2019/abstract/AITP_2019_paper_27.pdf. ↗
  7. Simon Colton. Automated theory formation in pure mathematics. Springer Science & Business Media, 2012. find
  8. Ádám Darvas, Reiner Hähnle, and David Sands. A theorem proving approach to analysis of secure information flow. In International Conference on Security in Pervasive Computing, pages 193–209. Springer, 2005. find
  9. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In International Conference on Automated Deduction, pages 378–388. Springer, 2015. find
  10. Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Fei-Fei Li. Imagenet: A large-scale hierarchical image database. In 2009 IEEE Computer Society Conference on Computer Vision and Pattern Recognition (CVPR 2009), 20-25 June 2009, Miami, Florida, USA, pages 248–255. find
  11. IEEE Computer Society, 2009. doi: 10.1109/CVPR.2009.5206848. URL https://doi.org/10.1109/CVPR.2009.5206848. ↗
  12. David Steven Dummit and Richard M Foote. Abstract algebra, volume 3. Wiley Hoboken, 2004. find
  13. Siemion Fajtlowicz. On conjectures of graffiti. In Annals of Discrete Mathematics, volume 38, pages 113–118. Elsevier, 1988. find
  14. Matthias Fey and Jan Eric Lenssen. Fast graph representation learning with pytorch geometric. CoRR, abs/1903.02428, 2019. URL http://arxiv.org/abs/1903.02428. ↗
  15. Thibault Gauthier. Deep reinforcement learning in HOL4. CoRR, abs/1910.11797, 2019. URL http://arxiv.org/abs/1910.11797. ↗
  16. Thibault Gauthier. Deep reinforcement learning for synthesizing functions in higher-order logic. In Elvira Albert and Laura Kovács, editors, LPAR 2020: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Alicante, Spain, May 22-27, 2020, volume 73 of EPiC S…
  17. EasyChair, 2020. URL https://easychair.org/publications/paper/Tctp. ↗
  18. Thibault Gauthier and Cezary Kaliszyk. Sharing HOL4 and HOL light proof knowledge. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28,… find
  19. Springer, 2015. doi: 10.1007/978-3-662-48899-7\\_26. URL https://doi.org/10.1007/978-3-662-48899-7_26. — [doi:10.1007/978-3-662-48899-7\\_26](https://doi.org/10.1007/978-3-662-48899-7_26) ↗
  20. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Initial experiments with statistical conjecturing over large formal corpora. In Andrea Kohlhase, Paul Libbrecht, Bruce R. Miller, Adam Naumowicz, Walther Neuper, Pedro Quaresma, Frank Wm. Tompa, and Martin Suda, editors, Joint Proceedings of the F… find
  21. CEUR-WS.org, 2016. URL http://ceur-ws.org/Vol-1785/W23.pdf. ↗
  22. 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
  23. EasyChair, 2017. URL https://easychair.org/publications/paper/WsM. ↗
  24. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. Learning to prove with tactics. CoRR, abs/1804.00596, 2018. URL http://arxiv.org/abs/1804.00596. ↗
  25. Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen, François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi Ould Biha, et al. A machine-checked proof of the odd order theorem. In International Conference on Interactive Theorem Proving, pages 163–179. Spring… find
  26. Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. A formal proof of the kepler conjecture. In Forum of mathematics, Pi, volume 5. Cambridge University Press, 2017.
  27. John Harrison. HOL Light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pages 265–269. Springer, 1996. find
  28. 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.
  29. OpenReview.net, 2019. URL https://openreview.net/forum?id=r1xwKoR9Y7. ↗
  30. Geoffrey Irving, Christian Szegedy, Alexander A. Alemi, Niklas Eén, François Chollet, and Josef Urban. DeepMath - deep sequence models for premise selection. In Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Roman Garnett, editors, Advances in Neural Information Processing…
  31. Jan Jakubuv and Josef Urban. Hammering mizar by learning clause guidance (short paper). In John Harrison, John O’Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPIcs, pages 34:1–34:8.… — [doi:10.4230/lipics.itp.2019.34](https://doi.org/10.4230/lipics.itp.2019.34) find
  32. Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, and Josef Urban. ENIGMA anonymous: Symbol-independent inference guiding machine (system description). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning - 10th International Joint Conferenc…
  33. Springer, 2020. doi: 10.1007/978-3-030-51054-1\\_29. URL https://doi.org/10.1007/978-3-030-51054-1_29. — [doi:10.1007/978-3-030-51054-1\\_29](https://doi.org/10.1007/978-3-030-51054-1_29) ↗
  34. Moa Johansson, Dan Rosén, Nicholas Smallbone, and Koen Claessen. Hipster: Integrating theory exploration in a proof assistant. In International Conference on Intelligent Computer Mathematics, pages 108–122. Springer, 2014. find
  35. Justin Johnson, Bharath Hariharan, Laurens van der Maaten, Li Fei-Fei, C Lawrence Zitnick, and Ross Girshick. Clevr: A diagnostic dataset for compositional language and elementary visual reasoning. In Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pages 2901–2910, 201…
  36. Cezary Kaliszyk and Josef Urban. Learning-assisted theorem proving with millions of lemmas. J. Symb. Comput., 69:109–128, 2015. doi: 10.1016/j.jsc.2014.09.032. URL https://doi.org/10.1016/j.jsc.2014.09.032. — [doi:10.1016/j.jsc.2014.09.032](https://doi.org/10.1016/j.jsc.2014.09.032) ↗
  37. Cezary Kaliszyk, Josef Urban, and Jirí Vyskocil. Lemmatization for stronger reasoning in large theories. In Carsten Lutz and Silvio Ranise, editors, Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Wroclaw, Poland, September 21-24, 2015. Proceedings, volume 9322 of Lecture… find
  38. Springer, 2015. doi: 10.1007/978-3-319-24246-0\\_21. URL https://doi.org/10.1007/978-3-319-24246-0_21. — [doi:10.1007/978-3-319-24246-0\\_21](https://doi.org/10.1007/978-3-319-24246-0_21) ↗
  39. Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A machine learning dataset for higher-order logic theorem proving. In 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, April 24-26, 2017, Conference Track Proceedings.
  40. OpenReview.net, 2017. URL https://openreview.net/forum?id=ryuxYmvel. ↗
  41. 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.
  42. Christoph Kern and Mark R Greenstreet. Formal verification in hardware design: a survey. ACM Transactions on Design Automation of Electronic Systems (TODAES), 4(2):123–193, 1999. find
  43. Diederik P. Kingma and Jimmy Ba. Adam: A method for stochastic optimization. In Yoshua Bengio and Yann LeCun, editors, 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. ↗
  44. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In International Conference on Computer Aided Verification, pages 1–35. Springer, 2013. find
  45. Dennis Lee, Christian Szegedy, Markus N. Rabe, Sarah M. Loos, and Kshitij Bansal. Mathematical reasoning in latent space. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26-30, 2020.
  46. OpenReview.net, 2020. URL https://openreview.net/forum?id=Ske31kBtPr. ↗
  47. Douglas B Lenat. Am: An artificial intelligence approach to discovery in mathematics as heuristic search, sail aim-286. Artificial Intelligence Laboratory, Stanford University, 1976. find
  48. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. Modelling high-level mathematical reasoning in mechanised declarative proofs. CoRR, abs/2006.09265, 2020. URL https://arxiv.org/abs/2006.09265. ↗
  49. 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…
  50. EasyChair, 2017. URL https://easychair.org/publications/paper/ND13. ↗
  51. William McCune. Solution of the Robbins’ problem. Journal of Automated Reasoning, 19(3): 263–276, 1997. find
  52. Norman Megill and David A Wheeler. Metamath: A Computer Language for Mathematical Proofs. Lulu. com, 2019.
  53. Miroslav Olsák, Cezary Kaliszyk, and Josef Urban. Property invariant embedding for automated reasoning. In Giuseppe De Giacomo, Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín, and Jérôme Lang, editors, ECAI 2020 - 24th European Conference on Artificial Intelligence, 2…
  54. IOS Press, 2020. doi: 10.3233/FAIA200244. URL https://doi.org/10.3233/FAIA200244. ↗
  55. Myle Ott, Sergey Edunov, Alexei Baevski, Angela Fan, Sam Gross, Nathan Ng, David Grangier, and Michael Auli. fairseq: A fast, extensible toolkit for sequence modeling. In Waleed Ammar, Annie Louis, and Nasrin Mostafazadeh, editors, Proceedings of the 2019 Conference of the North American Chapter of…
  56. Lawrence C. Paulson. Natural deduction as higher-order resolution. The Journal of Logic Programming, 3(3):237–258, 1986. find
  57. Bartosz Piotrowski and Josef Urban. Atpboost: Learning premise selection in binary setting with ATP feedback. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, Automated Reasoning - 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, Flo… find
  58. Springer, 2018. doi: 10.1007/978-3-319-94205-6\\_37. URL https://doi.org/10.1007/978-3-319-94205-6_37. — [doi:10.1007/978-3-319-94205-6\\_37](https://doi.org/10.1007/978-3-319-94205-6_37) ↗
  59. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393. ↗
  60. Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757, 2020.
  61. Pranav Rajpurkar, Jian Zhang, Konstantin Lopyrev, and Percy Liang. Squad: 100, 000+ questions for machine comprehension of text. In Jian Su, Xavier Carreras, and Kevin Duh, editors, Proceedings of the 2016 Conference on Empirical Methods in Natural Language Processing, EMNLP 2016, Austin, Texas, USA…
  62. Tim Rocktäschel and Sebastian Riedel. End-to-end differentiable proving. In Advances in Neural Information Processing Systems, pages 3788–3800, 2017.
  63. Germán Ros, Laura Sellart, Joanna Materzynska, David Vázquez, and Antonio M. López. The SYNTHIA dataset: A large collection of synthetic images for semantic segmentation of urban scenes. In 2016 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2016, Las Vegas, NV, USA, June 27-30, 20… find
  64. IEEE Computer Society, 2016. doi: 10.1109/CVPR.2016.352. URL https://doi.org/10.1109/CVPR.2016.352. ↗
  65. Piotr Rudnicki. An overview of the mizar project. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, pages 311–330. find
  66. Stephan Schulz. System description: E 1.8. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pages 735–743. Springer, 2013. find
  67. David Silver, Julian Schrittwieser, Karen Simonyan, Ioannis Antonoglou, Aja Huang, Arthur Guez, Thomas Hubert, Lucas Baker, Matthew Lai, Adrian Bolton, et al. Mastering the game of Go without human knowledge. Nature, 550(7676):354–359, 2017. find
  68. David Silver, Thomas Hubert, Julian Schrittwieser, Ioannis Antonoglou, Matthew Lai, Arthur Guez, Marc Lanctot, Laurent Sifre, Dharshan Kumaran, Thore Graepel, Timothy Lillicrap, Karen Simonyan, and Demis Hassabis. A general reinforcement learning algorithm that masters chess, shogi, and Go through s… — [doi:10.1126/science.aar6404](https://doi.org/10.1126/science.aar6404) find
  69. Kai Sheng Tai, Richard Socher, and Christopher D. Manning. Improved semantic representations from tree-structured long short-term memory networks. In Proceedings of the 53rd Annual Meeting of the Association for Computational Linguistics and the 7th International Joint Conference on Natural Language… find
  70. Josef Urban. Malarea: a metasystem for automated reasoning in large theories. In Geoff Sutcliffe, Josef Urban, and Stephan Schulz, editors, Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007, volume 257 of CEUR Worksho…
  71. CEUR-WS.org, 2007. URL http://ceur-ws.org/Vol-257/05_Urban.pdf. ↗
  72. Josef Urban and Jan Jakubv. First neural conjecturing datasets and experiments. arXiv preprint arXiv:2005.14664, 2020.
  73. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jirí Vyskocil. Malarea SG1- machine learner for automated reasoning with semantic guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, Augu… find
  74. Springer, 2008. doi: 10.1007/978-3-540-71070-7\\_37. URL https://doi.org/10.1007/978-3-540-71070-7_37. — [doi:10.1007/978-3-540-71070-7\\_37](https://doi.org/10.1007/978-3-540-71070-7_37) ↗
  75. Josef Urban, Jiří Vyskočil, and Petr Štěpánek. MaLeCoP machine learning connection prover. In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, pages 263–277. Springer, 2011. find
  76. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Advances in neural information processing systems, pages 5998–6008, 2017.
  77. Oriol Vinyals, Igor Babuschkin, Wojciech Marian Czarnecki, Michaël Mathieu, Andrew Joseph Dudzik, Junyoung Chung, Duck Hwan Choi, Richard W. Powell, Timo Ewalds, Petko Georgiev, Junhyuk Oh, Dan Horgan, Manuel Kroiss, Ivo Danihelka, Aja Huang, Laurent Sifre, Trevor Cai, John P. Agapiou, Max Jaderberg… find
  78. Mingzhe Wang and Jia Deng. Learning to prove theorems by learning to generate theorems. CoRR, abs/2002.07019, 2020. URL https://arxiv.org/abs/2002.07019. ↗
  79. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. In Advances in Neural Information Processing Systems, pages 2786–2796, 2017.
  80. Minjie Wang, Lingfan Yu, Da Zheng, Quan Gan, Yu Gai, Zihao Ye, Mufei Li, Jinjing Zhou, Qi Huang, Chao Ma, Ziyue Huang, Qipeng Guo, Hao Zhang, Haibin Lin, Junbo Zhao, Jinyang Li, Alexander J. Smola, and Zheng Zhang. Deep graph library: Towards efficient and scalable deep learning on graphs. CoRR, abs… — [arXiv:1909.01315](https://arxiv.org/abs/1909.01315) find
  81. Jason Weston, Antoine Bordes, Sumit Chopra, and Tomas Mikolov. Towards AI-complete question answering: A set of prerequisite toy tasks. In Yoshua Bengio and Yann LeCun, editors, 4th International Conference on Learning Representations, ICLR 2016, San Juan, Puerto Rico, May 2-4, 2016, Conference Trac…
  82. Keyulu Xu, Weihua Hu, Jure Leskovec, and Stefanie Jegelka. How powerful are graph neural networks? In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019.
  83. OpenReview.net, 2019. URL https://openreview.net/forum?id=ryGs6iA5Km. ↗
  84. 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, volume 97 of Proceedings of Machine Learning Research, pages 6984–6994, Long Beach…
  85. Zsolt Zombori, Adrián Csiszárik, Henryk Michalewski, Cezary Kaliszyk, and Josef Urban. Towards finding longer proofs. CoRR, abs/1905.13100, 2019. URL http://arxiv.org/abs/1905.13100. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wu-2020-int-inequality-benchmark-evaluating-generalization/