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中，與當前最先進的SOTA結果65.9%相比，實現了68.4%的通過率。它證明了4個IMO陳述（imo_1960_p2、imo_1962_p2、imo_1964_p2和imo_1983_p6）在miniF2F-test中。為了造福社區，我們將開源一個包含30k合成實例的數據集，每個實例包含自然語言中的原始問題、自動形式化轉換的陳述以及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.