HunyuanProver：面向自动定理证明的可扩展数据合成框架与引导树搜索
人工智能
2025-03-24 v3 计算与语言
摘要
我们介绍 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）。为 benefiting 社区，我们将开源一个包含 30k 个合成实例的数据集，其中每个实例包含原始自然语言问题、由自动化形式化转换的陈述，以及由 HunyuanProver 提供的证明。
关键词
引用
@article{arxiv.2412.20735,
title = {HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving},
author = {Yang Li and Dong Du and Linfeng Song and Chen Li and Weikang Wang and Tao Yang and Haitao Mi},
journal= {arXiv preprint arXiv:2412.20735},
year = {2025}
}