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

Yang Li; Dong Du; Linfeng Song; Chen Li; Weikang Wang; Tao Yang; Haitao Mi

返回文献探索

Paper · arXiv 2412.20735

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

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

11 upvotesDecember 30, 2024arXiv 预印本

AI 摘要

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.

language modelHunyuan 7Binteractive automatic theorem provingLEAN4data sparsityscalable frameworkiterative synthesizelow costguided tree search algorithmssystem 2 thinkingstate-of-the-art performanceminiF2F-testautoformalization

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.