基于自动定理生成的组合恒等式基准测试
人工智能
2025-02-26 v1
摘要
大型语言模型（LLM）在形式定理证明方面取得了显著进展，但稀缺的高质量训练数据限制了其在复杂数学领域的能力。组合数学作为数学的基石，为分析离散结构和解决优化问题提供了 essential 工具。然而，其内在复杂性使得自动定理证明（ATP）针对组合恒等式 particularly 有具有挑战性。为此，我们手动构建 LeanComb——一个针对组合恒等式的定理证明基准，据称是首个为组合恒等式 formal 化的定理证明基准。我们开发了用于组合恒等式的自动定理生成器（ATG4CI），其结合了来自自我改进大型语言模型所建议的候选 tactic 与强化学习树搜索方法进行 tactic 预测。通过利用 ATG4CI，我们生成了 LeanComb-Enhanced 数据集，包含 26 万个组合恒等式定理，每个定理都有一个完整的 Lean formal 证明。实验评估表明，基于该数据集训练的模型能够生成更有效的 tactic，从而提高了在组合恒等式自动定理证明中的成功率。
引用
@article{arxiv.2502.17840,
title = {A Combinatorial Identities Benchmark for Theorem Proving via Automated Theorem Generation},
author = {Beibei Xiong and Hangyu Lv and Haojia Shan and Jianlin Wang and Zhengfeng Yang and Lihong Zhi},
journal= {arXiv preprint arXiv:2502.17840},
year = {2025}
}