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.

本文引入HunyuanProver，一个基于Hunyuan 7B的语言模型，旨在解决数据稀疏问题，提供一个低成本的数据合成框架。此外，设计了引导树搜索算法以促进定理证明的“系统2思维”。研究表明，HunyuanProver在重要基准测试中实现了最新的性能，尤其是在miniF2F-test中通过率达到68.4%。

HUNYUANPROVER：可扩展的数据合成框架和引导树搜索用于自动定理证明