title: HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree
    Search for Automated Theorem Proving
summary: 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.
paper_authors._id: 6776bdde4f9262d263382cf3
paper_authors.name: Yang Li
paper_authors._id: 6776bdde4f9262d263382cf4
paper_authors.name: Dong Du
paper_authors._id: 6776bdde4f9262d263382cf5
paper_authors.name: Linfeng Song
paper_authors._id: 6776bdde4f9262d263382cf6
paper_authors.name: Chen Li
paper_authors._id: 6776bdde4f9262d263382cf7
paper_authors.name: Weikang Wang
paper_authors._id: 6776bdde4f9262d263382cf8
paper_authors.name: Tao Yang
paper_authors._id: 6776bdde4f9262d263382cf9
paper_authors.name: Haitao Mi
paper_title: HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree
    Search for Automated Theorem Proving
paper_summary: 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.
paper_ai_summary: HunyuanProver, a language model fine-tuned for interactive theorem proving with LEAN4, achieves state-of-the-art performance on benchmarks by using a scalable data synthesis framework and guided tree search algorithms.
paper_ai_keywords: language model Hunyuan 7B interactive automatic theorem proving LEAN4 data sparsity scalable framework iterative synthesize low cost guided tree search algorithms system 2 thinking state-of-the-art performance miniF2F-test autoformalization