CoChat
Sign Up
PreprintCited by 30AI-based Problem Solving and PlanningLogic, programming, and type systemsArtificial Intelligence in Games

The DOI matches its DataCite record; 2 of the 2 references it cites were found in a registry or an index.

INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving

Open access
Wu, Yuhuai, Jiang, Albert Qiaochu, Ba, Jimmy, Grosse, Roger·2020·arXiv
DOI 10.48550/arxiv.2007.02924arXiv 2007.02924
Open this paper in CoChat — free accountOpen PDF

Abstract

In learning-assisted theorem proving, one of the most critical challenges is to generalize to theorems unlike those seen at training time. In this paper, we introduce INT, an INequality Theorem proving benchmark, specifically designed to test agents' generalization ability. INT is based on a procedure for generating theorems and proofs; this procedure's knobs allow us to measure 6 different types of generalization, each reflecting a distinct challenge characteristic to automated theorem proving. In addition, unlike prior benchmarks for learning-assisted theorem proving, INT provides a lightweight and user-friendly theorem proving environment with fast simulations, conducive to performing learning-based and search-based research. We introduce learning-based baselines and evaluate them across 6 dimensions of generalization with the benchmark. We then evaluate the same agents augmented with Monte Carlo Tree Search (MCTS) at test time, and show that MCTS can help to prove new theorems.

Overview

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.2007.02924

Cites

2 of 2 references verified0 citation errors · 0 not checkable

Statistics

Verification

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Synthetic data has long been recognized and used as an important ingredient in theorem proving.

    “Synthetic data has long been recognized and used as an important ingredient in theorem proving63–66.”

    From Solving olympiad geometry without human demonstrations (2024) · cites this paper as [63]

    The Introduction describes synthetic datasets as a way to address data scarcity in theorem proving, and the paper introduces a synthetic theorem-proving benchmark. Section 4.1 also reports training agents on generated proofs. These passages support the use and value of synthetic data, but do not establish that it has *long* been recognized as an important ingredient. (LLM, conf=0.82)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Citations

Cites

Flagged first, then by citations

Research works printed but not linked: 63

  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 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of Machine Learning Research, pages 454-463. PMLR, 2019. URL http: //proceedings.mlr.press/v97/bansal19a.html.
  2. 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.
  3. 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.
  4. 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.
  5. Karel Chvalovskỳ, Thibault Gauthier, and Josef Urban. First experiments with data driven con- jecturing. AITP 2019, 2019. URL http://aitp-conference.org/2019/abstract/ AITP_2019_paper_27.pdf.
  6. Simon Colton. Automated theory formation in pure mathematics. Springer Science & Business Media, 2012.
  7. Á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.
  8. 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.
  9. David Steven Dummit and Richard M Foote. Abstract algebra, volume 3. Wiley Hoboken, 2004.
  10. Siemion Fajtlowicz. On conjectures of graffiti. In Annals of Discrete Mathematics, volume 38, pages 113-118. Elsevier, 1988.
  11. 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. · arXiv
  12. Thibault Gauthier. Deep reinforcement learning in HOL4. CoRR, abs/1910.11797, 2019. URL http://arxiv.org/abs/1910.11797. · arXiv
  13. 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 Series in Computing, pages 230-248. EasyChair, 2020. URL https://easychair. org/publications/paper/Tctp.
  14. 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, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 372-386. Springer, 2015. doi: 10.1007/978-3-662-48899-7\_26. URL https://doi.org/10.1007/978-3-662-48899-7_26. · DOI
  15. 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 FM4M, MathUI, and ThEdu Workshops, Doctoral Program, and Work in Progress at the Conference on Intelligent Computer Mathematics 2016 co-located with the 9th Conference on Intelligent Computer Mathematics (CICM 2016), Bialystok, Poland, July 25-29, 2016, volume 1785 of CEUR Workshop Proceedings, pages 219-228. CEUR-WS.org, 2016. URL http: //ceur-ws.org/Vol-1785/W23.pdf.
  16. 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 Series in Computing, pages 125-143. EasyChair, 2017. URL https://easychair.org/publications/paper/WsM.
  17. 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. · arXiv
  18. 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. Springer, 2013.
  19. 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.
  20. John Harrison. HOL Light: A tutorial introduction. In International Conference on Formal Methods in Computer-Aided Design, pages 265-269. Springer, 1996.
  21. 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. OpenReview.net, 2019. URL https://openreview. net/forum?id=r1xwKoR9Y7.
  22. Daniel D. Lee, Masashi Sugiyama, Ulrike von Luxburg, Isabelle Guyon, and Ro- man Garnett, editors, Advances in Neural Information Processing Systems 29: An- nual Conference on Neural Information Processing Systems 2016, December 5-10, 2016, Barcelona, Spain, pages 2235-2243, 2016. URL http://papers.nips.cc/paper/ 6280-deepmath-deep-sequence-models-for-premise-selection.
  23. 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. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2019. doi: 10.4230/ LIPIcs.ITP.2019.34. URL https://doi.org/10.4230/LIPIcs.ITP.2019. · DOI
  24. Jan Jakubuv, Karel Chvalovský, Miroslav Olsák, Bartosz Piotrowski, Martin Suda, and Josef Urban. ENIGMA anonymous: Symbol-independent inference guiding machine (system de- scription). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Rea- soning -10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II, volume 12167 of Lecture Notes in Computer Science, pages 448-463. Springer, 2020. doi: 10.1007/978-3-030-51054-1\_29. URL https://doi.org/10.1007/ 978-3-030-51054-1_29. · DOI
  25. 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.
  26. 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, 2017.
  27. 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
  28. 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 Notes in Computer Science, pages 341-356. Springer, 2015. doi: 10.1007/ 978-3-319-24246-0\_21. URL https://doi.org/10.1007/978-3-319-24246-0_ · DOI
  29. 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. OpenReview.net, 2017. URL https://openreview.net/forum?id=ryuxYmvel.
  30. 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.
  31. 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.
  32. 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. · arXiv
  33. Laura Kovács and Andrei Voronkov. First-order theorem proving and Vampire. In International Conference on Computer Aided Verification, pages 1-35. Springer, 2013.
  34. 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. OpenReview.net, 2020. URL https:// openreview.net/forum?id=Ske31kBtPr.
  35. 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. · arXiv
  36. 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 EPiC Series in Computing, pages 85-105. EasyChair, 2017. URL https://easychair.org/publications/paper/ND13.
  37. William McCune. Solution of the Robbins' problem. Journal of Automated Reasoning, 19(3): 263-276, 1997.
  38. 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, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 -September 8, 2020 -Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020), volume 325 of Frontiers in Artificial Intelligence and Applications, pages 1395-1402. IOS Press, 2020. doi: 10.3233/FAIA200244. URL https://doi.org/10. 3233/FAIA200244. · DOI
  39. 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 the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT 2019, Minneapolis, MN, USA, June 2-7, 2019, Demonstrations, pages 48-53. Association for Computational Linguistics, 2019. doi: 10.18653/v1/n19-4009. URL https://doi.org/10.18653/v1/n19-4009. · DOI
  40. Lawrence C. Paulson. Natural deduction as higher-order resolution. The Journal of Logic Program- ming, 3(3):237-258, 1986.
  41. 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, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, volume 10900 of Lecture Notes in Computer Science, pages 566-574. Springer, 2018. doi: 10.1007/978-3-319-94205-6\_37. URL https://doi.org/10.1007/978-3-319-94205-6_37. · DOI
  42. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393. · arXiv
  43. Markus N Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. arXiv preprint arXiv:2006.04757, 2020. · arXiv
  44. 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, November 1-4, 2016, pages 2383-2392. The Association for Computational Linguistics, 2016. doi: 10.18653/v1/d16-1264. URL https://doi.org/10.18653/v1/ d16-1264. · DOI · Paper page
  45. Tim Rocktäschel and Sebastian Riedel. End-to-end differentiable proving. In Advances in Neural Information Processing Systems, pages 3788-3800, 2017.
  46. 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, 2016, pages 3234-3243. IEEE Computer Society, 2016. doi: 10.1109/CVPR.2016.352. URL https://doi.org/10.1109/CVPR.2016.352. · DOI · Paper page
  47. Piotr Rudnicki. An overview of the mizar project. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, pages 311-330.
  48. Stephan Schulz. System description: E 1.8. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pages 735-743. Springer, 2013.
  49. 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.
  50. 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 Processing (Volume 1: Long Papers), pages 1556-1566, Beijing, China, July 2015. Association for Computational Linguistics. doi: 10.3115/v1/P15-1150. URL https: //www.aclweb.org/anthology/P15-1150. · DOI · Paper page
  51. 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 Workshop Proceedings. CEUR-WS.org, 2007. URL http://ceur-ws.org/ Vol-257/05_Urban.pdf.
  52. Josef Urban and Jan Jakubv. First neural conjecturing datasets and experiments. arXiv preprint arXiv:2005.14664, 2020. · arXiv
  53. 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, August 12-15, 2008, Proceedings, volume 5195 of Lecture Notes in Computer Science, pages 441-456. Springer, 2008. doi: 10.1007/978-3-540-71070-7\_37. URL https: //doi.org/10.1007/978-3-540-71070-7_37. · DOI
  54. 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.
  55. 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.
  56. 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, Alexander Sasha Vezhnevets, Rémi Leblond, Tobias Pohlen, Valentin Dalibard, David Budden, Yury Sulsky, James Molloy, Tom Le Paine, Caglar Gulcehre, Ziyu Wang, Tobias Pfaff, Yuhuai Wu, Roman Ring, Dani Yogatama, Dario Wünsch, Katrina McKinney, Oliver Smith, Tom Schaul, Timothy P. Lillicrap, Koray Kavukcuoglu, Demis Hassabis, Chris Apps, and David Silver. Grandmaster level in StarCraft II using multi-agent reinforcement learning. Nature, pages 1-5, 2019.
  57. 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. · arXiv
  58. 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.
  59. 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/1909.01315, 2019. URL http://arxiv.org/abs/1909.01315. · arXiv
  60. 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 Track Proceedings, 2016. URL http://arxiv.org/abs/1502. 05698.
  61. 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. OpenReview.net, 2019. URL https://openreview.net/forum? id=ryGs6iA5Km.
  62. 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, California, USA, 09-15 Jun 2019. PMLR. URL http:// proceedings.mlr.press/v97/yang19a.html.
  63. 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. · arXiv

Cited by

Sorted by citations

Metadata

Authors
Wu, Y., Jiang, A. Q., Ba, J., & Grosse, R.
Affiliations
University of Toronto (CA)
ORCID
Ba, Jimmy
Venue
arXiv
Publisher
arXiv
Published
2020
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.2007.02924
arXiv
2007.02924
OpenAlex
W3040226941
Cited by
30
References
2
Citations by year
2025: 5 · 2024: 8 · 2023: 10 · 2022: 2 · 2021: 2 · 2020: 3
Type
posted content
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
  • arXiv (Cornell University) (submittedVersion)
  • arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › AI-based Problem Solving and Planning
  • Physical Sciences › Computer Science › Software › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Artificial Intelligence › Artificial Intelligence in Games
Keywords
benchmark, generalization, automated theorem proving, Monte Carlo tree search

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review