Elamur Research⌕
☰
home / papers / 2024 / SubgoalXL: Subgoal-based Expert Learning for Theorem Proving

SubgoalXL: Subgoal-based Expert Learning for Theorem Proving

Paper · 2024 · Xueliang Zhao, Lin Zheng, Haige Bo et al.

Summary

SubgoalXL targets two obstacles for LLM-based formal theorem proving in Isabelle: proof data in this domain is scarce, and models struggle with long multi-step reasoning. Rather than gathering massive synthetic corpora, the authors aim to get more value out of a small amount of human-written material. Informal proofs are replaced by "subgoal-based proofs": step-by-step natural-language plans in which each step matches an intermediate Isabelle goal. These are annotated with GPT-4o, guided by hand-built examples. An expert learning loop then repeatedly retrains three cooperating models, one producing formal statements, one producing formal proofs and one producing subgoals. Each model is fine-tuned on data drawn from estimated optimal distributions, and the models score one another by how likely they are to reconstruct each other's outputs. Only the proof generator is used at test time. The system sets a new Isabelle record on miniF2F-test. This suggests that careful supervision and data efficiency can rival approaches built on far more synthetic data.

Key points

  • On miniF2F-test, SubgoalXL reaches 56.1% in Isabelle, an absolute gain of 4.9 points over the previous best, Lyra. On miniF2F-valid it scores 61.9%.
  • It solves 41 AMC12, 9 AIME and 3 IMO problems from miniF2F.
  • An auxiliary posterior subgoal generator, conditioned on the formal proof, evaluates the formal proof generator during training.
  • The system is built on Llama-3 with roughly 38k synthesized theorems and a search budget of 16,384. Lean systems such as DeepSeek-Prover-V1.5 use about 9B tokens of synthetic data, yet SubgoalXL still beats InternLM2-StepProver (54.5%) and DeepSeek-Prover (50.0%) on the test split.
  • Code is released at github.com/zhaoxlpku/SubgoalXL.

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 Hong KongPok Fu Lam · China127 works · 13,824 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 Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker and Lingpeng Kong. 2024. SubgoalXL: Subgoal-based Expert Learning for Theorem Proving. arXiv:2408.11172.

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

@misc{zhao2024subgoalxl,
  title = {{SubgoalXL: Subgoal-based Expert Learning for Theorem Proving}},
  author = {Xueliang Zhao, Lin Zheng, Haige Bo, Changran Hu, Urmish Thakker and Lingpeng Kong},
  year = {2024},
  doi = {10.48550/arxiv.2408.11172},
  eprint = {2408.11172},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2408.11172}
}

References

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

  1. Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichiro Nakano, et al. Training verifiers to solve math word problems. arXiv preprint arXiv:2110.14168, 2021.
  2. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris Van Doorn, and Jakob von Raumer. The lean theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pp. 378–388. find
  3. Emily First, Markus N Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. arXiv preprint arXiv:2303.04910, 2023.
  4. Jiatao Gu, James Bradbury, Caiming Xiong, Victor O.K. Li, and Richard Socher. Non-autoregressive neural machine translation. In International Conference on Learning Representations, 2018. URL https://openreview.net/forum?id=B1l8BtlCb. ↗
  5. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W Ayers, and Stanislas Polu. Proof artifact co-training for theorem proving with language models. arXiv preprint arXiv:2102.06203, 2021.
  6. Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2103.03874, 2021.
  7. 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. arXiv preprint arXiv:2210.12283, 2022a.
  8. Albert Qiaochu 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. Advances in Neural Information Processing Systems, 35: 8360–8373, 2022b.
  9. 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. Advances in Neural Information Processing Systems, 35:26337–26349, 2022.
  10. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, et al. Solving quantitative reasoning problems with language models. arXiv preprint arXiv:2206.14858, 2022.
  11. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C Paulson. Modelling high-level mathematical reasoning in mechanised declarative proofs. arXiv preprint arXiv:2006.09265, 2020.
  12. Haohan Lin, Zhiqing Sun, Yiming Yang, and Sean Welleck. Lean-star: Learning to interleave thinking and proving. arXiv preprint arXiv:2407.10040, 2024.
  13. 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.
  14. Lawrence C Paulson. Isabelle: A generic theorem prover. Springer, 1994. find
  15. Lawrence C Paulsson and Jasmin C Blanchette. Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers. In Proceedings of the 8th International Workshop on the Implementation of Logics (IWIL-2010), Yogyakarta, Indonesia. EPiC, volume 2, 2012. find
  16. Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020.
  17. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. Formal mathematics statement curriculum learning. arXiv preprint arXiv:2202.01344, 2022.
  18. John Schulman, Nicolas Heess, Theophane Weber, and Pieter Abbeel. Gradient estimation using stochastic computation graphs. Advances in neural information processing systems, 28, 2015. find
  19. David Silver, Aja Huang, Chris J Maddison, Arthur Guez, Laurent Sifre, George Van Den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, et al. Mastering the game of go with deep neural networks and tree search. nature, 529(7587):484–489, 2016. find
  20. 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.
  21. Zijian Wu, Jiayu Wang, Dahua Lin, and Kai Chen. Lean-github: Compiling github lean repositories for a versatile lean prover. arXiv preprint arXiv:2407.17227, 2024.
  22. Huajian Xin, Haiming Wang, Chuanyang Zheng, Lin Li, Zhengying Liu, Qingxing Cao, Yinya Huang, Jing Xiong, Han Shi, Enze Xie, et al. Lego-prover: Neural theorem proving with growing libraries. arXiv preprint arXiv:2310.00656, 2023.
  23. Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, and Xiaodan Liang. Deepseek-prover: Advancing theorem proving in llms through large-scale synthetic data. arXiv preprint arXiv:2405.14333, 2024a.
  24. Huajian Xin, ZZ Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, et al. Deepseek-prover-v1. 5: Harnessing proof assistant feedback for reinforcement learning and monte-carlo tree search. arXiv preprint arXiv:2408.08152, 2024b.
  25. Xueliang Zhao, Wenda Li, and Lingpeng Kong. Subgoal-based demonstration learning for formal theorem proving. In Ruslan Salakhutdinov, Zico Kolter, Katherine Heller, Adrian Weller, Nuria Oliver, Jonathan Scarlett, and Felix Berkenkamp (eds.), Proceedings of the 41st International Conference on Machin… find
  26. Chuanyang Zheng, Haiming Wang, Enze Xie, Zhengying Liu, Jiankai Sun, Huajian Xin, Jianhao Shen, Zhenguo Li, and Yu Li. Lyra: Orchestrating dual correction in automated theorem proving. arXiv preprint arXiv:2309.15806, 2023.
  27. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: a cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.00110, 2021.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zhao-2024-subgoalxl-subgoal-based-expert-learning/