HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866913749148893184 |
|---|---|
| author | Li, Yang Du, Dong Song, Linfeng Li, Chen Wang, Weikang Yang, Tao Mi, Haitao |
| author_facet | Li, Yang Du, Dong Song, Linfeng Li, Chen Wang, Weikang Yang, Tao Mi, Haitao |
| contents | We introduce HunyuanProver, an language model finetuned from the Hunyuan 7B for interactive automatic theorem proving with LEAN4. To alleviate the data sparsity issue, we design a scalable framework to iterative synthesize data with low cost. Besides, guided tree search algorithms are designed to enable effective ``system 2 thinking`` of the prover. HunyuanProver achieves state-of-the-art (SOTA) performances on major benchmarks. Specifically, it achieves a pass of 68.4% on the miniF2F-test compared to 65.9%, the current SOTA results. It proves 4 IMO statements (imo_1960_p2, imo_1962_p2}, imo_1964_p2 and imo_1983_p6) in miniF2F-test. To benefit the community, we will open-source a dataset of 30k synthesized instances, where each instance contains the original question in natural language, the converted statement by autoformalization, and the proof by HunyuanProver. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2412_20735 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving Li, Yang Du, Dong Song, Linfeng Li, Chen Wang, Weikang Yang, Tao Mi, Haitao Artificial Intelligence Computation and Language We introduce HunyuanProver, an language model finetuned from the Hunyuan 7B for interactive automatic theorem proving with LEAN4. To alleviate the data sparsity issue, we design a scalable framework to iterative synthesize data with low cost. Besides, guided tree search algorithms are designed to enable effective ``system 2 thinking`` of the prover. HunyuanProver achieves state-of-the-art (SOTA) performances on major benchmarks. Specifically, it achieves a pass of 68.4% on the miniF2F-test compared to 65.9%, the current SOTA results. It proves 4 IMO statements (imo_1960_p2, imo_1962_p2}, imo_1964_p2 and imo_1983_p6) in miniF2F-test. To benefit the community, we will open-source a dataset of 30k synthesized instances, where each instance contains the original question in natural language, the converted statement by autoformalization, and the proof by HunyuanProver. |
| title | HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving |
| topic | Artificial Intelligence Computation and Language |
| url | https://arxiv.org/abs/2412.20735 |