Elamur Research⌕
☰
home / papers / 2023 / DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function

DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function

Paper · 2023 · Haiming Wang, Ye Yuan, Zhengying Liu et al.

Summary

Neural theorem provers usually combine a language model that proposes the next tactic with a tree search that assembles a full proof. Systems in the GPT-f line give every proof state the same effort and expand each node only once. Their search can therefore stop early when no generated candidate applies, and they judge states in isolation. DT-Solver addresses these weaknesses. A policy model trained on formal library data suggests tactics. A Monte-Carlo-style search attaches a virtual child to each node, so a state can be re-expanded and the tree widened when needed. A modified PUCT score steers compute toward promising but difficult states. A RoBERTa critic is trained on trajectories collected from successful searches over the training theorems. It estimates whether the whole proof path is heading toward success, instead of scoring a single step. On PISA (Isabelle) and Mathlib (Lean), DT-Solver beats prior state-of-the-art methods by 6.65% success rate on average. The gain rises to 11.03% under low compute, which matters for teams without huge GPU budgets.

Key points

  • Benchmarks are PISA (Isabelle) and Mathlib (Lean), evaluated with a 300-second time budget per theorem. The average success-rate gain is 6.65% overall and 11.03% in low-resource settings.
  • Dynamic-tree sampling with virtual nodes lets a node be expanded repeatedly. This avoids premature "empty queue" failures and raises the pass rate from 39.9% to 48.4%.
  • The proof-level value function (a RoBERTa critic) improves value-prediction accuracy from 63.6% to 70.7% compared with a step-level estimate.
  • Feeding the critic the full trajectory caused truncation in 53.00% of queries. A "root-state-and-current-state" input cut truncation to 3.10%.
  • In the authors' assessment, the main limitation is the weak policy model, which often fails to propose correct steps even when the critic picks the right state to expand.

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

🎓Peking UniversityBeijing · China335 works · 43,758 citations🏢Huawei TechnologiesShenzhen · China105 works · 15,705 citations🎓Mohamed bin Zayed University of Artificial IntelligenceAbu Dhabi · United Arab Emirates145 works · 6,810 citations🎓Sun Yat-sen UniversityGuangzhou · China80 works · 9,799 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksArts and Humanities · 17,959 worksLanguage and Linguistics · 17,789 works

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

Cite

Cite as Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li and Xiaodan Liang. 2023. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2023.acl-long.706

@inproceedings{wang2023dt,
  title = {{DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function}},
  author = {Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin, Zhenguo Li and Xiaodan Liang},
  booktitle = {Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)},
  year = {2023},
  doi = {10.18653/v1/2023.acl-long.706},
  url = {https://doi.org/10.18653/v1/2023.acl-long.706}
}

References

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

  1. Alexander A. Alemi, François Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, and Josef Urban. 2016. DeepMath - deep sequence models for premise selection. In Proceedings of the 30th International Conference on Neural Information Processing Systems, NIPS’16, pages 2243–2251, Red Hook, NY, US…
  2. Kshitij Bansal, Christian Szegedy, Markus Norman Rabe, Sarah M. Loos, and Viktor Toman. 2020. Learning to Reason in Large Theories without Imitation.
  3. Bruno Barras, Samuel Boutin, Cristina Cornes, Ju-dicaë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. 1997. The Coq Proof Assistant Reference Manual : Versi… find
  4. Alexander Bentkamp, Jasmin Blanchette, Sophie Tour-ret, and Petar Vukmirović. 2021. Superposition for Full Higher-order Logic. In Automated Deduction – CADE 28, Lecture Notes in Computer Science, pages 396–412, Cham. find
  5. Springer International Publishing. 2022. HyperTree Proof Search for Neural Theorem Proving. Technical Report arXiv:2205.11491, arXiv. ArXiv:2205.11491 [cs] type: article.
  6. Yann LeCun, Yoshua Bengio, and Geoffrey Hinton. 2015. Deep learning. Nature, 521(7553):436–444. Number: 7553 Publisher: Nature Publishing Group. find
  7. Wenda Li, Lei Yu, Yuhuai Wu, and Lawrence C. Paulson. 2020. IsarStep: a Benchmark for High-level Mathematical Reasoning. In ICLR 2021.
  8. Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science, pages 337–340, Berlin, Heidelberg. Springer. find
  9. Yinhan Liu, Myle Ott, Naman Goyal, Jingfei Du, Mandar Joshi, Danqi Chen, Omer Levy, Mike Lewis, Luke Zettlemoyer, and Veselin Stoyanov. 2019. Roberta: A robustly optimized BERT pretraining approach. CoRR, abs/1907.11692.
  10. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. 2015. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25, Lecture Notes in Computer Science, pages 378–388, Cham. Springer International Publishing. find
  11. John McCarthy, Marvin L Minsky, Nathaniel Rochester, and Claude E Shannon. 2006. A proposal for the dartmouth summer research project on artificial intelligence, august 31, 1955. AI magazine, 27(4):12–12. find
  12. 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. 2020. The Pile: An 800gb dataset of diverse text for language modeling. arXiv preprint arXiv:2101.00027. find
  13. Jesse Michael Han, Jason Rute, Yuhuai Wu, Edward W. Ayers, and Stanislas Polu. 2021. Proof Artifact Co-training for Theorem Proving with Language Models.
  14. John Harrison, Josef Urban, and Freek Wiedijk. 2014. History of interactive theorem proving. In Computational Logic, volume 9, pages 135–214.
  15. William Alvin Howard. 1980. The Formulae-as-Types Notion of Construction. In Haskell Curry, Hindley B, Seldin J. Roger, and P. Jonathan, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press. find
  16. Albert Q Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. 2022. Thor: Wielding hammers to integrate language models and automated theorem provers. arXiv preprint arXiv:2205.10893.
  17. Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. 2021. Lisa: Language models of isabelle proofs. find
  18. Laura Kovács and Andrei Voronkov. 2013. First-Order Theorem Proving and Vampire. In Computer Aided Verification, Lecture Notes in Computer Science, pages 1–35, Berlin, Heidelberg. Springer. find
  19. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. find
  20. NORMAN. WHEELER MEGILL and DAVID A. 2019. METAMATH: a computer language for mathematical proofs. Lulu Press, Place of publication not identified. OCLC: 1105224041.
  21. Lawrence C. Paulson. 1994. Isabelle a Generic Theorem Prover. Springer Verlag. find
  22. Stanislas Polu, Jesse Michael Han, Kunhao Zheng, Mantas Baksys, Igor Babuschkin, and Ilya Sutskever. 2022. Formal Mathematics Statement Curriculum Learning. Technical Report arXiv:2202.01344, arXiv. ArXiv:2202.01344 [cs] type: article.
  23. Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. arXiv:2009.03393 [cs, stat]. ArXiv: 2009.03393.
  24. Markus Norman Rabe, Dennis Lee, Kshitij Bansal, and Christian Szegedy. 2020. Mathematical Reasoning via Self-supervised Skip-tree Training.
  25. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. Language Models are Unsupervised Multitask Learners. page 24. find
  26. Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, and Ilya Sutskever. 2018. Language models are unsupervised multitask learners. find
  27. 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
  28. Stephan Schulz. 2002. E - a brainiac theorem prover. AI Communications, 15(2,3):111–126. find
  29. 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
  30. 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. 2017. Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Alg…
  31. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N. Gomez, Lukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. In Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017,…
  32. Mingzhe Wang and Jia Deng. 2020. Learning to Prove Theorems by Learning to Generate Theorems. In Advances in Neural Information Processing Systems, volume 33, pages 18146–18157. Curran Associates, Inc.
  33. Daniel Whalen. 2016. Holophrasm: a neural Automated Theorem Prover for higher-order logic. Technical Report arXiv:1608.02644, arXiv. ArXiv:1608.02644 [cs] type: article.
  34. Yuhuai Wu, Albert Qiaochu Jiang, Jimmy Ba, and Roger Grosse. 2021. INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving.
  35. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2021. miniF2F: a cross-system benchmark for formal Olympiad-level mathematics.

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/wang-2023-dt-solver-automated-theorem-proving/