AI4Math：自动形式化与语义评估
报告专家：罗涛副教授（上海交通大学）
报告时间：9月9日（星期二）上午10:30-11:30
报告地点：国家天元数学西南中心516
报告摘要：
数学人工智能（AI4Math）是一个快速发展的领域，对学术研究和工业应用都具有重要意义。本次报告中，我们将回顾人工智能驱动的数学推理发展历程，追溯从基于自然语言的直觉性方法到形式语言支撑的严谨可验证证明的转变。在提供基础概述后，我们针对形式化系统中的三个关键研究前沿展开技术性综述：自动定理证明、自动形式化与自动语义评估。重点聚焦我们在后两个领域的研究贡献，这些工作对弥补人类数学知识与机器可验证逻辑之间的鸿沟具有重要意义。
专家简介：
罗涛博士现任上海交通大学数学科学学院/自然科学研究院副教授。研究方向聚焦机器学习与材料科学的数学理论。他于2012年获上海交通大学致远学院学士学位，2017年获香港科技大学博士学位，并荣获香港数学学会最佳博士论文奖。2017至2020年期间，担任普渡大学数学系Golomb访问助理教授。他在深度学习的频率原理与凝聚现象、材料科学的Peierls-Nabarro模型、外延生长及Cauchy-Born准则等研究领域做出贡献，相关成果发表于SIAM系列期刊、Arch. Ration. Mech. Anal.、J. Mach. Learn. Res.、NeurIPS和ICLR等国际顶级会议与期刊。
邀请人：郭汝驰
