@inproceedings{wang-etal-2023-dt,
    title = "{DT}-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function",
    author = "Wang, Haiming  and
      Yuan, Ye  and
      Liu, Zhengying  and
      Shen, Jianhao  and
      Yin, Yichun  and
      Xiong, Jing  and
      Xie, Enze  and
      Shi, Han  and
      Li, Yujun  and
      Li, Lin  and
      Yin, Jian  and
      Li, Zhenguo  and
      Liang, Xiaodan",
    editor = "Rogers, Anna  and
      Boyd-Graber, Jordan  and
      Okazaki, Naoaki",
    booktitle = "Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)",
    month = jul,
    year = "2023",
    address = "Toronto, Canada",
    publisher = "Association for Computational Linguistics",
    url = "https://aclanthology.org/2023.acl-long.706",
    doi = "10.18653/v1/2023.acl-long.706",
    pages = "12632--12646",
    abstract = "Recent advances in neural theorem-proving resort to large language models and tree searches. When proving a theorem, a language model advises single-step actions based on the current proving state and the tree search finds a sequence of correct steps using actions given by the language model. However, prior works often conduct constant computation efforts for each proving state while ignoring that the hard states often need more exploration than easy states. Moreover, they evaluate and guide the proof search solely depending on the current proof state instead of considering the whole proof trajectory as human reasoning does. Here, to accommodate general theorems, we propose a novel Dynamic-Tree Driven Theorem Solver (DT-Solver) by guiding the search procedure with state confidence and proof-level values. Specifically, DT-Solver introduces a dynamic-tree Monte-Carlo search algorithm, which dynamically allocates computing budgets for different state confidences, guided by a new proof-level value function to discover proof states that require substantial exploration. Experiments on two popular theorem-proving datasets, PISA and Mathlib, show significant performance gains by our DT-Solver over the state-of-the-art approaches, with a 6.65{\%} improvement on average in terms of success rate. And especially under low computing resource settings (11.03{\%} improvement on average).",
}

Recent advances in neural theorem-proving resort to large language models and tree searches. When proving a theorem, a language model advises single-step actions based on the current proving state and the tree search finds a sequence of correct steps using actions given by the language model. However, prior works often conduct constant computation efforts for each proving state while ignoring that the hard states often need more exploration than easy states. Moreover, they evaluate and guide the proof search solely depending on the current proof state instead of considering the whole proof trajectory as human reasoning does. Here, to accommodate general theorems, we propose a novel Dynamic-Tree Driven Theorem Solver (DT-Solver) by guiding the search procedure with state confidence and proof-level values. Specifically, DT-Solver introduces a dynamic-tree Monte-Carlo search algorithm, which dynamically allocates computing budgets for different state confidences, guided by a new proof-level value function to discover proof states that require substantial exploration. Experiments on two popular theorem-proving datasets, PISA and Mathlib, show significant performance gains by our DT-Solver over the state-of-the-art approaches, with a 6.65{\%} improvement on average in terms of success rate. And especially under low computing resource settings (11.03{\%} improvement on average).
Wang, Haiming Yuan, Ye Liu, Zhengying Shen, Jianhao Yin, Yichun Xiong, Jing Xie, Enze Shi, Han Li, Yujun Li, Lin Yin, Jian Li, Zhenguo Liang, Xiaodan
DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function