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

HUNYUANPROVER: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving

December 30, 2024

作者: Yang Li, Dong Du, Linfeng Song, Chen Li, Weikang Wang, Tao Yang, Haitao Mi

cs.AI

摘要

我们介绍HunyuanProver，这是从Hunyuan 7B微调而来的语言模型，用于与LEAN4一起进行交互式自动定理证明。为了缓解数据稀疏问题，我们设计了一个可扩展的框架来迭代合成数据，成本较低。此外，我们设计了引导树搜索算法，以实现证明者有效的“系统2思维”。HunyuanProver在主要基准测试中实现了最先进的性能。具体来说，在miniF2F-test中，它的通过率为68.4%，而当前最先进的结果为65.9%。它证明了4个IMO命题（imo_1960_p2，imo_1962_p2，imo_1964_p2和imo_1983_p6）。为了造福社区，我们将开源一个包含3万个合成实例的数据集，每个实例包含自然语言中的原始问题、自动形式化转换的陈述，以及HunyuanProver的证明。

English

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.