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

📄 arXiv: 2412.20735v3 📥 PDF

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

分类: cs.AI, cs.CL

发布日期: 2024-12-30 (更新: 2025-03-21)

💡 一句话要点

HunyuanProver：一种可扩展的数据合成框架和引导树搜索的自动定理证明方法

🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction)

关键词: 自动定理证明 数据合成 语言模型 树搜索 LEAN4 HunyuanProver miniF2F

📋 核心要点

  1. 现有自动定理证明方法面临数据稀疏的挑战，限制了模型的泛化能力和证明能力。
  2. HunyuanProver通过可扩展的数据合成框架和引导树搜索算法，提升了定理证明的效率和准确性。
  3. 实验结果表明，HunyuanProver在miniF2F-test上取得了SOTA性能，证明了其有效性。

📝 摘要（中文）

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

🔬 方法详解

问题定义：自动定理证明旨在利用计算机程序自动推导数学定理。现有方法面临数据稀疏的问题，即缺乏足够数量和多样性的训练数据，导致模型难以学习到有效的证明策略，从而限制了其在复杂定理证明任务中的表现。

核心思路：本文的核心思路是通过数据合成来扩充训练数据集，并结合引导树搜索算法来提升证明效率。数据合成旨在生成更多样化的训练样本，而引导树搜索则模拟人类的思考过程，帮助模型更有效地探索证明空间。

技术框架：HunyuanProver的整体框架包含数据合成模块、模型训练模块和证明搜索模块。数据合成模块负责生成新的训练样本，模型训练模块使用合成数据对Hunyuan 7B语言模型进行微调，证明搜索模块则利用引导树搜索算法来寻找定理的证明。

关键创新：该论文的关键创新在于可扩展的数据合成框架和引导树搜索算法。数据合成框架能够以较低的成本生成大量的训练数据，有效缓解了数据稀疏问题。引导树搜索算法则通过模拟人类的思考过程，提升了证明的效率和准确性。

关键设计：数据合成框架的具体实现细节未知，但强调了其可扩展性和低成本。引导树搜索算法的具体设计细节也未知，但其目标是模拟人类的“系统2思考”，即有意识的、分析性的思考过程。HunyuanProver基于Hunyuan 7B语言模型进行微调，具体的微调策略和损失函数未知。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

HunyuanProver在miniF2F-test上取得了68.4%的通过率，超越了当前SOTA结果65.9%。此外，它成功证明了miniF2F-test中的4个IMO陈述（imo_1960_p2, imo_1962_p2, imo_1964_p2 和 imo_1983_p6），表明其在复杂定理证明任务中具有强大的能力。

🎯 应用场景

HunyuanProver可应用于数学、计算机科学等领域的自动定理证明，辅助研究人员进行定理推导和验证，提高科研效率。此外，该技术还可应用于智能合约验证、程序正确性验证等领域，提升软件系统的可靠性和安全性。未来，该研究有望推动人工智能在数学推理和逻辑推理方面的应用。

📄 摘要（原文）

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.