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, pages 12632–12646 July 9-14, 2023 ©2023 Association for Computational Linguistics DT-Solver: Automated Theorem Proving with Dynamic-Tree Sampling Guided by Proof-level Value Function Haiming Wang1∗, Ye Yuan2, Zhengying Liu3 Jianhao Shen2, Yichun Yin3, Jing Xiong1, Enze Xie3, Han Shi3, Yujun Li3, Lin Li3, Jian Yin1†, Zhenguo Li3, Xiaodan Liang1,4† 1Sun Yat-sen University, 2Peking University, 3Huawei Noah’s Ark Lab, 4MBZUAI {wanghm39,xiongj69}@mail2.sysu.edu.cn, {yuanye_pku,jhshen}@pku.edu.cn, {liuzhengying2,yinyichun,xie.enze,shi.han}@huawei.com {liyujun9,lilin29,Li.Zhenguo}@huawei.com issjyin@mail.sysu.edu.cn, xdliang328@gmail.com Abstract Recent advances in neural theorem-proving re- sort to large language models and tree searches. When proving a theorem, a language model advises single-step actions based on the cur- rent 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 pro- pose a novel Dynamic-Tree Driven Theorem Solver (DT-Solver) by guiding the search pro- cedure with state confidence and proof-level values. Specifically, DT-Solver introduces a dynamic-tree Monte-Carlo search algorithm, which dynamically allocates computing bud- gets 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% im- provement on average in terms of success rate. And especially under low computing resource settings (11.03% improvement on average). 1 Introduction Automated theorem proving (ATP) (Harrison et al., 2014) has been considered an essential task of Arti- ficial Intelligence (AI) ever since the birth of mod- ern AI (McCarthy et al., 2006). Besides its re- markable theoretical value and huge potential to accelerate research in mathematics, ATP already demonstrates excellent application value in, for ex- †Corresponding authors. ∗Work done during internship in Huawei Noah’s Ark Lab Figure 1: Illustration of a theorem and its proof in Lean (de Moura et al., 2015). The theorem sub_ne_zero_of_ne states that if the hypothesis h holds (i.e. we have a ̸= b), then we have a − b ̸= 0. Three proof steps are used to prove this theorem. After the keyword begin, a proof state (containing one or several goals) is initialized. Then each proof step is applied to the current proof state to obtain a new one until a proof state ‘goals accomplished’ is reached, which marks the success of the proof. ample, formal verification (Barras et al., 1997) and code generation (Howard, 1980). In general, the goal of a theorem proving task is to construct a proof (a sequence of proof steps) that proves a given theorem (often within a given time budget, e.g. 300 seconds). The validity of this proof is verified by a formal environment …

Content truncated to 500 words