ATG : Benchmarking Automated Theorem Generation for Generative Language Models (2024)

Abstract: Humans can develop new theorems to explore broader and more complex mathematical results.While current generative language models (LMs) have achieved significant improvement in automatically proving theorems, their ability to generate new or reusable theorems is still under-explored. Without the new theorems, current LMs struggle to prove harder theorems that are distant from the given hypotheses with the exponentially growing search space.More advanced theorem proving is if an agent (for instance, a generative LM) can leverage its creativity to generate new but also reasonable theorems that properly substitute part of a proof and also be saved as reusable knowledge for future theorem proving.Therefore, this paper proposes an Automated Theorem Generation (ATG) benchmark that evaluates whether an agent can automatically generate valuable (and possibly brand new) theorems that are applicable for downstream theorem proving as reusable knowledge. Specifically, we construct the ATG benchmark by splitting the Metamath library into three sets: axioms, library, and problem based on their proving depth.We conduct extensive experiments to investigate whether current LMs can generate theorems in the library and benefit the problem theorems proving. The results demonstrate that high-quality ATG data facilitates models’ performances on downstream ATP. However, there is still room for current LMs to develop better ATG and generate more advanced and human-like theorems. We hope the new ATG challenge can shed some light on advanced complex theorem proving.

## introduction recent generative language models (lms) can perform advanced mathematical reasoning including automated theorem proving (atp) @xcite where the lms need to provide a proof for a given theorem. some studies @xcite use the lms to perform all-at-once generation to obtain the proof, while another line of work @xcite leverages multi-step generation and combines reinforcement learning @xcite , expert iteration ( @xcite , or reflection techniques @xcite to simulate the multistep search process. given the models achieve some complex theorem proving, a shared limitation is their inability to reuse sub-propositions while proving or developing new theorems as humans do, which also leads to redundant proving processes and low efficiency. one demonstration is shown in figure 1 . given a basic propositional logic system (as shown in the top box), gpt-4 struggles deriving the basic proposition (@xmath0. although gpt-4 being the most advanced language model performs formal logical reasoning to a certain extent @xcite , in this case, it wrongly refers to the intermediate theorem in step 3 and axioms in steps 4 and 5. this case suggests an overlooked performance gap between lms and humans in rigorous logical and structured derivation. moreover, current state-of-the-art neural atp methods @xcite do not reuse the searched sub-propositions in proving sequences. thus they do not decompose the complex theorems into sub-problems and still suffer from the exponential search space. to address the above-mentioned issues, we need to develop the capability of an agent to automatically create new and reusable theorems that are applicable for downstream theorem proving. for example, generating a theorem that can serve as a general sub-problem in proofs. moreover, such new theorems as a data source can further facilitate model parameter updates. however, this question is under-explored and needs a clear problem definition and available data source. this paper thus introduces the automated theorem generation (atg) task, where the lms are required to automatically generate valuable theorems when given a set of axioms, and reduce the proof steps accordingly. figure 2 illustrates the atg task. in this case, an atg method is given axioms ("ax-1", "ax-mp", and "ax-3") and should properly deduce the theorem "pm2.21i", which effectively simplifies the proof by reducing the original steps 4-7 with the new step 4. the proposed atg task has the following merits. firstly, the forward deduction process in atg is more aligned with text or code generation. since the lms have shown impressive performance @xcite , the atg task can better probe lms' reasoning ability. secondly, the generated theorems can be used in proving other theorems, and reduce the proof difficulties by deducing the intermediate steps from given axioms. accordingly, we construct an atg benchmark based on the metamath formal system @xcite and its "set.mm" library foot_0 . we also propose new metrics to evaluate the generated theorems by considering the correctness, compactness, and usefulness of the proving target theorems. furthermore, we combine the monte carlo tree search method @xcite with lms and train the pipeline with selfplay policy learning to generate valuable theorems. the generated theorems, as augmented data training theorems prover, improved the performance of holophrasm @xcite and gpt-f (polu and sutskever, 2020) by 16.16% (passrate@1, from 20.48% to 23.79%) and 7.72% (passrate@1, from 30.94% to 33.53%), respectively. our contributions are summarized as follows: ## related work over the past few years, generative language models @xcite @xcite have achieved better mathematical reasoning. for example, solving math word problems @xcite @xcite , linear programming @xcite , and parametric partial differential equations @xcite . among the mathematical reasoning tasks, automated theorem proving @xcite @xcite @xcite is one of the most challenging tasks as requires the neural models to perform consistent reasoning and rigorous multi-step deduction. more recent work @xcite applies the generative lm to automated theorem proving, and following works improve the pipeline with kernellevel proof terms @xcite , expert iteration @xcite , hypertree proof search @xcite , and sketching intermediate theorems @xcite . such works suggest a great potential for generative lms to prove theorems. however, a more advanced capability of synthesizing new and provable theorems and reusing them as intermediate proofs during proving remains unexplored. synthesizing theorems and their applications are in the preliminary research stage. previous works theoretically investigate theorem generation systems by executing computer programs @xcite @xcite @xcite @xcite or by deriving from proof schemes @xcite @xcite . such systems are barely applicable to modern neural models. another line of work @xcite @xcite leverages transformer-based lms to generate theorems. however, the quality of the generated theorems is not guaranteed, and thus are less beneficial for downstream applications such as automated theorem proving (atp). therefore, this work proposes a rigorous task that challenges models to perform automated theorem generation and introduces corresponding metrics. to our knowledge, this is the first work on benchmarking neural automated theorem generation, and the resulting synthetic theorems can be directly applied to atp. ## self-play policy learning in this section, we propose a theorem generation method based on monte carlo tree search and selfplay learning. we use the current proof stack as a state and act to apply one possible axiom, hypothesis, or theorem. starting with an empty state, we iteratively select a state and action to expand based on policy/value network (pvn) output until a valid proof or maximum length is reached. during training, we sample state-action/state-value pairs with policy/value networks and use the sample pairs as supervised signals. action actions are axioms or hypotheses that can be applied during theorem generation. we use a subset of possible actions during each generation. specifically, the sub-action space includes all axioms and all symbols such as φ, ψ, χ. we randomly add 5 theorems from the current generated theorem library l ′ t and then sample 5 hypotheses from proof of the selected theorems. we further build a graph indicating their referring relation, as shown in figure 6 . state the state represents the current proof stack. as shown in figure 6 , we start with an empty state "{}" s 0 . if we apply action φ, then the resulting state s 1 is "φ". further applying action ψ and "ax-1", we obtain the state s 5 = {φ, ψ, ax-1} and reduce to φ → ψ. monte carlo tree search we expand the initial empty state iteratively until we reach a valid proof or a maximum step. figure 6 shows the process of one-step expansion. at each step, we first obtain the policy probability and value for all state-action pairs. specifically, we apply gpt2-large @xcite to encode the action history with special prefix tokens. for example, to encode state s 3 , we input sequence "[cls] proofstep wph wps" to the lm, where "[cls] proofstep" is the prefix and "wph" and "wps" represent ϕ and ψ in metamath. we also use a graph convolution network @xcite to encode the action and their relations. the action features are then concatenated with the state feature, then flattened and fed into a fully connected layer to obtain the value of current state v(s, a) and the policy probability π(a|s) for all possible actions. given the policy π(a|s) and the value v(s, a), we obtain the puct @xcite scores: ## conclusion this paper introduces the automated theorem generation (atg) task that evaluates generative language models' capability of generating highquality theorems and reducing complex theorems. we also introduce evaluation metrics that consider the correctness, compactness, and usefulness of the generated theorems. we conduct extensive experiments and find that high-quality human-like theorems benefit downstream tasks such as automated theorem proving. moreover, there is still room for current language models to generate such high-quality theorems. therefore, we hope the proposed atg benchmark can facilitate the development of language models' theorem generation and thus improve the overall theorem proving.