近年来，人工智能技术的突破性发展使其在其他领域的应用得到极大关注。数学作为基础科学的核心，将AI技术融入到数学研究领域，不仅可以加速数学定理的证明和新猜想的发现，在处理实际复杂问题中也发挥着重要作用。AI驱动的数学研究不仅是对传统方法的补充，也为数学理论探索开辟了新的视野和可能性。

软件工程学院（滴水湖国际软件学院）研究生围绕非线性约束求解与自动定理证明等问题取得阶段性进展，相关成果获得EMSOFT 2024最佳论文提名以及ICML 2024数学自动推理挑战赛第一名的好成绩。

面向CPS验证的学习型非线性约束求解方法

安全攸关系统形式化验证的核心数学问题是非线性约束求解，如何设计快速算法提高验证效率是一项挑战。针对面向安全验证的非线性约束求解问题，软件工程学院（滴水湖国际软件学院）赵韩蕊（2021级博士）提出了一种学习型非线性约束求解方法，通过构造学习驱动的障碍证书，将NP-hard的双线性矩阵不等式约束求解问题近似转化为逐次凸的线性矩阵不等式可行性判定问题。这一创新使得障碍证书在生成维度和效率上均超越了目前最先进的学习和传统数值计算方法，并能够处理更复杂的CPS验证问题。

该研究成果已被嵌入式系统领域的顶级会议EMSOFT收录，并获得最佳论文提名。论文将在顶级期刊《IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD)》发表。华东师范大学为唯一完成单位，论文其他合作者包括刘邦龙（2023级硕士）、Lydia Dehbi（博士后）、谢慧娇（2022级硕士）、杨争峰教授和钱海峰研究员。

融合大语言模型与强化学习的定理自动生成及证明

数学推理是人类智力的最高形式之一。人类通过使用形式语言来严格描述数学问题并推导数学知识。自动定理证明是一项意义重大且极具挑战性的任务。尽管大型语言模型(large language models，LLMs)在数学推理方面表现出了潜力，但由于训练数据的稀缺性，它们在形式化定理证明方面的能力仍然有限。

近日，学院研究生王蕾（2023级硕士）、左若冰（2024级硕士）、史书铭（2024级硕士）、任勐鑫（2024级硕士）和单好佳（2023级硕士）在杨争峰教授的指导下，参加了ICML 2024自动数学推理挑战赛（ICML 2024 Challenges on Automated Math Reasoning）。其提出的融合大语言模型与强化学习的自动定理生成（ATG）算法，成功应对了这一挑战，并在自动定理生成和证明赛道中获得了第一名。