Elamur Research⌕
☰
home / papers / 2023 / LEGO-Prover: Neural Theorem Proving with Growing Libraries

LEGO-Prover: Neural Theorem Proving with Growing Libraries

Paper · 2023 · Haiming Wang, Huajian Xin, Chuanyang Zheng et al.

Summary

Formal theorem proving is still hard for large language models. Existing LLM-based provers often fail on competition problems at middle-school level. These "plain" provers write each proof as one long monolithic block and treat the available theorem library as fixed. So a lemma proved for one problem cannot help with another, and long reasoning chains often break. LEGO-Prover addresses this by building proofs from modular pieces. It works in Isabelle and follows the Draft, Sketch, and Prove setup, where each problem comes with an informal statement, an informal proof and a formal statement. A prover component retrieves verified lemmas ("skills") from a library, asks the LLM to write sub-goal lemmas plus a final proof, and stores newly verified lemmas. An evolver component prompts the LLM to rewrite stored skills into more general, reusable forms, which are verified and added back. On miniF2F, this growing-library approach sets new state-of-the-art pass rates. It shows that accumulating and refining reusable lemmas, much as mathematicians do, makes LLM provers stronger.

Key points

  • miniF2F pass rates improve from 48.0% to 57.0% on the validation split and from 45.5% to 50.0% on the test split, an average absolute gain of 6.75 points.
  • During proving, the system generated more than 20,000 verified lemmas, and the final skill library holds 22,532 skills.
  • In an ablation, adding the newly generated skills raised the success rate from 47.1% to 50.4%.
  • The architecture has two parts, a prover that composes modular proofs from retrieved skills and an evolver that generalizes skills, linked by a shared, growing skill library.
  • Code and all generated skills are released at github.com/wiio12/LEGO-Prover.

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

🎓Chinese University of Hong KongHong Kong · China159 works · 16,154 citations🏢Huawei TechnologiesShenzhen · China96 works · 15,432 citations🎓Mohamed bin Zayed University of Artificial IntelligenceAbu Dhabi · United Arab Emirates138 works · 6,590 citations🎓City University of Hong KongHong Kong · China59 works · 3,480 citations

 Fields, topics and concepts

📚 Shelves 3The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputational Theory and Mathematics · 321 works

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

Cite

Cite as Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao and Xiaodan Liang. 2023. LEGO-Prover: Neural Theorem Proving with Growing Libraries. arXiv:2310.00656.

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

@misc{wang2023lego,
  title = {{LEGO-Prover: Neural Theorem Proving with Growing Libraries}},
  author = {Haiming Wang, Huajian Xin, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, Jian Yin, Zhenguo Li, Heng Liao and Xiaodan Liang},
  year = {2023},
  doi = {10.48550/arxiv.2310.00656},
  eprint = {2310.00656},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2310.00656}
}

References

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

  1. Jesse Alama, Michael Kohlhase, Lionel Mamane, Adam Naumowicz, Piotr Rudnicki, and Josef Urban. Licensing the mizar mathematical library. In James H. Davenport, William M. Farmer, Josef Urban, and Florian Rabe (eds.), Intelligent Computer Mathematics - 18th Symposium, Calculemus 2011, and 10th Intern… find
  2. Springer, 2011. doi: 10.1007/ 978-3-642-22673-1\\ 11. URL https://doi.org/10.1007/978-3-642-22673-1_ 11. — [doi:10.1007/978-3-642-22673-1_](https://doi.org/10.1007/978-3-642-22673-1_) ↗
  3. Alexander A. Alemi, François Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban. DeepMath - deep sequence models for premise selection. In Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS’16, pp. 2243–2251, Red Hook, NY, USA, Dece…
  4. Jeremy Avigad. Mathematics and the formal turn. 2023. URL https://www.andrew.cmu.edu/user/avigad/Papers/formal_turn.pdf. ↗
  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 (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2… — HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
  6. PMLR, 2019. URL http://proceedings.mlr.press/v97/bansal19a.html. 1 ↗
  7. Kshitij Bansal, Christian Szegedy, Markus Norman Rabe, Sarah M. Loos, and Viktor Toman. Learning to Reason in Large Theories without Imitation. September 2020. URL https://openreview.net/forum?id=qbRv1k2AcH. ↗
  8. Bruno Barras, Samuel Boutin, Cristina Cornes, Judicaël Courant, Jean-Christophe Filliâtre, Eduardo Giménez, Hugo Herbelin, Gérard Huet, César Muñoz, Chetan Murthy, Catherine Parent, Christine Paulin-Mohring, Amokrane Saı̈bi, and Benjamin Werner. The Coq Proof Assistant Reference Manual : Versi… find
  9. Clark Barrett, Christopher L Conway, Morgan Deters, Liana Hadarean, Dejan Jovanović, Tim King, Andrew Reynolds, and Cesare Tinelli. Cvc4. In Computer Aided Verification: 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 23, pp. 171–177. find
  10. Alexander Bentkamp, Jasmin Blanchette, Sophie Tourret, and Petar Vukmirović. Superposition for Full Higher-order Logic. In André Platzer and Geoff Sutcliffe (eds.), Automated Deduction – CADE 28, Lecture Notes in Computer Science, pp. 396–412, Cham, 2021. Springer International Publishing. ISBN 97… — [doi:10.1007/978-3-030-79876-5](https://doi.org/10.1007/978-3-030-79876-5) find
  11. Garrett Birkhoff. Rings of sets. Duke Mathematical Journal, (3):443–454, 1937. find
  12. Rishi Bommasani, Drew A. Hudson, Ehsan Adeli, Russ Altman, Simran Arora, Sydney von Arx, Michael S. Bernstein, Jeannette Bohg, Antoine Bosselut, Emma Brunskill, Erik Brynjolfsson, Shyamal Buch, Dallas Card, Rodrigo Castellon, Niladri Chatterji, Annie Chen, Kathleen Creel, Jared Quincy Davis, Dora De… — On the Opportunities and Risks of Foundation Models
  13. Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D 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 Ziegler, Jeffrey Wu, Clemens Winter, Chri… find
  14. Curran Associates, Inc., 2020. URL https://proceedings.neurips.cc/paper/2020/file/1457c0d6bfcb4967418bfb8ac142f64a-Paper.pdf. ↗
  15. Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, Harsha Nori, Hamid Palangi, Marco Tulio Ribeiro, and Yi Zhang. Sparks of artificial general intelligence: Early experiments with gpt-4, 2023.
  16. Aydar Bulatov, Yuri Kuratov, and Mikhail S. Burtsev. Recurrent memory transformer, 2022. find
  17. Aydar Bulatov, Yuri Kuratov, and Mikhail S. Burtsev. Scaling transformer to 1m tokens and beyond with rmt, 2023. find
  18. Kevin Buzzard, Johan Commelin, and Patrick Massot. Formalising perfectoid spaces. CoRR, abs/1910.12320, 2019. URL http://arxiv.org/abs/1910.12320. ↗
  19. Tianle Cai, Xuezhi Wang, Tengyu Ma, Xinyun Chen, and Denny Zhou. Large language models as tool makers. arXiv preprint arXiv:2305.17126, 2023. 3
  20. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Pondé de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mi… — Evaluating Large Language Models Trained on Code
  21. Noam Chomsky. Three models for the description of language. IRE Transactions on information theory, 2(3):113–124, 1956. find
  22. Thierry Coquand and Gérard Huet. The calculus of constructions. PhD thesis, INRIA, 1986. find
  23. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76 (2):95–120, February 1988. ISSN 0890-5401. doi: 10.1016/0890-5401(88)90005-3. URL https://www.sciencedirect.com/science/article/pii/0890540188900053. ↗
  24. Thierry Coquand and Christine Paulin. Inductively defined types. In Per Martin-Löf and Grigori Mints (eds.), COLOG-88, Lecture Notes in Computer Science, pp. 50–66, Berlin, Heidelberg, 1990. Springer. ISBN 978-3-540-46963-6. doi: 10.1007/3-540-52335-9 47. — [doi:10.1007/3-540-52335-9](https://doi.org/10.1007/3-540-52335-9) find
  25. Sander R. Dahmen, Johannes Hölzl, and Robert Y. Lewis. Formalizing the solution to the cap set problem. In John Harrison, John O’Leary, and Andrew Tolmach (eds.), 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA, volume 141 of LIPIcs, p… — [doi:10.4230/lipics.itp.2019.15](https://doi.org/10.4230/lipics.itp.2019.15) find
  26. Giannis Daras and Alexandros G. Dimakis. Discovering the Hidden Vocabulary of DALLE-2. Technical Report arXiv:2206.00169, arXiv, May 2022. URL http://arxiv.org/abs/ 2206.00169. arXiv:2206.00169 [cs] type: article. — [arXiv:2206.00169](https://arxiv.org/abs/2206.00169) ↗
  27. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem-proving. Communications of the ACM, 5(7):394–397, 1962. ISSN 0001-0782. doi: 10.1145/368273.368557. URL https://doi.org/10.1145/368273.368557. ↗
  28. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pp. 337–340, Berlin, Heidelberg, 2008. Springer-Verlag. IS… find
  29. Leonardo de Moura and Nikolaj Bjørner. Z3: An Efficient SMT Solver. In C. R. Ramakrishnan and Jakob Rehof (eds.), Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pp. 337–340, Berlin, Heidelberg, 2008. Springer. ISBN 978-3-540-78800-3. doi: 10.100… find
  30. Leonardo 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 (eds.), Automated Deduction - CADE-25, Lecture Notes in Computer Science, pp. 378–388, Cham, 2015. Springer International Publishin… find
  31. Jacob Devlin, Ming-Wei Chang, Kenton Lee, and Kristina Toutanova. BERT: pre-training of deep bidirectional transformers for language understanding. In Jill Burstein, Christy Doran, and Thamar Solorio (eds.), Proceedings of the 2019 Conference of the North American Chapter of the Association for Comp…
  32. Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de Moura. A metaprogramming framework for formal verification. Proc. ACM Program. Lang., 1(ICFP), aug 2017. doi: 10.1145/3110278. URL https://doi.org/10.1145/3110278. — [doi:10.1145/3110278](https://doi.org/10.1145/3110278) ↗
  33. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. CoRR, abs/2303.04910, 2023. doi: 10.48550/arXiv.2303.04910. URL https://doi.org/10.48550/arXiv.2303.04910. 1, 2, 3 ↗
  34. 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. arXiv preprint arXiv:2101.00027, 2020. find
  35. Vijay K. Garg. Introduction to Lattice Theory with Computer Science Applications. Wiley Publishing, 1st edition, 2015. ISBN 1118914376. find
  36. Thibault Gauthier, Cezary Kaliszyk, and Josef Urban. Tactictoe: Learning to reason with HOL4 tactics. In Thomas Eiter and David Sands (eds.), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPiC Seri… find
  37. EasyChair, 2017. doi: 10.29007/ntlb. URL https://doi.org/10.29007/ntlb. ↗
  38. Emmanuel Gunther, Miguel Pagano, Pedro Sánchez Terraf, and Matı́as Steinberg. The independence of the continuum hypothesis in isabelle/zf. Arch. Formal Proofs, 2022, 2022. URL https://www.isa-afp.org/entries/Independence_CH.html. ↗
  39. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. Proof Artifact Co-training for Theorem Proving with Language Models. ICLR 2022, February 2021. URL http://arxiv.org/abs/2102.06203. arXiv: 2102.06203. ↗
  40. 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.
  41. OpenReview.net, 2022. URL https://openreview.net/forum?id=rpxJc9j04U. 1, 2, 3 ↗
  42. John Harrison. HOL light: An overview. In Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (eds.), Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Scien… find
  43. Springer, 2009. doi: 10.1007/978-3-642-03359-9\\ 4. URL https://doi.org/10.1007/978-3-642-03359-9_4. — [doi:10.1007/978-3-642-03359-9\](https://doi.org/10.1007/978-3-642-03359-9\) ↗
  44. John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Jörg H. Siekmann (ed.), Computational Logic, volume 9 of Handbook of the History of Logic, pp. 135–214. Elsevier, 2014a. doi: 10.1016/B978-0-444-51624-4.50004-6. URL https://doi.org/10. 1016/B978-0-444-51624-4… find
  45. John Harrison, Josef Urban, and Freek Wiedijk. History of interactive theorem proving. In Computational Logic, volume 9, pp. 135–214, 2014b. find
  46. John Harrison, Josef Urban, and Freek Wiedijk. History of Interactive Theorem Proving. In Handbook of the History of Logic, volume 9, pp. 135–214. Elsevier, 2014c. ISBN 978-0-444-51624-4. doi: 10.1016/B978-0-444-51624-4.50004-6. URL https://linkinghub.elsevier.com/retrieve/pii/B9780444516244500046. ↗
  47. Chadi Helwe, Chloe Clavel, and Fabian Suchanek. Reasoning with Transformer-based Models: Deep Learning, but Shallow Reasoning. Deep Learning, pp. 28. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem so… — Measuring Mathematical Problem Solving With the MATH Dataset
  48. William Alvin Howard. The Formulae-as-Types Notion of Construction. In Haskell Curry, Hindley B, Seldin J. Roger, and P. Jonathan (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, 1980. find
  49. Geoffrey Jefferson. The mind of mechanical man. British Medical Journal, 1(4616):1105, 1949. find
  50. Ziwei Ji, Nayeon Lee, Rita Frieske, Tiezheng Yu, Dan Su, Yan Xu, Etsuko Ishii, Yejin Bang, Andrea Madotto, and Pascale Fung. Survey of hallucination in natural language generation. CoRR, abs/2202.03629, 2022. URL https://arxiv.org/abs/2202.03629. ↗
  51. 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. arXiv preprint arXiv:2205.10893, 2022a. 1, 2, 3, 6, 7
  52. 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. URL https://doi.org/10.…
  53. Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. Lisa: Language models of isabelle proofs. 2021. 1, 6 find
  54. Takeshi Kojima, Shixiang Shane Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large Language Models are Zero-Shot Reasoners. Technical Report arXiv:2205.11916, arXiv, May 2022. URL http://arxiv.org/abs/2205.11916. arXiv:2205.11916 [cs] type: article. ↗
  55. Laura Kovács and Andrei Voronkov. First-Order Theorem Proving and Vampire. In Natasha Sharygina and Helmut Veith (eds.), Computer Aided Verification, Lecture Notes in Computer Science, pp. 1–35, Berlin, Heidelberg, 2013. Springer. ISBN 978-3-642-39799-8. doi: 10.1007/ 978-3-642-39799-8 1. find
  56. Guillaume Lample and François Charton. Deep Learning for Symbolic Mathematics. arXiv:1912.01412 [cs], December 2019. URL http://arxiv.org/abs/1912.01412. arXiv: 1912.01412. ↗
  57. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. HyperTree Proof Search for Neural Theorem Proving. Technical Report arXiv:2205.11491, arXiv, May 2022. URL http://arxiv.org/ abs/2205.11491. arXiv:2205.1149… ↗
  58. Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. Deep learning. Nature, 521(7553):436–444, May 2015. ISSN 1476-4687. doi: 10.1038/nature14539. URL https://www.nature.com/ articles/nature14539. Number: 7553 Publisher: Nature Publishing Group. — [doi:10.1038/nature14539](https://doi.org/10.1038/nature14539) ↗
  59. Mike Lewis, Yinhan Liu, Naman Goyal, Marjan Ghazvininejad, Abdelrahman Mohamed, Omer Levy, Ves Stoyanov, and Luke Zettlemoyer. Bart: Denoising sequence-to-sequence pre-training for natural language generation, translation, and comprehension, 2019.
  60. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. 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 NeurIPS, 2022. UR…
  61. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. IsarStep: a Benchmark for High-level Mathematical Reasoning. In ICLR 2021, September 2020. URL https://openreview.net/ forum?id=Pzj6fzU6wkj. ↗
  62. Yujia Li, David Choi, Junyoung Chung, Nate Kushman, Julian Schrittwieser, Rémi Leblond, Tom Eccles, James Keeling, Felix Gimeno, Agustin Dal Lago, Thomas Hubert, Peter Choy, Cyprien de Masson d’Autume, Igor Babuschkin, Xinyun Chen, Po-Sen Huang, Johannes Welbl, Sven Gowal, Alexey Cherepanov, James… — Competition-Level Code Generation with AlphaCode
  63. Chengwu Liu, Jianhao Shen, Huajian Xin, Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295, 2023. 1
  64. Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zettlemoyer, and Veselin Stoyanov. Roberta: A robustly optimized BERT pretraining approach. CoRR, abs/1907.11692, 2019. URL http://arxiv.org/abs/1907.11692. ↗
  65. Sarah M. Loos, Geoffrey Irving, Christian Szegedy, and Cezary Kaliszyk. Deep network guided proof search. In Thomas Eiter and David Sands (eds.), LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 7-12, 2017, volume 46 of EPiC…
  66. EasyChair, 2017. doi: 10.29007/8mwc. URL https://doi.org/10.29007/8mwc. — [doi:10.29007/8mwc](https://doi.org/10.29007/8mwc) ↗
  67. Haipeng Luo, Qingfeng Sun, Can Xu, Pu Zhao, Jianguang Lou, Chongyang Tao, Xiubo Geng, Qingwei Lin, Shifeng Chen, and Dongmei Zhang. WizardMath: Empowering Mathematical Reasoning for Large Language Models via Reinforced Evol-Instruct, August 2023. URL http://arxiv.org/abs/2308.09583. arXiv:2308.0958… ↗
  68. Carlin MacKenzie, Jacques D. Fleuriot, and James Vaughan. An evaluation of the archive of formal proofs. CoRR, abs/2104.01052, 2021. URL https://arxiv.org/abs/2104.01052. — [arXiv:2104.01052](https://arxiv.org/abs/2104.01052) ↗
  69. The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pp. 367–381, New York, NY, USA, 2020. Association for Computing Machinery. ISBN 978-1-4503-7097-4. doi: 10.1145/ 3372885.3373824. URL https…
  70. John McCarthy, Marvin L Minsky, Nathaniel Rochester, and Claude E Shannon. A proposal for the dartmouth summer research project on artificial intelligence, august 31, 1955. AI magazine, 27(4): 12–12, 2006. find
  71. Norman Megill and David A Wheeler. Metamath: a computer language for mathematical proofs. Lulu Press, 2019. ISBN 978-0-359-70223-7. OCLC: 1105224041. 3 find
  72. Maciej Mikuła, Szymon Antoniak, Szymon Tworkowski, Albert Qiaochu Jiang, Jin Peng Zhou, Christian Szegedy, Łukasz Kuciński, Piotr Miłoś, and Yuhuai Wu. Magnushammer: A transformer-based approach to premise selection. arXiv preprint arXiv:2303.04488, 2023. 3 find
  73. OpenAI. GPT-4 technical report. CoRR, abs/2303.08774, 2023. doi: 10.48550/arXiv.2303.08774. URL https://doi.org/10.48550/arXiv.2303.08774. 2 ↗
  74. Joon Sung Park, Joseph C. O’Brien, Carrie J. Cai, Meredith Ringel Morris, Percy Liang, and Michael S. Bernstein. Generative agents: Interactive simulacra of human behavior, 2023. 3 find
  75. Lawrence C. Paulson. Isabelle a Generic Theorem Prover. Springer Verlag, 1994. 1, 3 find
  76. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020a. URL https://arxiv.org/abs/2009.03393. 1, 2, 3 ↗
  77. Stanislas Polu and Ilya Sutskever. Generative Language Modeling for Automated Theorem Proving. arXiv:2009.03393 [cs, stat], September 2020b. URL http://arxiv.org/abs/2009. 03393. arXiv: 2009.03393. ↗
  78. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal Mathematics Statement Curriculum Learning. (arXiv:2202.01344), February 2022. doi: 10.48550/arXiv.2202.01344. URL http://arxiv.org/abs/2202.01344. arXiv:2202.01344 [cs] type: article. 2, 3 ↗
  79. Jianing Qiu, Lin Li, Jiankai Sun, Jiachuan Peng, Peilun Shi, Ruiyang Zhang, Yinzhao Dong, Kyle Lam, Frank P-W Lo, Bo Xiao, et al. Large ai models in health informatics: Applications, challenges, and the future. arXiv preprint arXiv:2303.11568, 2023. — [arXiv:2303.11568](https://arxiv.org/abs/2303.11568) find
  80. Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical Reasoning via Self-supervised Skip-tree Training. September 2020. URL https://openreview.net/ forum?id=YmqAnY0CMEy. ↗
  81. Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. Mathematical reasoning via self-supervised skip-tree training. In 9th International Conference on Learning Representations, ICLR 2021, Virtual Event, Austria, May 3-7, 2021. find
  82. OpenReview.net, 2021. URL https://openreview.net/forum?id=YmqAnY0CMEy. ↗
  83. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language Models are Unsupervised Multitask Learners. pp. 24. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. 2018a. URL https… find
  84. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language models are unsupervised multitask learners. 2018b. URL https://d4mucfpksywv.cloudfront.net/better-language-models/language-models.pdf. ↗
  85. 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, 2020.
  86. Scott Reed, Konrad Zolna, Emilio Parisotto, Sergio Gomez Colmenarejo, Alexander Novikov, Gabriel Barth-Maron, Mai Gimenez, Yury Sulsky, Jackie Kay, Jost Tobias Springenberg, Tom Eccles, Jake Bruce, Ali Razavi, Ashley Edwards, Nicolas Heess, Yutian Chen, Raia Hadsell, Oriol Vinyals, Mahyar Bordbar, a… find
  87. Alexandre Riazanov and Andrei Voronkov. The design and implementation of vampire. AI communications, 15(2-3):91–110, 2002. find
  88. J. A. Robinson. A Machine-Oriented Logic Based on the Resolution Principle. Journal of the ACM, 12(1):23–41, 1965. ISSN 0004-5411. doi: 10.1145/321250.321253. URL https://doi.org/ 10.1145/321250.321253. find
  89. Stephan Schulz. E - a brainiac theorem prover. AI Communications, 15(2,3):111–126, August 2002. ISSN 0921-7126. find
  90. Yongliang Shen, Kaitao Song, Xu Tan, Dongsheng Li, Weiming Lu, and Yueting Zhuang. Hugginggpt: Solving ai tasks with chatgpt and its friends in hugging face, 2023. 3
  91. David Silver, Aja Huang, Chris J. Maddison, Arthur Guez, Laurent Sifre, George van den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, Ilya Sutskever, Timothy Lillicrap, Madeleine Leach, Koray Kavukc… find
  92. 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. Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm…
  93. Hugo Touvron, Thibaut Lavril, Gautier Izacard, Xavier Martinet, Marie-Anne Lachaux, Timothée Lacroix, Baptiste Rozière, Naman Goyal, Eric Hambro, Faisal Azhar, Aurelien Rodriguez, Armand Joulin, Edouard Grave, and Guillaume Lample. LLaMA: Open and Efficient Foundation Language Models, February 202…
  94. Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Nikolay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cristian Canton Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller,… — Llama 2: Open Foundation and Fine-Tuned Chat Models
  95. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. Attention is all you need. In Isabelle Guyon, Ulrike von Luxburg, Samy Bengio, Hanna M. Wallach, Rob Fergus, S. V. N. Vishwanathan, and Roman Garnett (eds.), Advances in Neur…
  96. Guanzhi Wang, Yuqi Xie, Yunfan Jiang, Ajay Mandlekar, Chaowei Xiao, Yuke Zhu, Linxi Fan, and Anima Anandkumar. Voyager: An open-ended embodied agent with large language models. arXiv preprint arXiv: Arxiv-2305.16291, 2023a. 3 find
  97. Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, et al. Dt-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In Proceedings of the 61st Annual Meeting of the Association for Computational… find
  98. Mingzhe Wang and Jia Deng. Learning to Prove Theorems by Learning to Generate Theorems. In Advances in Neural Information Processing Systems, volume 33, pp. 18146–18157. Curran Associates, Inc., 2020. URL https://proceedings.neurips.cc/paper/2020/hash/ d2a27e83d429f0dcae6b937cf440aeb1-Abstract.html. ↗
  99. Qingxiang Wang, Cezary Kaliszyk, and Josef Urban. First experiments with neural translation of informal to formal mathematics. In Intelligent Computer Mathematics: 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings 11, pp. 255–270. find
  100. Zhenhailong Wang, Shaoguang Mao, Wenshan Wu, Tao Ge, Furu Wei, and Heng Ji. Unleashing cognitive synergy in large language models: A task-solving agent through multi-persona self-collaboration, 2023c. 3 find
  101. Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, and Patrick Wischnewski. Spass version 3.5. In Renate A. Schmidt (ed.), Automated Deduction – CADE-22, pp. 140–145, Berlin, Heidelberg, 2009. Springer Berlin Heidelberg. ISBN 978-3-642-02959-2. find
  102. Daniel Whalen. Holophrasm: a neural automated theorem prover for higher-order logic. CoRR, abs/1608.02644, 2016a. URL http://arxiv.org/abs/1608.02644. ↗
  103. Daniel Whalen. Holophrasm: a neural Automated Theorem Prover for higher-order logic. Technical Report arXiv:1608.02644, arXiv, August 2016b. URL http://arxiv.org/abs/1608. 02644. arXiv:1608.02644 [cs] type: article. ↗
  104. Wikipedia contributors. Recursion (computer science) — Wikipedia, the free encyclopedia, 2023. URL https://en.wikipedia.org/w/index.php?title=Recursion_ (computer_science)&oldid=1143431394. [Online; accessed 14-May-2023]. ↗
  105. Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, and Roger Grosse. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving. ICLR 2021, April 2021. URL http://arxiv.org/abs/2007.02924. arXiv: 2007.02924. ↗
  106. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353–32368, 2022. 3, 6, 7
  107. Jing Xiong, Chengming Li, Min Yang, Xiping Hu, and Bin Hu. Expression syntax information bottleneck for math word problems. In Enrique Amigó, Pablo Castells, Julio Gonzalo, Ben Carterette, J. Shane Culpepper, and Gabriella Kazai (eds.), SIGIR ’22: The 45th International ACM SIGIR Conference on Rese…
  108. ACM, 2022. doi: 10.1145/3477495.3531824. URL https://doi.org/10.1145/3477495.3531824. — [doi:10.1145/3477495.3531824](https://doi.org/10.1145/3477495.3531824) ↗
  109. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.), Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA, volume 97 of Proceedings of…
  110. PMLR, 2019. URL http://proceedings.mlr.press/v97/yang19a.html. ↗
  111. 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. arXiv preprint arXiv:2306.15626, 2023. 1, 2
  112. Longhui Yu, Weisen Jiang, Han Shi, Jincheng Yu, Zhengying Liu, Yu Zhang, James T. Kwok, Zhenguo Li, Adrian Weller, and Weiyang Liu. Metamath: Bootstrap your own mathematical questions for large language models, 2023.
  113. Zahra Zahedi and Subbarao Kambhampati. Human-ai symbiosis: A survey of current approaches, 2021. 3 find
  114. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Decomposing the enigma: Subgoal-based demonstration learning for formal theorem proving. arXiv preprint arXiv:2305.16366, 2023. 1, 2, 3, 5, 6, 7 find
  115. Chuanyang Zheng, Zhengying Liu, Enze Xie, Zhenguo Li, and Yu Li. Progressive-hint prompting improves reasoning in large language models. arXiv preprint arXiv:2304.09797, 2023.
  116. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics. September 2021. URL https://openreview.net/ forum?id=9ZPegFuFTFv. 2, 6 ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wang-2023-lego-prover-neural-theorem-proving/