Elamur Research⌕
☰
home / papers / 2024 / Proving Theorems Recursively

Proving Theorems Recursively

Paper · 2024 · Haiming Wang, Huajian Xin, Zhengying Liu et al.

Summary

Neural theorem provers usually build proofs one step at a time. A language model proposes the next tactic, and a search procedure ranks candidates with local scores such as log-probability, value estimates, or PUCT. These myopic signals often send the search into irrelevant intermediate goals, which makes long proofs hard to reach. POETRY (PrOvE Theorems RecursivelY) addresses this in the Isabelle prover. At each proof level it first looks for an outline that Isabelle can verify, with the proofs of intermediate conjectures left as the sorry placeholder. Those deferred conjectures are then attacked in the same way at deeper levels, until no placeholder remains. If a sketch relies on a false conjecture, it fails at the lower level and the search moves on to another sketch. The model is trained on data where proofs are split by Isabelle's proof level. On miniF2F and PISA, POETRY beats earlier methods and finds much longer proofs than step-by-step search. This shows that hierarchical decomposition helps neural provers scale to harder problems.

Key points

  • POETRY reached a 42.2% pass rate on the miniF2F valid and test splits. This is a 5.1% absolute gain on average over the previous state of the art.
  • In ablation, recursive proving gave an average 3.9% absolute gain over step-by-step GPT-f-style baselines.
  • On PISA, the longest proof found grew from 10 steps (step-by-step baseline) to 26 steps.
  • In one case study, an 11-step proof that the baseline could not find within the 600-second limit was split into 3 sketches, none longer than 4 steps.
  • The method is built on Isabelle/Isar proof levels. The authors argue it could carry over to Lean (sorry) or Coq (Admitted) with extra engineering, and they offer no theoretical guarantee against exponential search growth.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Fields, topics and concepts

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

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

Cite

Cite as Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li and Xiaodan Liang. 2024. Proving Theorems Recursively. arXiv:2405.14414.

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

@misc{wang2024proving,
  title = {{Proving Theorems Recursively}},
  author = {Haiming Wang, Huajian Xin, Zhengying Liu, Wenda Li, Yinya Huang, Jianqiao Lu, Zhicheng Yang, Jing Tang, Jian Yin, Zhenguo Li and Xiaodan Liang},
  year = {2024},
  doi = {10.48550/arxiv.2405.14414},
  eprint = {2405.14414},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2405.14414}
}

References

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

  1. Z. Azerbayev, B. Piotrowski, H. Schoelkopf, E. W. Ayers, D. Radev, and J. Avigad. Proofnet: Autoformalizing and formally proving undergraduate-level mathematics, 2023. 6, 14
  2. B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saïbi, and B. Werner. The Coq Proof Assistant Reference Manual : Version 6.1. report, INRIA, May 1997. URL https://hal.inria.fr/inria-00069968. Pages… ↗
  3. M. Chen, J. Tworek, H. Jun, Q. Yuan, H. P. de Oliveira Pinto, J. Kaplan, H. Edwards, Y. Burda, N. Joseph, G. Brockman, A. Ray, R. Puri, G. Krueger, M. Petrov, H. Khlaaf, G. Sastry, P. Mishkin, B. Chan, S. Gray, N. Ryder, M. Pavlov, A. Power, L. Kaiser, M. Bavarian, C. Winter, P. Tillet, F. P. Such,… — Evaluating Large Language Models Trained on Code
  4. K. Czechowski, T. Odrzygóźdź, M. Zbysiński, M. Zawalski, K. Olejnik, Y. Wu, Łukasz Kuciński, and P. Miłoś. Subgoal search for complex reasoning tasks, 2024. 9 find
  5. R. B. e. a. Daniel Selsam, Kevin Buzzard. imo-grand-challenge.github.io/. 6 Imo grand challenge. 2019. find
  6. URL https://L.de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer. The Lean Theorem Prover (System Description). In A. P. Felty and A. Middeldorp, editors, Automated Deduction - CADE-25, Lecture Notes in Computer Science, pages 378–388, Cham, 2015. Springer International Publishing. ISBN… ↗
  7. J. Devlin, M. Chang, K. Lee, and K. Toutanova. BERT: pre-training of deep bidirectional transformers for language understanding. In J. Burstein, C. Doran, and T. Solorio, editors, Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human…
  8. R. Dunford, Q. Su, and E. Tamang. The pareto principle. The Race, 2021. URL https://api.semanticscholar.org/CorpusID:15925174. 15 ↗
  9. E. First, M. N. Rabe, T. Ringer, and Y. 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. 9 ↗
  10. L. Gao, S. Biderman, S. Black, L. Golding, T. Hoppe, C. Foster, J. Phang, H. He, A. Thite, N. Nabeshima, S. Presser, and C. Leahy. The pile: An 800gb dataset of diverse text for language modeling, 2020. 6 find
  11. L. Gesellensetter, S. Glesner, and E. Salecker. Formal verification with isabelle/hol in practice: finding a bug in the gcc scheduler. In Formal Methods for Industrial Critical Systems: 12th International Workshop, FMICS 2007, Berlin, Germany, July 1-2, 2007, Revised Selected Papers 12, pages 85–100… find
  12. J. M. Han, J. Rute, Y. Wu, E. W. Ayers, and S. 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.
  13. OpenReview.net, 2022. URL https://openreview.net/forum?id=rpxJc9j04U. 1, 2, 6, 7, 9 ↗
  14. J. Harrison. HOL light: An overview. In S. Berghofer, T. Nipkow, C. Urban, and M. Wenzel, editors, 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 Science, pages 60–66. find
  15. Springer, 2009. doi: 10.1007/978-3-642-03359-9\\_4. URL https://doi.org/10.1007/978-3-642-03359-9_4. 3 — [doi:10.1007/978-3-642-03359-9\\_4](https://doi.org/10.1007/978-3-642-03359-9_4) ↗
  16. D. Hendrycks, C. Burns, S. Kadavath, A. Arora, S. Basart, E. Tang, D. Song, and J. Steinhardt. Measuring mathematical problem solving with the math dataset, 2021. 6
  17. Y. Huang, X. Lin, Z. Liu, Q. Cao, H. Xin, H. Wang, Z. Li, L. Song, and X. Liang. Mustard: Mastering uniform synthesis of theorem and proof data, 2024. 1, 9
  18. A. Q. Jiang, W. Li, J. M. Han, and Y. Wu. Lisa: Language models of isabelle proofs. 2021. 1, 3, 6, 9, 15 find
  19. A. Q. Jiang, W. Li, S. Tworkowski, K. Czechowski, T. Odrzygóźdź, P. Miłoś, Y. Wu, and M. Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. arXiv preprint arXiv:2205.10893, 2022a. 1, 2, 4, 6, 7, 8, 9, 15
  20. A. Q. Jiang, S. Welleck, J. P. Zhou, W. Li, J. Liu, M. Jamnik, T. Lacroix, Y. Wu, and G. 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.48550/arXiv.2210. 12283. 1, 6, 9 ↗
  21. G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207–220, 2009. 3 find
  22. G. Lample, M.-A. Lachaux, T. Lavril, X. Martinet, A. Hayat, G. Ebner, A. Rodriguez, and T. 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.11491 [cs] type: article. 1, 2, 6, 8, 9 ↗
  23. A. Lewkowycz, A. Andreassen, D. Dohan, E. Dyer, H. Michalewski, V. V. Ramasesh, A. Slone, C. Anil, I. Schlag, T. Gutman-Solo, Y. Wu, B. Neyshabur, G. Gur-Ari, and V. Misra. Solving quantitative reasoning problems with language models. In NeurIPS, 2022. URL http://papers.nips.cc/paper_files/paper/202… ↗
  24. C. Liu, J. Shen, H. Xin, Z. Liu, Y. Yuan, H. Wang, W. Ju, C. Zheng, Y. Yin, L. Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprint arXiv:2309.04295, 2023. 1
  25. C. MacKenzie, J. Fleuriot, and J. Vaughan. An evaluation of the archive of formal proofs, 2021. 6 find
  26. M. Mikuła, S. Antoniak, S. Tworkowski, A. Q. Jiang, J. P. Zhou, C. Szegedy, Ł. Kuciński, P. Miłoś, and Y. Wu. Magnushammer: A transformer-based approach to premise selection. arXiv preprint arXiv:2303.04488, 2023. 6, 7, 8
  27. T. Nipkow, M. Wenzel, and L. C. Paulson. Isabelle/HOL: a proof assistant for higher-order logic. Springer-Verlag, Berlin, Heidelberg, 2002. ISBN 3540433767. 6 find
  28. 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. 6 ↗
  29. L. C. Paulson. Isabelle a Generic Theorem Prover. Springer Verlag, 1994. 3, 9 find
  30. L. C. Paulson. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In R. A. Schmidt, S. Schulz, and B. Konev, editors, Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, PAAR-2010, Edinburgh, Scotland, UK, July 14… find
  31. EasyChair, 2010. doi: 10.29007/TNFD. URL https://doi.org/10.29007/tnfd. 6 ↗
  32. S. Polu and I. Sutskever. Generative language modeling for automated theorem proving. CoRR, abs/2009.03393, 2020. URL https://arxiv.org/abs/2009.03393. 1, 2, 3, 6, 9 ↗
  33. S. Polu, J. M. Han, K. Zheng, M. Baksys, I. Babuschkin, and I. Sutskever. Formal Mathematics Statement Curriculum Learning. (arXiv:2202.01344), Feb. 2022. doi: 10.48550/arXiv.2202.01344. URL http://arxiv.org/abs/2202.01344. arXiv:2202.01344 [cs] type: article. 1, 2, 6, 7, 8, 9 ↗
  34. D. Silver, A. Huang, C. J. Maddison, A. Guez, L. Sifre, G. van den Driessche, J. Schrittwieser, I. Antonoglou, V. Panneershelvam, M. Lanctot, S. Dieleman, D. Grewe, J. Nham, N. Kalchbrenner, I. Sutskever, T. Lillicrap, M. Leach, K. Kavukcuoglu, T. Graepel, and D. Hassabis. Mastering the game of Go w… find
  35. A. Thakur, G. Tsoukalas, Y. Wen, J. Xin, and S. Chaudhuri. An in-context learning agent for formal theorem-proving, 2024. 1, 6, 7
  36. G. Wang, Y. Xie, Y. Jiang, A. Mandlekar, C. Xiao, Y. Zhu, L. Fan, and A. Anandkumar. Voyager: An open-ended embodied agent with large language models. arXiv preprint arXiv: Arxiv-2305.16291, 2023a. 9 find
  37. H. Wang, H. Xin, C. Zheng, L. Li, Z. Liu, Q. Cao, Y. Huang, J. Xiong, H. Shi, E. Xie, J. Yin, Z. Li, H. Liao, and X. Liang. Lego-prover: Neural theorem proving with growing libraries, 2023b. 1, 6, 9
  38. H. Wang, Y. Yuan, Z. Liu, J. Shen, Y. Yin, J. Xiong, E. Xie, H. Shi, Y. Li, L. 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 Linguistics (Volume 1: Long P…
  39. J. Wei, X. Wang, D. Schuurmans, M. Bosma, B. Ichter, F. Xia, E. Chi, Q. Le, and D. Zhou. Chain-of-thought prompting elicits reasoning in large language models, 2023. 9
  40. M. Wenzel et al. The isabelle/isar reference manual, 2004. 3 find
  41. Y. Wu, A. Q. Jiang, W. Li, M. Rabe, C. Staats, M. Jamnik, and C. Szegedy. Autoformalization with large language models. Advances in Neural Information Processing Systems, 35:32353–32368, 2022. 6, 7, 8
  42. J. Xiong, J. Shen, Y. Yuan, H. Wang, Y. Yin, Z. Liu, L. Li, Z. Guo, Q. Cao, Y. Huang, C. Zheng, X. Liang, M. Zhang, and Q. Liu. Trigo: Benchmarking formal mathematical proof reduction for generative language models, 2023. 1
  43. K. Yang, A. M. Swope, A. Gu, R. Chalamala, P. Song, S. Yu, S. Godil, R. Prenger, and A. Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models. arXiv preprint arXiv:2306.15626, 2023. 1, 2, 6, 7, 8, 9
  44. L. Zhang, S. Lu, and N. Duan. Selene: Pioneering automated proof in software verification, 2024. 3 find
  45. C. Zheng, H. Wang, E. Xie, Z. Liu, J. Sun, H. Xin, J. Shen, Z. Li, and Y. Li. Lyra: Orchestrating dual correction in automated theorem proving, 2023. 6, 9
  46. K. Zheng, J. M. Han, and S. Polu. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics. Sept. 2021. URL https://openreview.net/forum?id=9ZPegFuFTFv. 3, 6 ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wang-2024-proving-theorems-recursively/