Elamur Research⌕
☰
home / papers / 2023 / Magnushammer: A Transformer-Based Approach to Premise Selection

Magnushammer: A Transformer-Based Approach to Premise Selection

Paper · 2023 · Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak et al.

Summary

Premise selection means picking, from a large library of proven facts, the few that help close the current goal in a formal proof. It is central to automated theorem proving. In Isabelle, the standard tool for this is Sledgehammer. It relies on hand-engineered relevance heuristics, translation into other logics, and external ATPs, so it is costly to port to other proof assistants. The authors propose Magnushammer, a transformer trained contrastively on textual proof states and premises. It works in two steps. A SELECT stage embeds states and premises in a shared space and keeps the top 1024 candidates by cosine similarity. A RERANK stage then scores each (state, premise) pair jointly to produce a final ranking. The selected premises are passed directly to native Isabelle tactics, with no external provers involved. To train the model, the team extracted and released a large premise selection dataset from Isabelle and its proof libraries. Magnushammer clearly beats Sledgehammer on PISA and miniF2F. This shows that generic neural retrieval can replace heavily engineered, logic-specific tooling.

Key points

  • PISA: 59.5% proof rate for Magnushammer, compared with 38.3% for Sledgehammer.
  • miniF2F: 34.0% for Magnushammer, compared with 20.9% for Sledgehammer.
  • Combined with Thor: swapping Sledgehammer for Magnushammer inside the neural-symbolic prover Thor raises the PISA state of the art from 57.0% to 71.0%, using about 4x fewer parameters.
  • New dataset: 4.4M (proof state, relevant premise) examples with 433K unique premises. The authors describe it as the largest open premise selection dataset and the first for Isabelle.
  • Scale and efficiency:
    • SELECT narrows roughly 30K–50K available premises per proof state down to 1024.
    • The model outperforms Sledgehammer with only 4K training examples, about 0.1% of the data.
    • Its advantage holds across different compute budgets.

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🎓Cornell UniversityIthaca · United States139 works · 65,295 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 works

🧭 Topics 1Research subjects and languages the work is about.Reasoning · 1,948 works

Cite

Cite as Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś and Yuhuai Wu. 2023. Magnushammer: A Transformer-Based Approach to Premise Selection. arXiv:2303.04488.

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

@misc{mikula2023magnushammer,
  title = {{Magnushammer: A Transformer-Based Approach to Premise Selection}},
  author = {Maciej Mikuła, Szymon Tworkowski, Szymon Antoniak, Bartosz Piotrowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś and Yuhuai Wu},
  year = {2023},
  doi = {10.48550/arxiv.2303.04488},
  eprint = {2303.04488},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2303.04488}
}

References

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

  1. Jesse Alama, Daniel Kühlwein, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Premise selection for mathematics by corpus analysis and kernel methods. CoRR, abs/1108.3446, 2011. URL http://arxiv.org/abs/1108.3446. ↗
  2. Jesse Alama, Tom Heskes, Daniel Kühlwein, Evgeni Tsivtsivadze, and Josef Urban. Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason., 52(2): 191–213, 2014. doi: 10.1007/s10817-013-9286-5. URL https://doi.org/10.1007/s10817-013-9286-5. ↗
  3. Alexander A. Alemi, François Chollet, Geoffrey Irving, Christian Szegedy, and Josef Urban. Deep-Math – deep sequence models for premise selection. CoRR, abs/1606.04442, 2016. URL http://arxiv.org/abs/1606.04442. ↗
  4. Zhangir Azerbayev, Bartosz Piotrowski, and Jeremy Avigad. ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems. In Advances in Neural Information Processing Systems 35, 2nd MATH-AI Workshop at NeurIPS’22, 2022. URL https://mathai2022.github.io/paper… ↗
  5. 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
  6. PMLR, 2019. URL http://proceedings.mlr.press/v97/bansal19a.html. ↗
  7. Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT sol… — cvc5: A Versatile and Industrial-Strength SMT Solver
  8. Springer, 2022. doi: 10.1007/978-3-030-99524-9\\ 24. URL https://doi.org/10.1007/978-3-030-99524-9_24. — [doi:10.1007/978-3-030-99524-9\](https://doi.org/10.1007/978-3-030-99524-9\) ↗
  9. Yves Bertot. A short presentation of coq. In Otmane Aı̈t Mohamed, César A. Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings, volume 5170 of Lecture Notes in Computer Science, pa… find
  10. Springer, 2008. doi: 10.1007/978-3-540-71067-7\\ 3. URL https://doi.org/10.1007/978-3-540-71067-7_3. — [doi:10.1007/978-3-540-71067-7\](https://doi.org/10.1007/978-3-540-71067-7\) ↗
  11. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. J. Autom. Reason., 51(1):109–128, 2013. doi: 10.1007/s10817-013-9278-5. URL https://doi.org/10.1007/s10817-013-9278-5. — [doi:10.1007/s10817-013-9278-5](https://doi.org/10.1007/s10817-013-9278-5) ↗
  12. Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban. A learning-based fact selector for Isabelle/HOL. J. Autom. Reason., 57(3):219–244, 2016. doi: 10.1007/s10817-016-9362-8. URL https://doi.org/10.1007/s10817-016-9362-8. — [doi:10.1007/s10817-016-9362-8](https://doi.org/10.1007/s10817-016-9362-8) ↗
  13. Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement day. In Jürgen Giesl and Reiner Hähnle, editors, Automated Reasoning, pages 107–121, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. ISBN 978-3-642-14203-1. find
  14. Sebastian Borgeaud, Arthur Mensch, Jordan Hoffmann, Trevor Cai, Eliza Rutherford, Katie Millican, George van den Driessche, Jean-Baptiste Lespiau, Bogdan Damoc, Aidan Clark, Diego de Las Casas, Aurelia Guy, Jacob Menick, Roman Ring, Tom Hennigan, Saffron Huang, Loren Maggiore, Chris Jones, Albin Cas… find
  15. PMLR, 2022. URL https://proceedings.mlr.press/v162/borgeaud22a.html. ↗
  16. 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
  17. Ting Chen, Simon Kornblith, Mohammad Norouzi, and Geoffrey E. Hinton. A simple framework for contrastive learning of visual representations. In Proceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event, volume 119 of Proceedings of Machine Learni…
  18. PMLR, 2020. URL http://proceedings.mlr.press/v119/chen20j.html. ↗
  19. Alexis Conneau and Guillaume Lample. Cross-lingual language model pretraining. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc, E. Fox, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 32. Curran Associates, Inc., 2019. URL https://proceedings.neurips.… ↗
  20. Lukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for dependent type theory. J. Autom. Reason., 61(1-4):423–453, 2018. doi: 10.1007/s10817-018-9458-4. URL https://doi.org/10.1007/s10817-018-9458-4. ↗
  21. Nicolaas Govert De Bruijn. The mathematical language AUTOMATH, its usage, and some of its extensions. In Symposium on automatic demonstration, pages 29–61. Springer, 1970. find
  22. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Tools and Algorithms for the Construction and Analysis of Systems, pages 337–340, Berlin, Heidelberg, 2008. Springer Berlin Heidelberg. ISBN 978-3-540-78800-3. find
  23. Leonardo Mendonça de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean theorem prover (system description). In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction – CADE-25 – 25th International Conference on Automated Deduction, Berlin, Germany, August 1… find
  24. 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\](https://doi.org/10.1007/978-3-319-21401-6\) ↗
  25. Gabriel Ebner. Integration of general-purpose automated theorem provers in Lean, 2020. https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/slides/fomm_ebner.pdf. ↗
  26. Leo Gao, Stella Biderman, Sid Black, Laurence Golding, Travis Hoppe, Charles Foster, Jason Phang, Horace He, Anish Thite, Noa Nabeshima, Shawn Presser, and Connor Leahy. The Pile: An 800GB dataset of diverse text for language modeling. CoRR, abs/2101.00027, 2021. URL https://arxiv.org/abs/2101.00027… ↗
  27. Thibault Gauthier and Cezary Kaliszyk. Premise selection and external provers for HOL4. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, Mumbai, India, January 15-17, 2015, pages 49–57. find
  28. ACM, 2015. doi: 10.1145/2676724.2693173. URL https://doi.org/10.1145/2676724.2693173. — [doi:10.1145/2676724.2693173](https://doi.org/10.1145/2676724.2693173) ↗
  29. Zarathustra Amadeus Goertzel, Jan Jakubuv, Cezary Kaliszyk, Miroslav Olsák, Jelle Piepenbrock, and Josef Urban. The Isabelle ENIGMA. In June Andronick and Leonardo de Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237… — [doi:10.4230/lipics.itp.2022.16](https://doi.org/10.4230/lipics.itp.2022.16) find
  30. Adam Grabowski, Artur Kornilowicz, and Adam Naumowicz. Mizar in a nutshell. J. Formaliz. Reason., 3(2):153–245, 2010. doi: 10.6092/issn.1972-5787/1980. URL https://doi.org/10.6092/issn.1972-5787/1980. — [doi:10.6092/issn.1972-5787/1980](https://doi.org/10.6092/issn.1972-5787/1980) ↗
  31. Jesse Michael Han, Tao Xu, Stanislas Polu, Arvind Neelakantan, and Alec Radford. Contrastive finetuning of generative language models for informal premise selection. 6th Conference on Artificial Intelligence and Theorem Proving, 2021. find
  32. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022.
  33. OpenReview.net, 2022. URL https://openreview.net/forum?id=rpxJc9j04U. ↗
  34. 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
  35. Springer, 1996. doi: 10.1007/BFb0031814. URL https://doi.org/10.1007/BFb0031814. — [doi:10.1007/bfb0031814](https://doi.org/10.1007/bfb0031814) ↗
  36. Jordan Hoffmann, Sebastian Borgeaud, Arthur Mensch, Elena Buchatskaya, Trevor Cai, Eliza Rutherford, Diego de Las Casas, Lisa Anne Hendricks, Johannes Welbl, Aidan Clark, Tom Hennigan, Eric Noland, Katie Millican, George van den Driessche, Bogdan Damoc, Aurelia Guy, Simon Osindero, Karen Simonyan, E… — Training Compute-Optimal Large Language Models
  37. Jeremy Howard and Sebastian Ruder. Universal language model fine-tuning for text classification. In Iryna Gurevych and Yusuke Miyao, editors, Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics, ACL 2018, Melbourne, Australia, July 15-20, 2018, Volume 1: Long Pape… find
  38. Gautier Izacard, Mathilde Caron, Lucas Hosseini, Sebastian Riedel, Piotr Bojanowski, Armand Joulin, and Edouard Grave. Towards unsupervised dense information retrieval with contrastive learning. CoRR, abs/2112.09118, 2021. URL https://arxiv.org/abs/2112.09118. ↗
  39. Albert Q. Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. LISA: Language models of ISAbelle proofs. 6th Conference on Artificial Intelligence and Theorem Proving, 2021. find
  40. Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances…
  41. Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. CoRR, abs/2210.12283, 2022b. doi: 10.48550/arXiv.2210.12283.
  42. Cezary Kaliszyk and Josef Urban. HOL(y)Hammer: Online ATP service for HOL Light. Math. Comput. Sci., 9(1):5–22, 2015a. doi: 10.1007/s11786-014-0182-0. URL https://doi.org/10.1007/s11786-014-0182-0. ↗
  43. Cezary Kaliszyk and Josef Urban. MizAR 40 for Mizar 40. Journal of Automated Reasoning, 55(3): 245–256, 2015b.
  44. Cezary Kaliszyk, François Chollet, and Christian Szegedy. HolStep: A machine learning dataset for higher-order logic theorem proving. CoRR, abs/1703.00426, 2017. URL http://arxiv.org/abs/1703.00426. ↗
  45. Jared Kaplan, Sam McCandlish, Tom Henighan, Tom B. Brown, Benjamin Chess, Rewon Child, Scott Gray, Alec Radford, Jeffrey Wu, and Dario Amodei. Scaling laws for neural language models. CoRR, abs/2001.08361, 2020. URL https://arxiv.org/abs/2001.08361. ↗
  46. Laura Kovács and Andrei Voronkov. First-order theorem proving and vampire. In Natasha Sharygina and Helmut Veith, editors, Computer Aided Verification – 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings, volume 8044 of Lecture Notes in Computer Science… find
  47. Springer, 2013. doi: 10.1007/978-3-642-39799-8\\ 1. URL https://doi.org/10.1007/978-3-642-39799-8_1. — [doi:10.1007/978-3-642-39799-8\](https://doi.org/10.1007/978-3-642-39799-8\) ↗
  48. Alex Krizhevsky, Ilya Sutskever, and Geoffrey E. Hinton. ImageNet classification with deep convolutional neural networks. In Peter L. Bartlett, Fernando C. N. Pereira, Christopher J. C. Burges, Léon Bottou, and Kilian Q. Weinberger, editors, Advances in Neural Information Processing Systems 25: 26t…
  49. Daniel Kühlwein, Twan van Laarhoven, Evgeni Tsivtsivadze, Josef Urban, and Tom Heskes. Overview and evaluation of premise selection techniques for large theory mathematics. In Bernhard Gramlich, Dale Miller, and Uli Sattler, editors, Automated Reasoning – 6th International Joint Conference, IJCAR 2… find
  50. Springer, 2012. doi: 10.1007/978-3-642-31365-3\\ 30. URL https://doi.org/10.1007/978-3-642-31365-3_30. — [doi:10.1007/978-3-642-31365-3\](https://doi.org/10.1007/978-3-642-31365-3\) ↗
  51. Daniel Kühlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. MaSh: Machine learning for Sledgehammer. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving – 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013.… find
  52. Springer, 2013. doi: 10.1007/978-3-642-39634-2\\ 6. URL https://doi.org/10.1007/978-3-642-39634-2_6. — [doi:10.1007/978-3-642-39634-2\](https://doi.org/10.1007/978-3-642-39634-2\) ↗
  53. Guillaume Lample, Timothee Lacroix, Marie Anne Lachaux, Aurelien Rodriguez, Amaury Hayat, Thibaut Lavril, Gabriel Ebner, and Xavier Martinet. HyperTree proof search for neural theorem proving. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances in Neural Informatio…
  54. Aitor Lewkowycz, Anders Johan Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Venkatesh Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. Solving quantitative reasoning problems with language models. In Alic…
  55. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. IsarStep: A benchmark for high-level mathematical reasoning. In International Conference on Learning Representations, 2021. URL https://openreview.net/forum?id=Pzj6fzU6wkj. ↗
  56. Jia Meng and Lawrence C. Paulson. Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log., 7(1):41–57, 2009. doi: 10.1016/j.jal.2007.07.004. — [doi:10.1016/j.jal.2007.07.004](https://doi.org/10.1016/j.jal.2007.07.004) find
  57. Yutaka Nagashima and Yilun He. PaMpeR: Proof Method Recommendation system for Isabelle/HOL, 2018. URL https://arxiv.org/abs/1806.07239. ↗
  58. Arvind Neelakantan, Tao Xu, Raul Puri, Alec Radford, Jesse Michael Han, Jerry Tworek, Qiming Yuan, Nikolas Tezak, Jong Wook Kim, Chris Hallacy, Johannes Heidecke, Pranav Shyam, Boris Power, Tyna Eloundou Nekoul, Girish Sastry, Gretchen Krueger, David Schnurr, Felipe Petroski Such, Kenny Hsu, Madelei… — Text and Code Embeddings by Contrastive Pre-Training
  59. Tobias Nipkow. Fun with functions. Archive of Formal Proofs, August 2008. ISSN 2150-914x. https://isa-afp.org/entries/FunWithFunctions.html, Formal proof development. ↗
  60. Rodrigo Frassetto Nogueira and Kyunghyun Cho. Passage re-ranking with BERT. abs/1901.04085, 2019. URL http://arxiv.org/abs/1901.04085. ↗
  61. CoRR, Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. 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 Intelligen…
  62. AAAI Press, 2020. URL https://ojs.aaai.org/index.php/AAAI/article/view/5689. ↗
  63. Lawrence C. Paulson. Isabelle: The next 700 theorem provers. CoRR, cs.LO/9301106, 1993. URL https://arxiv.org/abs/cs/9301106. ↗
  64. Lawrence Charles Paulson and Jasmin Christian Blanchette. Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In IWIL@LPAR, 2012. find
  65. 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
  66. 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\](https://doi.org/10.1007/978-3-319-94205-6\) ↗
  67. Bartosz Piotrowski and Josef Urban. Stateful premise selection by recurrent neural networks. 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 Seri…
  68. EasyChair, 2020. doi: 10.29007/j5hd. URL https://doi.org/10.29007/j5hd. — [doi:10.29007/j5hd](https://doi.org/10.29007/j5hd) ↗
  69. Bartosz Piotrowski, Ramon Fernández Mir, and Edward W. Ayers. Machine-learned premise selection for Lean. In Revantha Ramanayake and Josef Urban, editors, Automated Reasoning with Analytic Tableaux and Related Methods - 32nd International Conference, TABLEAUX 2023, Prague, Czech Republic, September… find
  70. Springer, 2023. doi: 10.1007/978-3-031-43513-3\\ 10. URL https://doi.org/10.1007/978-3-031-43513-3_10. — [doi:10.1007/978-3-031-43513-3\](https://doi.org/10.1007/978-3-031-43513-3\) ↗
  71. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393. ↗
  72. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. In The Eleventh International Conference on Learning Representations, ICLR 2023, Kigali, Rwanda, May 1-5, 2023.
  73. OpenReview.net, 2023. URL https://openreview.net/pdf?id=-P7G-8dmSh4. ↗
  74. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya Sutskever, et al. Language models are unsupervised multitask learners. OpenAI blog, 1(8):9, 2019. find
  75. Alec Radford, Jong Wook Kim, Chris Hallacy, Aditya Ramesh, Gabriel Goh, Sandhini Agarwal, Girish Sastry, Amanda Askell, Pamela Mishkin, Jack Clark, Gretchen Krueger, and Ilya Sutskever. Learning transferable visual models from natural language supervision. CoRR, abs/2103.00020, 2021. URL https://arx…
  76. Stephen E. Robertson and Hugo Zaragoza. The probabilistic relevance framework: BM25 and beyond. Found. Trends Inf. Retr., 3(4):333–389, 2009. doi: 10.1561/1500000019. find
  77. Joshua David Robinson, Ching-Yao Chuang, Suvrit Sra, and Stefanie Jegelka. Contrastive learning with hard negative samples. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. find
  78. OpenReview.net, 2021. URL https://openreview.net/forum?id=CR1XOQ0UTh-. ↗
  79. Stephan Schulz. System description: E 0.81. In David Basin and Michaël Rusinowitch, editors, Automated Reasoning, pages 223–228, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. ISBN 978-3-540-25984-8. find
  80. Jianlin Su, Yu Lu, Shengfeng Pan, Bo Wen, and Yunfeng Liu. Roformer: Enhanced transformer with rotary position embedding. CoRR, abs/2104.09864, 2021. URL https://arxiv.org/abs/2104.09864. ↗
  81. G. Sutcliffe. The TPTP Problem Library and Associated Infrastructure. From CNF to TH0, TPTP v6.4.0. Journal of Automated Reasoning, 59(4):483–502, 2017. find
  82. Terence Tao. Solving mathematical problems: A personal perspective. Oxford University Press, 2010. find
  83. Nandan Thakur, Nils Reimers, Andreas Rücklé, Abhishek Srivastava, and Iryna Gurevych. BEIR: A heterogenous benchmark for zero-shot evaluation of information retrieval models. CoRR, abs/2104.08663, 2021. URL https://arxiv.org/abs/2104.08663. ↗
  84. Szymon Tworkowski, Maciej Mikuła, Tomasz Odrzygóźdź, Konrad Czechowski, Szymon Antoniak, Albert Jiang, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Formal premise selection with language models. AITP 2022, 2022. URL http://aitp-conference.org/2022/abstract/AITP_2022_paper_32.… ↗
  85. Josef Urban and Jan Jakubuv. First neural conjecturing datasets and experiments. In Christoph Benzmüller and Bruce R. Miller, editors, Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings, volume 12236 of Lecture Notes in Compu…
  86. Springer, 2020. doi: 10.1007/978-3-030-53518-6\\ 24. URL https://doi.org/10.1007/978-3-030-53518-6_24. — [doi:10.1007/978-3-030-53518-6\](https://doi.org/10.1007/978-3-030-53518-6\) ↗
  87. Josef Urban, Geoff Sutcliffe, Petr Pudlák, and Jiřı́ Vyskočil. MaLARea SG1 – machine learner for automated reasoning with semantic guidance. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, pages 441–456, Berlin, Heidelberg, 2008. Springer Berlin Heidelber… find
  88. Aäron van den Oord, Yazhe Li, and Oriol Vinyals. Representation learning with contrastive predictive coding. CoRR, abs/1807.03748, 2018. URL http://arxiv.org/abs/1807.03748. ↗
  89. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. CoRR, abs/1706.03762, 2017. URL http://arxiv.org/abs/1706.03762. ↗
  90. Ben Wang and Aran Komatsuzaki. GPT-J-6B: A 6 Billion Parameter Autoregressive Language Model. https://github.com/kingoflolz/mesh-transformer-jax, May 2021. ↗
  91. Mingzhe Wang, Yihe Tang, Jian Wang, and Jia Deng. Premise selection for theorem proving by deep graph embedding. CoRR, abs/1709.09994, 2017. URL http://arxiv.org/abs/1709.09994. ↗
  92. Christoph Weidenbach. Combining superposition, sorts and splitting. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, pages 1965–2013. find
  93. Elsevier and MIT Press, 2001. doi: 10.1016/b978-044450813-3/50029-1. URL https://doi.org/10.1016/b978-044450813-3/50029-1. — [doi:10.1016/b978-044450813-3/50029-1](https://doi.org/10.1016/b978-044450813-3/50029-1) ↗
  94. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus Norman Rabe, Charles E Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Alice H. Oh, Alekh Agarwal, Danielle Belgrave, and Kyunghyun Cho, editors, Advances in Neural Information Processing Systems, 2022a. URL…
  95. Yuhuai Wu, Markus Norman Rabe, DeLesley Hutchins, and Christian Szegedy. Memorizing transformers. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. find
  96. OpenReview.net, 2022b. URL https://openreview.net/forum?id=TrjbxzRcnf-. ↗
  97. 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, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings o…
  98. PMLR, 2019. URL http://proceedings.mlr.press/v97/yang19a.html. ↗
  99. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. CoRR, abs/2306.15626, 2023. doi: 10.48550/arXiv.2306.15626. URL https://doi.org/10.48550/arXiv.2306.156… ↗
  100. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: A cross-system benchmark for formal olympiad-level mathematics. In The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022.
  101. OpenReview.net, 2022. URL https://openreview.net/forum?id=9ZPegFuFTFv. ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/mikula-2023-magnushammer-transformer-based-approach-premise/