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

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).

## introduction automated theorem proving (atp) @xcite has been considered an essential task of artificial intelligence (ai) ever since the birth of modern ai @xcite . besides its remarkable theoretical value and huge potential to accelerate research in mathematics, atp already demonstrates excellent application value in, for ex-figure 1 : illustration of a theorem and its proof in @xcite . the theorem sub_ne_zero_of_ne states that if the hypothesis h holds (i.e. we have a ̸ = b), then we have ab ̸ = 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. 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 in which the theorem and the proof are formalized. we show in fig. 1 an example of a theorem proven in @xcite , a formal environment we use in this work. sec.2.1 gives more details on the formal environment. to deal with this theorem proving problem automatically, many task-specific algorithms have been proposed and are later implemented as stateof-the-art atp solvers such as z3 @xcite , vampire @xcite , e @xcite and zipperposition @xcite . these approaches are taskspecific in that they are specific to one given formal environment and rely on solid domain knowledge, symbolic operations, and usually human heuris-tics. with the exciting development of deep learning @xcite over the past decade, approaches (not necessarily for atp) in the taskagnostic paradigm have been proposed, such as alphazero @xcite and more recently gato @xcite . as for atp, task-agnostic approaches are also proposed. for example, gptf @xcite ) uses a language model to suggest a set of candidates for the next proof step and then search for a complete valid proof within the formal system metamath (megill and @xcite . in contrast to classic atp algorithms, gpt-f has remarkable generality and can be applied to any atp tasks in any formal system, such as propositional logic, first-order logic, higherorder logic, typed lambda calculi, etc. with gpt-f, domain knowledge and human heuristics are no more absolutely required. some works following the workflow of gpt-f are introduced in a.2. although approaches such as gpt-f demonstrate impressive generality and performance, they still have two significant drawbacks. on the one hand, gpt-f consumes considerable computational resources. according to @xcite , the original gpt-f requires 2000 gpu days (a100) for training, and their approach htps (hypertree proof search @xcite ) also consumes more than 1000 gpu days for one training process, which sets a prohibitive threshold for most researchers. even worse, the cost for inference with gpt models and search can be 5 to 10 times heavier than that of training. on the other hand, the search process in gpt-f could reach a state of 'empty queue', where all proof step candidates (i.e. all leaf nodes in the search tree) generated by the language model turn out to be inapplicable. this can typically take place within the time budget and an premature 'failed' result is returned, potentially resulting in a low pass rate (sometimes we also use the term 'one-pass success rate' to be more specific). also, prior works @xcite @xcite 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. in this work, we address the above two issues and propose a novel dynamic-tree driven theorem solver (dt-solver). as an automated theorem-proving algorithm, dt-solver uses dynamic-tree sampling guided by a proof-level value function. we illustrate these two main components as follows. ## methodology starting from the initial state of the theorem, dt-solver adapts the language model to suggest forward-moving actions and empowers dynamictree sampling guided by a proof-level value function to find the complete proof path. this is ac-complished by a three-step pipeline: (1) following procedures described in sec. 2.2, dt-solver trains a language model using supervised data extracted from formal mathematics libraries to predict proof steps based on proof states. the trained language model is called the policy model. (2) subsequently, dynamic-tree sampling uses the trained policy model to generate steps and searches for theorems proofs in the training set. a data collection procedure collects proof trajectories from successful proof searches. (3) lastly, dt-solver trains the proof-level value function (called the critic model) to identify promising proof paths from astray ones on collected data with a classification loss. at test time, to evaluate the performance of our method, we use the trained policy model and critic model to perform dynamic-tree sampling on the test set theorems. in the following section, we first introduce the dynamic-tree sampling algorithm and the data collection procedure (sec.3.1). after that, we introduce our proof-level value function (sec. 3.2). ## conclusion in this work, we introduced a new atp method, dt-solver, which uses a proof-level value function to guide the dynamic tree sampling algorithm. dt-solver smartly allocates computational budget to states that require more exploration and reduces the cost on easy states. the proof-level value function effectively locates difficult states. extensive tests show that our method can indeed improve success rates on both pisa and mathlib datasets while being efficient enough to find proofs within a limited time budget. although our method brings substantial advantages, there remain multiple aspects for improvement in the future, such as utilizing the for-mal environment's feedback or reducing enormous search spaces with high-level proof planning.