LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916742085738496 |
|---|---|
| author | Lai, Junyu Zhang, Jiakun Xu, Shuo Chen, Taolue Wang, Zihang Yang, Yao Zhang, Jiarui Cao, Chun Xu, Jingwei |
| author_facet | Lai, Junyu Zhang, Jiakun Xu, Shuo Chen, Taolue Wang, Zihang Yang, Yao Zhang, Jiarui Cao, Chun Xu, Jingwei |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_12031 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation Lai, Junyu Zhang, Jiakun Xu, Shuo Chen, Taolue Wang, Zihang Yang, Yao Zhang, Jiarui Cao, Chun Xu, Jingwei Artificial Intelligence I.2.7 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. |
| title | LLM-based Automated Theorem Proving Hinges on Scalable Synthetic Data Generation |
| topic | Artificial Intelligence I.2.7 |
| url | https://arxiv.org/abs/2505.12031 |