报告人：罗涛 副教授 上海交通大学

报告题目：AI4Math：自动形式化与语义评估

时间：2026年1月13日15:00—17:00

地点：北五楼427

摘要：

数学人工智能（AI4Math）是一个快速发展的领域，对学术研究和工业应用都具有重要意义。本次报告中，我们将回顾人工智能驱动的数学推理发展历程，追溯从基于自然语言的直觉性方法到形式语言支撑的严谨可验证证明的转变。在提供基础概述后，我们针对形式化系统中的三个关键研究前沿展开技术性综述：自动定理证明、自动形式化与自动语义评估。重点聚焦我们在后两个领域的研究贡献，这些工作对弥补人类数学知识与机器可验证逻辑之间的鸿沟具有重要意义。

报告人简介：

罗涛是上海交通大学长聘教轨副教授，入选上海海外高层次人才引进计划。2012年在上海交大首届致远学院理科班获学士学位。2017年在香港科技大学获得数学博士学位，获香港数学会最佳博士论文奖。2017-2020年在普渡大学数学系任Golomb访问助理教授。2020年加入上海交通大学数学科学学院和自然科学研究院。研究领域为机器学习和材料科学的数学理论。在深度学习的AI4Math、隐式偏好、误差分析等方向和材料科学的晶体位错、外延生长等方向具有代表性的成果，相关成果发表在应用数学和机器学习的一流期刊或会议上（如SIAM系列、ARMA、JMLR、NeurIPS、ICLR等）30余篇。其中一篇论文被NeurIPS 2025接收为oral。

邀请人：王飞 教授