报告名称：面向组合数学的定理自动生成和证明

报告专家：杨争峰

专家所在单位：华东师范大学

报告时间：2025-06-09，下午16:30-17:30点

报告地点: 数统楼203

专家简介：

杨争峰，华东师范大学软件工程学院教授。于2006年获得中国科学院数学与系统科学研究院博士学位。主要研究方向为数学机械化、人工智能数学、混成系统验证等。迄今为止在CAV、FM、ISSAC、NeurIPS、CVPR、EMSOFT等国际会议和ACM TECS、IEEE TCAD、JSC等国际期刊上发表了80余篇论文。近年来主持国家重点研发计划“数学和应用研究”专项课题、国防科工委创新项目、国家自然科学基金等多个科研课题的研究。

报告摘要：

自动化定理证明（ATP）传统上依赖于证明搜索，近年来，随着大语言模型的快速发展，AI赋能的定理自动证明已成为一种新范式。然而，由于现有证明数据的匮乏，基于人工智能的定理自动证明仍面临诸多挑战。针对组合恒等式定理自动证明问题，我们提出了一种结合大语言模型与强化学习的定理自动生成方法；通过融合人工形式化与定理自动生成，我们开发了一个基于Lean的组合恒等式形式化数据集LeanComb，及其相应的定理自动证明器；实验结果表明，针对组合恒等式的定理自动证明问题，我们开发的证明器在准确率上优于现有的证明器，且提出的定理自动生成方法显著提高了自动证明的效率和准确率。