ATG: Benchmarking Automated Theorem Generation for Generative Language Models

TL;DR

The paper addresses the gap in automated theorem generation by introducing ATG, a benchmark built on the Metamath/set.mm framework to generate reusable theorems that accelerate downstream proving. It defines a formal task, proposes robust evaluation metrics (APR, Human-Aligned Precision, Theorem Count), and creates wb/wif/minimp datasets to study generation across depths. The authors present a self-play policy learning pipeline using Monte Carlo Tree Search guided by neural policy/value networks, demonstrating that high-quality ATG data can improve ATP performance for Holophrasm and GPT-f, with notable gains when combined with human-annotated theorems. This work offers a practical pathway to improve complex theorem proving by enabling models to synthesize and reuse subpropositions, with broader implications for formal methods and AI-assisted mathematical reasoning.

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

Figures (11)

• Figure 1: An example theorem generated by GPT-4 gpt-4. GPT-4 wrongly refers to the intermediate theorem $(A\rightarrow(B\rightarrow A)\rightarrow A \rightarrow A)$ as $((A \rightarrow B)\rightarrow(A\rightarrow A))$. In Step 4, it applies "ax-1" but obtains the wrong expression instead of correct ($A\rightarrow(B\rightarrow A)$) and can not derive ($A\rightarrow A$) even with the incorrect Steps 4 and 5.
• Figure 2: Illustration of the Automated Theorem Generation (ATG) task and the process of proof reduction. Black and green lines represent the proof and generation paths, while the red line is the new proof step. It takes 7 steps to prove the theorem "pm2.21dd" with given theorem "pm2.21i" and axioms while an ATG model can properly deduce the theorem "pm2.21i" and the total proof length of theorem "pm2.21dd" reduces from 7 steps to 4 steps.
• Figure 3: Example of proving with Metamath script. The script and verification process are shown on the left and the visualized proof step on the right. The script starts with defining symbols, hypotheses, and referred theorems. It pushes variables into the stack and applies substitution when encountering theorems. The applied result is pushed into the stack. The proof terminates when no more theorems are pushed in the stack.
• Figure 4: The construction process of the ATG benchmark. Each node is a theorem in "set.mm" and edges represent if a node refers to another in its proof. We assign each node a depth and use it to split the theorem library $\mathbb{L'}$ and $\mathbb{P}$. Lastly, we select the red node and use all its successor nodes for testing.
• Figure 5: Statistics of proof depth, tokens, and referred theorems of test theorem library.