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

Haiming Wang, Ye Yuan, Zhengying Liu, Jianhao Shen, Yichun Yin, Jing Xiong, Enze Xie, Han Shi, Yujun Li, Lin Li, Jian Yin 0001, Zhenguo Li, Xiaodan Liang. DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function. In Anna Rogers, Jordan L. Boyd-Graber, Naoaki Okazaki, editors, Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023. pages 12632-12646, Association for Computational Linguistics, 2023. [doi]

@inproceedings{WangYLSYXXSLL0L23,
  title = {DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function},
  author = {Haiming Wang and Ye Yuan and Zhengying Liu and Jianhao Shen and Yichun Yin and Jing Xiong and Enze Xie and Han Shi and Yujun Li and Lin Li and Jian Yin 0001 and Zhenguo Li and Xiaodan Liang},
  year = {2023},
  url = {https://aclanthology.org/2023.acl-long.706},
  researchr = {https://researchr.org/publication/WangYLSYXXSLL0L23},
  cites = {0},
  citedby = {0},
  pages = {12632-12646},
  booktitle = {Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023},
  editor = {Anna Rogers and Jordan L. Boyd-Graber and Naoaki Okazaki},
  publisher = {Association for Computational Linguistics},
  isbn = {978-1-959429-72-2},
}