LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation

TL;DR

This work addresses the data bottleneck in LLM-based automated theorem proving by introducing proof-state exploration to synthesize large-scale, diverse intermediate proof states for fine-tuning a policy model. It couples this data-generation approach with an adaptive beam size strategy in tree search, balancing exploration and exploitation to improve proof completion under limited computational budgets. Empirical results on MiniF2F and ProofNet show state-of-the-art performance among tree-search methods with Pass@1 scores of ${60.74\%}$ and ${21.18\%}$, respectively, highlighting the value of scalable synthetic data in advancing ATP. The DoBeVi visualization and Lean 4 interaction tooling further support practical integration and analysis of the search process, suggesting a promising direction for neuro-symbolic ATP systems.

Abstract

Recent advancements in large language models (LLMs) have sparked considerable interest in automated theorem proving and a prominent line of research integrates stepwise LLM-based provers into tree search. In this paper, we introduce a novel proof-state exploration approach for training data synthesis, designed to produce diverse tactics across a wide range of intermediate proof states, thereby facilitating effective one-shot fine-tuning of LLM as the policy model. We also propose an adaptive beam size strategy, which effectively takes advantage of our data synthesis method and achieves a trade-off between exploration and exploitation during tree search. Evaluations on the MiniF2F and ProofNet benchmarks demonstrate that our method outperforms strong baselines under the stringent Pass@1 metric, attaining an average pass rate of $60.74\%$ on MiniF2F and $21.18\%$ on ProofNet. These results underscore the impact of large-scale synthetic data in advancing automated theorem proving.

Figures (5)

• Figure 1: An illustration of the proposed tree search strategy. The example is derived from the MiniF2F benchmark, specifically the problem algebra_9onxpypzleqsum2onxpy. For simplicity, only the tactics are retained in the depicted proof states, while the associated premises are omitted.
• Figure 2: An illustration of the data synthesis pipeline.
• Figure 3: A example of search tree(amc12_2000_p6 in MiniF2F). Rectangular nodes represent Open Nodes, red elliptical nodes indicate Error Nodes, and green nodes denote ProofFinished Nodes. Edges are labeled with the applied tactic and its associated beam probability (beam_prob). Each node is annotated with its unique id and current score.
• Figure 4: Distribution of the top 60 most frequent tactics in the STP dataset.
• Figure 5: Frequency distribution of search depths of proving paths generated by our policy model on the MiniF2F benchmark, with the maximum number of expansions fixed at 600 ($E=600$).