用低成本数据合成与引导搜索，让大模型在数学定理证明上超越现有水平。
HunyuanProver: A Scalable Data Synthesis Framework and Guided Tree Search for Automated Theorem Proving
- 基于Hunyuan 7B微调模型，结合迭代数据合成缓解训练数据稀缺问题。
- 在miniF2F-test上达到68.4%通过率，成功证明4道国际数学奥赛题。
- 开源3万条合成数据集，含自然语言题目、形式化陈述和完整证明。
我们提出HunyuanProver，一个基于Hunyuan 7B微调的交互式自动定理证明系统，用于LEAN4。为缓解数据稀疏问题，设计了低成本可扩展的数据迭代合成框架。此外，引入引导树搜索算法，实现推理系统的“系统2思维”。HunyuanProver在主流基准上表现领先：在miniF2F-test上通过率达68.4%，优于当前SOTA的65.9%；成功证明4道国际数学奥林匹克（IMO）试题（imo_1960_p2, imo_1962_p2, imo_1964_p2, imo_1983_p6）。为促进社区发展，将开源包含3万条实例的数据集，每条包含自然语言原题、自动形式化后的命题及模型生成的完整证明。
原文摘要 · Abstract (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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。