构建首个组合恒等式形式化证明基准，提升AI自动证明能力
A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation
- 用自进化大模型+强化学习树搜索生成定理
- 产出26万条带完整形式化证明的组合恒等式
- 适合研究AI数学证明与形式化验证的学者
大型语言模型在形式化定理证明方面取得显著进展，但高质量训练数据的缺乏限制了其在复杂数学领域的能力。组合数学是分析离散结构和优化问题的核心工具，但其内在复杂性使自动定理证明面临挑战。为此，我们手工构建了首个针对组合恒等式的形式化证明基准LeanComb。开发了组合恒等式自动定理生成器ATG4CI，结合自改进大模型建议的候选策略与强化学习树搜索进行策略预测。利用ATG4CI生成了包含26万条组合恒等式定理的LeanComb-Enhanced数据集，每条均配有完整的形式化证明。实验表明，基于该数据集训练的模型能生成更有效的策略，从而显著提升组合恒等式自动定理证明的成功率。
原文摘要 · Abstract (English)
Large language models (LLMs) have significantly advanced formal theorem proving, yet the scarcity of high-quality training data constrains their capabilities in complex mathematical domains. Combinatorics, a cornerstone of mathematics, provides essential tools for analyzing discrete structures and solving optimization problems. However, its inherent complexity makes it particularly challenging for automated theorem proving (ATP) for combinatorial identities. To address this, we manually construct LeanComb, combinatorial identities benchmark in Lean, which is, to our knowledge, the first formalized theorem proving benchmark built for combinatorial identities. We develop an Automated Theorem Generator for Combinatorial Identities, ATG4CI, which combines candidate tactics suggested by a self-improving large language model with a Reinforcement Learning Tree Search approach for tactic prediction. By utilizing ATG4CI, we generate a LeanComb-Enhanced dataset comprising 260K combinatorial identities theorems, each with a complete formal proof in Lean, and experimental evaluations demonstrate that models trained on this dataset can generate more effective tactics, thereby improving success rates in automated theorem proving for combinatorial identities.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。