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

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 lightweight, one-pass data synthesis method that explores a wide range of intermediate proof states to generate diverse proof steps, which facilitates effective one-shot fine-tuning of the LLM 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 achieves competitive results compared to strong baselines, attaining an average pass rate of 60.74% on MiniF2F and 21.18% on ProofNet under the stringent Pass@1 metric, as well as a 68.85% pass rate on MiniF2F under the Pass@16 metric. These results underscore the impact of large-scale synthetic data in advancing automated theorem proving.