HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree
  Search for Automated Theorem Proving
Authors: name: Yang Li; name: Dong Du; name: Linfeng Song; name: Chen Li; name: Weikang Wang; name: Tao Yang; name: Haitao Mi
Published: 2024-12-30 06:18:33

Abstract: 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.